OpenAI derruba hipótese central da computação com IA avançada

Inteligência Artificial

Novos avanços da OpenAI desafiam conceitos fundamentais da computação e impulsionam pesquisas em matemática e física.

Leia também: SAP lança IA avançada para agentes Joule e modelo na ISS hoje

A OpenAI afirma que seus modelos internos de inteligência artificial produziram provas matemáticas que derrubam a Hipótese do Tempo Exponencial (ETH), um dos pilares da ciência da computação teórica, e ainda apontam avanços relevantes em matemática e física. As demonstrações estão em revisão por especialistas externos e foram traduzidas para a linguagem Lean, permitindo checagem formal computadorizada passo a passo.

O que a OpenAI afirma ter provado

Segundo a empresa, três resultados centrais foram obtidos por seus modelos: uma prova de que a ETH é falsa, um avanço em uma conjectura fundamental sobre ondas em matemática e um resultado em física teórica ligado à base matemática de certas teorias de campos quânticos. A OpenAI descreve os manuscritos como “dados brutos de pesquisa”, que ainda precisam ser completamente entendidos pela comunidade científica.

No caso da ciência da computação, o alvo é a Exponential Time Hypothesis, que há anos serve de base para estimar a dificuldade do problema da satisfatibilidade booleana, o SAT. Esse problema pergunta se existe uma forma de atribuir verdadeiro ou falso a cada variável de uma fórmula lógica para que o resultado final seja verdadeiro. O número de possibilidades explode à medida que as variáveis crescem: com 100 variáveis, já se fala em um número de combinações com 31 dígitos.

A ETH sustenta, em essência, que não existe atalho real para o pior caso do SAT: mesmo com truques e otimizações, o tempo de execução cresce exponencialmente com o número de variáveis. Essa crença é usada como alicerce em centenas de artigos que mostram, por exemplo, que certos problemas não podem ser resolvidos mais rápido do que um certo limite, desde que a ETH seja verdadeira.

A OpenAI agora sustenta que suas provas mostram que essa hipótese é falsa. “Se a prova se confirmar, centenas de trabalhos que dependem da ETH perderiam sua base”, afirma a empresa. Esses estudos não se tornariam automaticamente errados, mas deixariam de ter uma demonstração garantida.

Entenda o contexto

O SAT é um caso clássico na teoria da complexidade: é fácil verificar se uma solução funciona, mas encontrar uma solução é considerado difícil. Ele está no centro da discussão sobre a relação entre os conjuntos de problemas P e NP e serve de referência para milhares de outros desafios computacionais. Na prática, versões do SAT são atacadas todos os dias por programas especializados, os chamados SAT solvers, usados para checar projetos de chips e testar softwares críticos, muitas vezes lidando com fórmulas com milhões de variáveis.

Mesmo assim, esses sistemas exploram estruturas específicas dos problemas reais e, em geral, não encaram os piores casos abstratos tratados por hipóteses como a ETH. Por isso, um colapso teórico dessa hipótese não se traduz automaticamente em ganho imediato de desempenho nas ferramentas atuais, mas reabre todo o mapa das possibilidades de algoritmos mais rápidos.

Quais especialistas vão revisar a suposta refutação da ETH?

A revisão independente envolve alguns dos nomes mais diretamente ligados à própria ETH. O professor Ryan Williams, do MIT, e os pesquisadores Russell Impagliazzo e Ramamohan Paturi, ambos da Universidade da Califórnia em San Diego, aceitaram o convite para atuar como revisores externos do resultado em ciência da computação. Eles estão trabalhando sem acordo de confidencialidade e planejam divulgar conclusões intermediárias ao longo do processo.

Impagliazzo reforça que a participação não significa aval antecipado. “Nossa participação não é um endosso imediato; resultados dessa magnitude precisam de revisão independente cuidadosa”, afirma. A postura cautelosa ecoa o tom de Williams, que também evita projeções otimistas sobre uso imediato em código do dia a dia.

Questionado sobre o que programadores comuns poderiam notar primeiro, Williams responde com franqueza sobre a incerteza: “É plausível que vejamos progresso sério na resolução prática de SAT dentro de 12 meses. Ou talvez nada disso aconteça. Eu realmente não sei.”

Entenda o contexto

Uma eventual comprovação da refutação da ETH teria impacto profundo na teoria da complexidade de circuitos, que estuda o que pode ou não ser feito com redes de portas lógicas simples (AND, OR, NOT). Segundo Williams, dos argumentos apresentados pela OpenAI seguiria que certas classes de problemas extremamente exigentes não podem ser resolvidas por circuitos “pequenos” — aqueles cujo tamanho cresce, no máximo, proporcionalmente ao tamanho da entrada. Isso reorganizaria fronteiras conhecidas entre o que é tratável com recursos limitados e o que exige estruturas mais complexas.

Como a OpenAI está usando Lean para checar as provas?

Para tentar aumentar a confiança nos resultados, a OpenAI traduziu as provas em matemática e ciência da computação para Lean, uma linguagem de programação focada em verificação formal. Nela, cada passo lógico é codificado de modo que um computador possa checar se a conclusão decorre corretamente das premissas.

A empresa, porém, faz uma ressalva importante sobre o alcance dessa validação automática. “Lean verifica se a prova estabelece a afirmação como está escrita, mas especialistas devem confirmar se a formulação do problema está correta”, explica a OpenAI. Em outras palavras, o verificador formal garante a correção interna da dedução, mas não substitui o julgamento humano sobre se o enunciado formal realmente captura o problema matemático ou computacional pretendido.

Atendendo a pedidos dos revisores, a OpenAI publicou todo o material bruto: textos das provas, arquivos em Lean e demais dados usados na geração dos resultados. A empresa também se comprometeu a financiar um congresso científico dedicado a discutir as implicações do possível colapso da ETH e dos demais avanços anunciados.

Entenda o contexto

O uso de verificadores formais como o Lean vem se consolidando como um novo padrão de rigor em matemática e áreas correlatas. Ao exigir que cada passo da prova seja explicitado de forma que um computador possa conferir, esse tipo de ferramenta reduz o risco de erros sutis e torna mais fácil para outros pesquisadores inspecionarem, reutilizarem e estenderem resultados complexos. Se o processo liderado pela OpenAI for bem-sucedido, tende a reforçar a combinação entre criatividade de sistemas de IA, validação formal por máquina e escrutínio crítico de especialistas humanos como um modelo de produção de ciência de ponta.

Que impacto a queda da ETH pode ter na prática?

Na teoria, uma refutação sólida da ETH abre espaço para algoritmos mais rápidos para problemas antes considerados intratáveis em seus piores casos, incluindo o próprio SAT. Isso mexe com áreas que dependem de limites de complexidade bem estabelecidos, como grafos, biologia computacional, bancos de dados e geometria computacional, que ao longo dos anos passaram a basear suas garantias na validade da ETH. “Se a prova se confirmar, centenas de trabalhos que dependem da ETH perderiam sua base”, reforça a OpenAI.

Na prática, porém, o efeito imediato é incerto. Os SAT solvers atuais já conseguem lidar com instâncias gigantes de problemas do mundo real, com milhões de variáveis, justamente porque exploram padrões específicos que fogem do pior caso abstrato. Um novo algoritmo que só melhora esse pior caso pode levar tempo até ser adaptado e demonstrar vantagens concretas em aplicações como verificação de chips, análise de vulnerabilidades de software e otimização de sistemas complexos.

Ainda assim, especialistas não descartam mudanças em horizonte relativamente curto. Williams avalia que, mantido o ritmo atual de pesquisa, não é irrealista ver “progresso sério” em solvers práticos em até 12 meses, ainda que admita que também é possível que nada se traduza tão rápido em benefício visível para desenvolvedores.

Outros dois resultados: matemática e física

Além da ETH, a OpenAI diz ter avançado sobre uma conjectura central da teoria de ondas em matemática, ligada à forma como vibrações de som, luz ou terremotos podem se concentrar e depois se espalhar ao longo do tempo. O resultado, segundo a empresa, valeria não apenas em superfícies bidimensionais, mas em qualquer número de dimensões, com consequências em outras duas conjecturas conhecidas de geometria e análise de Fourier.

No campo da física teórica, a empresa afirma que seus modelos produziram uma prova de existência matemática para certas teorias de campos quânticos em quatro dimensões, nas quais partículas interagem entre si. Entre elas está uma formulação da chamada teoria de Yang-Mills, que descreve o comportamento de partículas mediadoras da força forte, responsável por manter prótons e nêutrons coesos no núcleo atômico.

Essa teoria está ligada a um dos problemas do prêmio de um milhão de dólares proposto por uma instituição internacional de matemática. A OpenAI destaca, porém, que o resultado apresentado cobre apenas a parte de existência da teoria, sem resolver outra peça central do desafio, conhecida como “mass gap”. Um laureado com Nobel, convidado pela empresa, está entre os cientistas que acompanham a revisão desse trabalho.

Em todos os casos, o clima predominante na comunidade científica é de cautela. Se validado, o pacote de provas produzidas por IA tem potencial para remodelar trechos importantes da ciência da computação, da matemática e da física. Se falhar, ainda assim deve servir como laboratório para entender melhor os limites e as possibilidades da colaboração entre sistemas de inteligência artificial, verificadores formais e especialistas humanos na fronteira do conhecimento.