Google DeepMind abre o código do AlphaProof e leva verificação formal de matemática para a era dos LLMs
Sistema que resolveu problemas da Olimpíada Internacional de Matemática em 2024 tem código-fonte e pesos liberados, permitindo que pesquisadores acoplem modelos de linguagem a provadores formais como o Lean
Entenda o Cenário
- O AlphaProof resolveu problemas da Olimpíada Internacional de Matemática de 2024 combinando um modelo de linguagem com o provador formal Lean, gerando demonstrações verificáveis por máquina
- A liberação inclui código-fonte e pesos do sistema, permitindo que laboratórios acadêmicos e empresas auditem e estendam o pipeline de treinamento
- A verificação formal por Lean é usada para eliminar alucinações matemáticas: cada passo da prova é checado por um kernel independente antes de ser aceito
O Google DeepMind liberou o código-fonte e os pesos do AlphaProof, sistema que em 2024 resolveu problemas da Olimpíada Internacional de Matemática (IMO) ao acoplar um modelo de linguagem a um provador formal. A abertura coloca nas mãos da comunidade de pesquisa uma das arquiteturas mais influentes para o raciocínio automatizado verificável.
A decisão transforma o que era um experimento fechado de laboratório em infraestrutura aberta para universidades, startups e grupos independentes que trabalham com demonstrações matemáticas assistidas por máquina.
Como o sistema funciona na prática
O AlphaProof não gera texto solto: ele produz provas escritas na linguagem formal Lean, em que cada passo lógico é checado por um kernel independente. Se uma etapa não se sustenta, a prova é rejeitada — o que elimina boa parte das alucinações típicas de modelos de linguagem.
A arquitetura combina um modelo de linguagem que propõe estratégias de demonstração com um mecanismo de busca que testa e refina cada tentativa contra o verificador. O aprendizado ocorre por reforço, com o sistema acumulando provas válidas ao longo do treinamento.
Por que a verificação formal importa
A verificação por Lean virou um dos campos mais disputados da pesquisa em IA. Diferentemente de um chatbot que responde com confiança a uma equação errada, um sistema que escreve provas formais precisa convencer um verificador matemático — não um leitor humano.
Essa propriedade atrai interesse de laboratórios que buscam modelos confiáveis para engenharia de software, criptografia e descoberta científica, áreas em que um erro silencioso custa caro.
O que muda com o código aberto
Com o acesso ao código e aos pesos, pesquisadores podem reproduzir o pipeline de treinamento, adaptar o sistema a outros provadores formais e medir seu desempenho em benchmarks próprios. A abertura também permite auditar as escolhas de design do DeepMind.
O movimento segue a estratégia do laboratório de publicar artefatos de pesquisa em matemática formal, campo em que a verificação por máquina se tornou um padrão de qualidade científica.