Matemáticos começam a questionar a fiabilidade dos 719 manuscritos matemáticos gerados por OpenAI, após a publicação de um artigo que sustenta que a anterior prova de Navier-Stokes da empresa não coincide com a sua versão verificada por computador.
Pontos-chave:
- O catálogo da OpenAI encolheu de 722 para 719 manuscritos depois de a empresa retirar três artigos devido a um erro de sinal.
- Três matemáticos sediados no Reino Unido documentaram duas divergências entre a prova escrita de Navier-Stokes e o respetivo código em Lean.
- Os autores não dizem que a prova é falsa, mas defendem que verificações automáticas não substituem a revisão por pares.
Lançamento do pacote de matemática da OpenAI
A empresa publicou a coleção em 6 de outubro, e um relatório divulgado na quinta-feira concluiu que o projeto se afastou das diretrizes elaboradas por um painel independente de matemáticos para laboratórios de IA. O catálogo foi lançado com 722 manuscritos. A OpenAI retirou três deles no dia seguinte, depois de um erro de sinal ter invalidado um argumento e, em cascata, outros dois artigos que dele dependiam.
Essas diretrizes, publicadas a 29 de setembro pelo Advisory Group on Mathematics and Artificial Intelligence, composto por nove membros, começam por pedir aos laboratórios que deixem de testar problemas avançados de matemática em modelos proprietários. O repositório da OpenAI indica que os artigos resultam da avaliação de um modelo interno, ainda não lançado, em problemas de investigação em aberto.
Resumos do raciocínio do modelo acompanham apenas 10 resultados, e cerca de 42% dos resultados de primeira linha foram formalizados em Lean, uma linguagem de programação que permite ao computador verificar uma prova.
Veja também: Quanto ganha o CEO da Anthropic? O prospeto do IPO traz a resposta
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 que a OpenAI anunciara em setembro. Identificaram dois pontos em que o argumento escrito e o código em Lean divergem, incluindo um caso em que o código estabelece apenas uma estimativa mais fraca do que a apresentada no artigo.
Os autores sublinham que não fazem qualquer afirmação sobre a correção ou não da prova escrita. A sua crítica é mais cirúrgica: o Lean confirma que o teorema final é válido, escrevem, mas não garante que os passos intermédios lidos por um humano sejam sólidos; por isso, mesmo provas formalizadas continuam a exigir revisão por pares.
O medalhista Fields Terence Tao escreveu, em 6 de outubro, que alguns problemas estão a ser “resolvidos por prompters de IA” que não compreendem suficientemente o resultado para responder a perguntas ou apresentar seminários sobre o trabalho. A professora de Harvard Melanie Matchett Wood, membro do grupo consultivo, observou que, quando estes resultados são divulgados, “nenhum humano os entende por completo — e é aí que o verdadeiro trabalho começa”.
Disputa em torno da prova da OpenAI
O grupo consultivo tem insistido que apenas a comunidade matemática alargada pode avaliar até que ponto a OpenAI cumpriu as suas recomendações. Esse escrutínio surge após um mês conturbado. A OpenAI anunciou o resultado em Navier-Stokes a 8 de setembro, desencadeando uma disputa de atribuição de crédito com o matemático da Universidade de Nova Iorque Tristan Buckmaster. Três dias depois, 25 medalhistas Fields lançaram uma declaração alertando que resultados produzidos em massa por IA podem prejudicar o desenvolvimento da disciplina.
Leia a seguir: Os 722 artigos de matemática gerados por IA da OpenAI são públicos; agora cabe aos matemáticos julgá-los
