O Google DeepMind desenvolveu o AlphaProof, um sistema de IA que igualou o desempenho de medalha de prata na Olimpíada Internacional de Matemática de 2024, pontuando 28 de 42 pontos. O sistema ficou a apenas um ponto do ouro na competição de matemática para graduandos mais prestigiada do mundo. Este avanço demonstra progressos na capacidade da IA de lidar com provas matemáticas complexas.
Os computadores há muito se destacam em cálculos, mas lutam com o raciocínio lógico necessário para a matemática avançada. A nova IA do Google DeepMind, AlphaProof, aborda isso ao alcançar o desempenho de medalhista de prata na Olimpíada Internacional de Matemática de 2024 (IMO), a principal competição de matemática no nível do ensino médio. A IMO incluiu seis problemas valendo sete pontos cada, totalizando 42 pontos. As medalhas de ouro exigiam 29 pontos ou mais, alcançadas por 58 de 609 participantes, enquanto a prata foi para aqueles com 22-28 pontos, com 123 destinatários. O AlphaProof pontuou 28 pontos, resolvendo quatro problemas de forma independente para 21 pontos e recorrendo ao AlphaGeometry 2 especializado para o problema de geometria para atingir o nível de prata.
O desenvolvimento do AlphaProof começou superando a limitada disponibilidade de dados de treinamento para provas matemáticas formais. A equipe usou o software Lean, uma ferramenta para definições e verificações matemáticas precisas. Para expandir o conjunto de dados, treinaram um modelo de linguagem grande Gemini para traduzir declarações matemáticas em linguagem natural para Lean, gerando cerca de 80 milhões de declarações formalizadas. Como explicou Thomas Hubert, pesquisador da DeepMind e autor principal, “A principal dificuldade de trabalhar com linguagens formais é que há muito poucos dados.” Apesar das imperfeições, “Há muitas maneiras de capitalizar traduções aproximadas,” ele acrescentou.
A arquitetura do sistema é inspirada no AlphaZero da DeepMind, combinando uma rede neural treinada por tentativa e erro com um algoritmo de busca em árvore para explorar caminhos de prova. Ela recompensa provas corretas e penaliza passos ineficientes, promovendo soluções elegantes. Uma adição nova, Test-Time Reinforcement Learning (TTRL), permite que o AlphaProof gere variações de problemas difíceis para treinamento em tempo real, imitando a resolução de problemas humanos. “Estávamos tentando aprender esse jogo por tentativa e erro,” disse Hubert.
No entanto, o AlphaProof exigiu assistência humana para formalizar problemas no Lean e levou vários dias por problema desafiador, consumindo centenas de dias-TPU—muito além dos limites de tempo humanos de 4,5 horas por sessão. Apenas seis humanos resolveram o problema mais difícil; o AlphaProof foi o sétimo. A DeepMind reconhece os altos custos computacionais, mas visa otimizar para uso mais amplo. “Não queremos parar em competições de matemática. Queremos construir um sistema de IA que possa realmente contribuir para a matemática em nível de pesquisa,” afirmou Hubert. A equipe planeja um programa de testadores confiáveis para compartilhar uma ferramenta AlphaProof com matemáticos.
O trabalho é detalhado em um artigo da Nature de 2025 (DOI: 10.1038/s41586-025-09833-y).