Nove provas da DeepMind enfrentam teste de novidade

Uma demonstração matemática pode ser elegante e, ainda assim, esconder uma lacuna que ninguém deteta durante anos. O agente de inteligência artificial AlphaProof Nexus, da Google DeepMind, produziu provas para nove problemas propostos por Paul Erdős, e um programa informático verificou cada passo. O trabalho foi divulgado primeiro num pré-publicação de maio (arXiv) e publicado, depois de revisão por pares, na Science, a 8 de outubro (Science). O programa podia confirmar a lógica; saber se essa lógica trazia algo de novo ficou a cargo dos matemáticos.

Um árbitro que não se deixa convencer pelo estilo

Os chatbots são bons a escrever matemática que parece correta. Um parágrafo confiante pode disfarçar um passo em falta, que só uma leitura atenta deteta. O AlphaProof Nexus evita esse problema trabalhando em Lean, uma linguagem de programação que permite formular definições, afirmações e provas com precisão suficiente para serem verificadas por um computador.

Lean funciona como um árbitro que lê cada linha de uma demonstração e aplica regras fixas. O estilo não conta: se um passo não decorrer dos anteriores, a prova falha, por mais elegante que seja o resto.

A equipa descreve o agente como um sistema que procura provas escritas em Lean. Os investigadores também lhe deram acesso ao AlphaProof, um sistema anterior da DeepMind, desenvolvido especificamente para demonstrações. Nos testes da equipa, uma configuração mais simples chegou aos mesmos resultados: um modelo de linguagem combinado com Lean, sem o AlphaProof, também obteve as nove provas de Erdős (The Decoder). Para estes problemas, o componente especializado não foi necessário.

O artigo apresenta provas aceites para as nove afirmações de Erdős e para 44 conjecturas — afirmações que se julga serem verdadeiras, mas que ainda não foram demonstradas — da Online Encyclopedia of Integer Sequences, um vasto catálogo de padrões numéricos (Science). Entre os resultados de Erdős está uma pergunta com duas partes sobre números inteiros, proposta por Erdős e András Sárközy em 1970. Permaneceu em aberto durante mais de meio século (ABC).

O que o árbitro não consegue ver

A garantia de Lean tem um limite preciso: confirma que uma prova demonstra exatamente a afirmação tal como foi escrita em código. Ficam de fora três perguntas: se o código exprime aquilo que Erdős queria dizer, se alguém já tinha respondido à pergunta há muito tempo e se a resposta ensina alguma coisa.

O problema de 1970 mostra por que razão as duas últimas perguntas importam. A segunda parte implica a primeira, pelo que uma única prova resolve ambas. Depois de as provas do agente terem circulado, descobriu-se que uma pequena alteração a uma construção do artigo original de 1970 também respondia às duas partes (arXiv). As provas do agente estavam corretas; o problema é que estava mais perto de estar resolvido do que sugeria a classificação de «em aberto».

Detetar casos destes exige especialistas que conheçam a área. Gergely Bérczi, matemático da Universidade de Aarhus, na Dinamarca, e um dos autores do artigo, ajudou a escolher problemas adequados e a validar as soluções (Aarhus University). Também ajudou a preparar versões das provas que os leitores humanos conseguem acompanhar. Lean confirmou cada passo; Bérczi e os colegas avaliaram o que esses passos demonstravam no conjunto.

Esta divisão de trabalho distingue o estudo de um marco anunciado no mês passado. Nessa ocasião, o Claude, da Anthropic, converteu para Lean uma demonstração já conhecida do Último Teorema de Fermat (To Brief). Traduzir uma prova célebre não levanta dúvidas sobre a novidade. Procurar respostas entre afirmações tratadas como problemas em aberto levanta; nesse caso, verificar a novidade torna-se a tarefa principal.

A equipa publicou os ficheiros das provas, para que outros possam submetê-los ao mesmo árbitro (GitHub). O avanço demonstrado pelo estudo é concreto: um agente de inteligência artificial produziu provas verificáveis por computador para algumas afirmações que os matemáticos consideravam em aberto, e a garantia aplica-se às afirmações tal como foram escritas em Lean. Coube aos matemáticos que as leram determinar o que cada prova acrescentava à matemática.