Matemáticos passaram a questionar se os 719 manuscritos de matemática gerados por OpenAI merecem confiança, após a publicação de um artigo que afirma que a anterior prova de Navier–Stokes anunciada pela empresa não coincide com a versão verificada por computador.
Pontos-chave:
- O catálogo da OpenAI encolheu de 722 para 719 manuscritos depois que a empresa retirou três artigos devido a um erro de sinal.
- Três matemáticos sediados no Reino Unido documentaram duas discrepâncias entre a versão escrita da prova de Navier–Stokes e o respetivo código em Lean.
- Os autores não afirmam que a prova esteja errada, 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 uma reportagem divulgada na quinta‑feira apontou que o projeto se afasta das diretrizes definidas por um painel independente de matemáticos para laboratórios de IA. O catálogo estreou com 722 manuscritos. A OpenAI retirou três deles no dia seguinte, depois de um erro de sinal comprometer um argumento e dois artigos que dele dependiam.
As diretrizes, divulgadas em 29 de setembro pelo Advisory Group on Mathematics and Artificial Intelligence, composto por nove membros, começam com um apelo para que os laboratórios deixem de testar problemas avançados de matemática em modelos proprietários. O repositório da OpenAI informa que os artigos resultam da avaliação de um modelo interno, ainda inédito, em problemas de pesquisa em aberto.
Apenas 10 resultados contam com resumos do raciocínio seguido pelo modelo, e cerca de 42% dos principais teoremas foram formalizados em Lean, uma linguagem de programação que permite a verificação automática de provas por computador.
Leia também: Quanto ganha o CEO da Anthropic? O prospecto 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 anunciou em setembro. Eles documentaram 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 enunciada no artigo.
Os autores dizem não se pronunciar sobre a correção ou não da prova escrita. O alvo é mais restrito: segundo eles, o Lean confirma que o teorema final é verdadeiro, mas não garante que os passos intermédios — aqueles que um humano de facto lê — 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 problemas estão a ser resolvidos por “prompters de IA” que não compreendem o resultado a fundo o suficiente para responder a perguntas ou fazer palestras sobre o tema. A professora de Harvard Melanie Matchett Wood, membro do grupo consultivo, afirmou que, quando tais resultados são divulgados, “nenhum humano os entende integralmente — e é aí que o trabalho começa”.
Disputa em torno da prova da OpenAI
O grupo consultivo afirma que apenas a comunidade matemática em geral pode avaliar até que ponto a OpenAI seguiu, ou não, as recomendações. Esse escrutínio vem na sequência de um mês tenso. A OpenAI anunciou o resultado em Navier–Stokes em 8 de setembro, o que desencadeou uma disputa de crédito com o matemático da Universidade de Nova Iorque Tristan Buckmaster; três dias depois, 25 medalhistas Fields divulgaram uma declaração alertando que resultados produzidos em massa por IA podem prejudicar o desenvolvimento da área.
Próxima leitura: Os 722 artigos de matemática gerados por IA da OpenAI já são públicos; agora cabe aos matemáticos julgá-los
