Em 26 de outubro, a OpenAI anunciou que seus modelos refutaram a hipótese.
A OpenAI diz que formalizou a prova no Lean em 17 de outubro.
A OpenAI informou que um grupo externo está analisando a descoberta.
A Anthropic diz que Claude descobriu um algoritmo que refutaria a hipótese.
A Anthropic diz que o resultado é assintótico e nada afirma sobre resolver fórmulas na prática.
A OpenAI e a Anthropic divulgaram resultados gerados por IA que afirmam refutar a Hipótese do Tempo Exponencial, uma conjectura antiga da teoria da complexidade computacional.
Em 26 de outubro, a OpenAI anunciou que seus modelos produziram uma prova de que a Hipótese do Tempo Exponencial é falsa. A hipótese, proposta no início dos anos 2000, afirma que o 3-SAT não pode ser resolvido em tempo subexponencial — o que significa que alguns quebra-cabeças lógicos comuns não podem ser resolvidos muito mais rápido do que testando todas as respostas possíveis na força bruta.
Como a hipótese foi amplamente aceita e usada em centenas de artigos para derivar resultados condicionais de dureza computacional em uma grande variedade de áreas, refutá-la invalidaria uma parcela significativa desses resultados e obrigaria os pesquisadores a reavaliar a dificuldade computacional de problemas em áreas como algoritmos, teoria dos grafos e biologia computacional.
A empresa de IA afirmou que seus modelos geraram a refutação em linguagem natural em 16 de outubro e a formalizaram no assistente de provas matemáticas Lean no dia seguinte; ambos os resultados estão disponíveis em um repositório público no GitHub.
A pesquisa está sendo analisada por um grupo externo liderado por Russell Impagliazzo e Ramamohan Paturi, da UC San Diego — dois dos proponentes originais da hipótese —, e Ryan Williams, do MIT, informou a OpenAI.
No X, Williams afirmou que os pesquisadores ainda estão tentando entender as implicações práticas da descoberta.
"No ritmo atual do progresso, é plausível que vejamos uma atualização significativa sobre a resolução prática do SAT nos próximos 12 meses. Ou talvez não vejamos nada parecido. Eu realmente não sei", disse Williams.
Separadamente, a Anthropic divulgou um artigo e uma formalização no Lean 4 afirmando que um algoritmo determinístico resolve o 3-SAT de uma maneira que refutaria a Hipótese do Tempo Exponencial. A empresa disse que um modelo interno de pesquisa Claude descobriu o algoritmo central em 16 de outubro — no mesmo dia em que os modelos da OpenAI fizeram a descoberta — usando 14 milhões de tokens de saída sem intervenção humana.
"O resultado é puramente assintótico e não diz nada sobre a resolução de fórmulas na prática", a Anthropic observou.
Enquanto isso, a OpenAI também revelou outros dois resultados gerados por IA: uma prova da conjectura do alisamento local em todas as dimensões na análise harmônica e uma prova matematicamente rigorosa da existência de certas teorias quânticas de campos, incluindo a Cromodinâmica Quântica e a teoria de Yang-Mills pura.
