Matemáticos passaram a questionar se os 719 manuscritos de matemática gerados por inteligência artificial pela OpenAI são realmente confiáveis, depois que um novo artigo apontou que a prova de Navier-Stokes divulgada pela empresa não coincide com a versão verificada por computador.
Principais pontos:
- O catálogo da OpenAI encolheu de 722 para 719 manuscritos após a empresa retirar três artigos por causa de um erro de sinal.
- Três matemáticos britânicos documentaram duas divergências entre a prova escrita de Navier-Stokes e o respectivo código em Lean.
- Os autores não afirmam que a prova está errada, mas ressaltam que checagens automatizadas não substituem a revisão por pares.
Lançamento do acervo de matemática da OpenAI
A empresa publicou a coleção em 6 de outubro, e uma reportagem divulgada na quinta-feira apontou que a iniciativa se afastou das diretrizes elaboradas por um painel independente de matemáticos para trabalhos de IA. O catálogo estreou com 722 manuscritos. A OpenAI retirou três deles no dia seguinte, depois que um erro de sinal derrubou um argumento e comprometeu outros dois artigos que dependiam desse resultado.
As diretrizes, publicadas em 29 de setembro pelo Advisory Group on Mathematics and Artificial Intelligence, formado por nove especialistas, começam com um pedido para que laboratórios parem de testar problemas avançados de matemática em modelos proprietários. O repositório da OpenAI afirma que os artigos resultam da avaliação de um modelo interno, ainda inédito, sobre problemas de pesquisa em aberto.
Resumos explicando o raciocínio do modelo acompanham apenas 10 resultados, e cerca de 42% dos teoremas principais foram formalizados em Lean, uma linguagem de programação que permite ao computador verificar a correção de uma prova.
Veja também: Quanto ganha o CEO da Anthropic? Prospecto de IPO revela o número
Lacunas na prova de Navier-Stokes
Alexander Bastounis, do King's College London, e Fabian Circelli e Anders Hansen, da Universidade de Cambridge, analisaram a prova de Navier-Stokes anunciada pela OpenAI em setembro. Eles identificaram dois pontos em que o argumento escrito e o código em Lean divergem, incluindo um caso em que o código demonstra apenas uma estimativa mais fraca do que a declarada no artigo.
Os autores enfatizam que não se pronunciam sobre a correção da prova escrita em si. O argumento deles é mais específico: o Lean confirma que o teorema final é verdadeiro, mas não consegue garantir que cada passo intermediário — aquele que um humano efetivamente lê — seja sólido. Por isso, defendem, essas provas seguem dependendo de revisão por pares.
O medalhista Fields Terence Tao escreveu, em 6 de outubro, que problemas estão sendo “resolvidos por prompters de IA” que não entendem o suficiente do resultado para responder perguntas ou apresentar palestras sobre o trabalho. A professora de Harvard Melanie Matchett Wood, integrante do grupo consultivo, observou que, quando esses resultados são divulgados, nenhum humano os compreende por completo — “e é aí que o trabalho começa”.
Disputa em torno das provas da OpenAI
O grupo consultivo já afirmou que apenas a comunidade matemática em geral pode avaliar quão fielmente a OpenAI seguiu suas recomendações. Esse escrutínio vem após um mês tenso. A OpenAI anunciou o resultado sobre Navier-Stokes em 8 de setembro, o que desencadeou uma disputa de crédito com o matemático da New York University Tristan Buckmaster. Três dias depois, 25 medalhistas Fields lançaram uma declaração alertando que a produção em massa de resultados por IA pode prejudicar o desenvolvimento da área.
Leia a seguir: Os 722 artigos de matemática da OpenAI estão públicos; agora cabe aos matemáticos julgá-los
