Matemáticos dizem que prova gerada por IA da OpenAI é ‘quase incompreensível’

Principais destaques

• Uma prova de 166 páginas: agentes de IA da OpenAI produziram um trabalho sobre Navier-Stokes que, se confirmado, resolveria um dos Problemas do Milênio.
• O problema não é só provar: matemáticos dizem que o material é extremamente difícil de transformar em conhecimento compreensível para humanos.
• OpenAI criou um novo painel: um grupo com matemáticos de elite terá como primeira tarefa ajudar a organizar a divulgação de mais de 100 resultados matemáticos atribuídos ao novo modelo.

A inteligência artificial pode ter chegado a um ponto curioso da matemática: conseguir produzir uma prova que computadores conseguem verificar, mas que humanos têm dificuldade de compreender.

É justamente essa situação que está provocando uma discussão entre matemáticos após a OpenAI divulgar resultados envolvendo o problema de Navier-Stokes.

O caso é particularmente importante porque não estamos falando de um exercício de olimpíada ou de uma conjectura obscura.

Estamos falando de um dos seis Problemas do Milênio, estabelecidos pelo Instituto Clay de Matemática, com prêmio de US$ 1 milhão para cada solução correta.

10 mil agentes, 88 horas e 166 páginas 🤯

Segundo o material fornecido, a OpenAI colocou cerca de 10.000 agentes de IA para trabalhar durante aproximadamente 88 horas.

O resultado foi uma prova de 166 páginas relacionada às equações de Navier-Stokes.

A questão central é descobrir se soluções dessas equações, usadas para descrever o comportamento de fluidos, podem desenvolver uma singularidade em tempo finito.

Se o resultado for validado nos termos necessários para resolver o problema do Instituto Clay, seria um feito histórico para a matemática.

🔎 Mas existe uma diferença importante: uma prova matematicamente verificável não é necessariamente uma prova que os seres humanos conseguem compreender facilmente.

E é justamente aí que começa a polêmica.

“Até agora, tem sido muito difícil extrair qualquer entendimento humano dessa nova prova de IA.”

A avaliação é de James Maynard, matemático da Universidade de Oxford, segundo a NPR.

O computador entende. E o matemático? 🧠

Uma das características mais interessantes do trabalho é a utilização de Lean, uma linguagem usada para verificação formal de provas matemáticas.

Em termos simplificados, isso permite que determinadas etapas sejam verificadas mecanicamente.

É uma diferença enorme em relação a simplesmente pedir para um chatbot escrever uma prova e confiar que os passos estão corretos.

Mas a verificação formal não resolve outro problema: entender por que a prova funciona e o que ela revela sobre a matemática por trás dela.

Javier Gómez-Serrano, matemático da Universidade Brown, afirmou que o trabalho poderia beneficiar a área depois de uma “reescrita séria”, mas que, até aquele momento, o artigo não havia proporcionado muito conhecimento novo aos matemáticos.

📝 A questão é quase filosófica: se uma máquina encontra uma demonstração válida, mas ninguém consegue extrair dela uma explicação humana, o que exatamente aprendemos?

A matemática sempre foi sobre mais do que estar certo

Uma prova não serve apenas para dizer “sim” ou “não”.

Ela também pode mostrar por que determinada afirmação é verdadeira, quais estruturas estão por trás dela e se a técnica pode ser utilizada em outros problemas.

Esse aspecto é particularmente importante na matemática contemporânea.

Uma demonstração pode ser gigantesca e ainda assim ser valiosa. Mas existe uma diferença entre uma prova longa e uma prova cuja estrutura é tão difícil de interpretar que os próprios especialistas têm dificuldade para identificar suas ideias centrais.

Foi esse ponto que chamou a atenção de pesquisadores.

E ainda apareceu uma disputa por crédito 👀

A controvérsia não ficou restrita à legibilidade.

O matemático Tristan Buckmaster, da Universidade de Nova York, acusou a OpenAI de ter utilizado pesquisa inédita relacionada ao seu trabalho sem atribuição adequada.

Segundo o relato apresentado, Buckmaster afirmou que a OpenAI chegou a oferecer sua inclusão como autor, desde que ele abrisse mão de seu colaborador Levent Alpöge, pesquisador da Anthropic.

A OpenAI negou ter utilizado diretamente o trabalho de Buckmaster.

Ao mesmo tempo, reconheceu uma possibilidade mais difícil de eliminar: dados anonimizados derivados da utilização de seus produtos por pesquisadores poderiam ter contribuído para o aprimoramento dos modelos.

Isso transforma a discussão sobre autoria em algo ainda mais complicado.

Se um sistema de IA foi treinado com enormes quantidades de conhecimento matemático produzido por humanos, onde termina a contribuição do modelo e começa a contribuição dos pesquisadores que construíram aquele conhecimento?

Agora a OpenAI quer colocar matemáticos na conversa 🧮

Em 21 de setembro, a OpenAI anunciou um Grupo Consultivo Independente sobre Matemática e Inteligência Artificial, sediado no Institute for Advanced Study, em Princeton.

O grupo tem nove integrantes e reúne pesquisadores de algumas das principais instituições acadêmicas do mundo, incluindo vencedores da Medalha Fields.

A proposta é justamente criar uma ponte entre o desenvolvimento de IA e a comunidade matemática.

Segundo a OpenAI, os integrantes poderão questionar a empresa, fazer recomendações não solicitadas e até controlar a própria composição do grupo.

A empresa também afirma que o grupo não será responsável por aconselhar sobre a condução de seu progresso interno em matemática.

O primeiro trabalho já é gigantesco 🚀

O novo painel não chega diante de uma folha em branco.

Junto com o anúncio, a OpenAI afirmou que o mesmo modelo ainda não lançado resolveu mais de 100 problemas matemáticos abertos de longa data, abrangendo diversas áreas da matemática.

A coordenação da divulgação desses resultados será a primeira prioridade do grupo.

Martin Hairer, vencedor da Medalha Fields e integrante do painel, explicou que a iniciativa surgiu em parte porque laboratórios de IA vêm produzindo resultados matemáticos de grande repercussão cuja publicação e divulgação estão muito abaixo do padrão esperado pela comunidade.

Mas Hairer também fez um alerta sobre a relação entre ciência e comunicação corporativa.

Ele afirmou que seria ingênuo acreditar que laboratórios de IA não tentarão apresentar as declarações do grupo de maneira que favoreça suas próprias estratégias de relações públicas.

“Torre de marfim”? 🏛️

A composição do painel também já provocou questionamentos.

Francesco Fournier-Facio, professor da Heriot-Watt, classificou a iniciativa como algo que “parece uma torre de marfim”.

Simon Machado, pesquisador da ETH Zurique, questionou como os integrantes foram escolhidos e descreveu o processo como envolto em mistério.

Essas críticas não significam necessariamente que o grupo não possa contribuir para a área. Elas apontam para outra questão: quem representa a matemática quando empresas de IA passam a produzir resultados em escala que a comunidade acadêmica precisa acompanhar?

A resposta ainda está sendo construída.

A próxima prova pode ser ainda mais estranha

O episódio de Navier-Stokes expõe um desafio que provavelmente vai ficar maior conforme os modelos se tornam melhores em matemática.

Até agora, a expectativa era que a IA ajudasse matemáticos a encontrar ideias, testar conjecturas ou automatizar cálculos.

Agora surge uma possibilidade diferente: a máquina pode chegar primeiro a resultados que os próprios especialistas ainda não sabem explicar de maneira satisfatória.

Isso muda o papel do matemático.

Em vez de apenas verificar se uma resposta está correta, será necessário também descobrir como transformar uma demonstração produzida por máquinas em conhecimento que outras pessoas possam compreender, questionar e utilizar.

A prova pode estar lá. O computador pode conseguir verificá-la.

Mas, para a matemática, talvez a parte mais interessante ainda seja descobrir o que aquela prova está tentando dizer.