FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

O artigo apresenta o FormalProofBench, um benchmark privado que avalia a capacidade de modelos de IA de gerar provas matemáticas de nível de pós-graduação formalmente verificadas no Lean 4, revelando que o melhor modelo testado alcança apenas 33,5% de precisão.

O essencial

Imagine que você tem um grupo de estudantes de matemática muito inteligentes (os modelos de IA) e quer saber se eles realmente entendem o que estão fazendo ou se apenas estão "adivinhando" de forma convincente.

O artigo "FormalProofBench" apresenta uma nova e rigorosa prova de fogo para essas IAs. Aqui está a explicação, traduzida para uma linguagem simples e cheia de analogias:

1. O Problema: A Ilusão da Competência

Até agora, testávamos a matemática das IAs com problemas de múltipla escolha ou respostas em texto livre (como "explique como resolver esta equação").

• A analogia: É como pedir para um aluno escrever uma redação sobre como construir uma ponte. Ele pode usar palavras bonitas, citar engenheiros famosos e parecer muito inteligente. Mas, se a ponte cair quando você tentar atravessá-la, a redação não serviu de nada.
• O risco: Uma IA pode inventar uma "prova" que soa lógica, mas que tem um erro sutil no meio. Humanos (e até outras IAs) muitas vezes não percebem esse erro porque o texto parece correto.

2. A Solução: O "Tribunal" Lean 4

Os autores criaram o FormalProofBench. Em vez de pedir uma redação, eles pedem para a IA escrever o código de uma prova matemática em uma linguagem chamada Lean 4.

• A analogia: Pense no Lean 4 como um inspetor de obras extremamente rigoroso e sem sentimentos. Ele não se importa com a beleza da frase ou com a confiança do engenheiro. Ele só verifica se cada peça da ponte encaixa perfeitamente.
• A regra de ouro: Se o código não "compilar" (se a ponte não ficar de pé), a resposta é considerada errada, ponto final. Não há meio-termo. Ou a prova é matematicamente perfeita e verificável, ou é lixo.

3. O Desafio: Nível de Pós-Graduação

Este não é um teste de matemática do ensino médio. Os problemas vêm de exames de qualificação para doutorado e livros avançados de tópicos como:

• Análise Real (o estudo de números e limites).
• Álgebra e Geometria Algébrica.
• Probabilidade e Teoria da Medida.
• A analogia: É como pedir para um estudante do ensino médio resolver um problema de física quântica que um professor universitário ainda está estudando. É difícil, complexo e exige conhecimento profundo.

4. Como o Teste Funciona (O "Agente")

As IAs não recebem apenas o problema; elas recebem uma "caixa de ferramentas" e 40 chances (turnos) para tentar resolver.

• As ferramentas:
  1. Pesquisa (Loogle): Para procurar teoremas existentes na biblioteca de matemática (como usar o Google para achar uma fórmula).
  2. Execução de Código (Lean Run): Para tentar escrever a prova, rodar o código e ver onde deu erro.
  3. Submissão: Para entregar a prova final.
• O processo: A IA tenta, o inspetor (Lean) diz "está errado aqui", a IA corrige, tenta de novo, pesquisa mais, e assim por diante, até conseguir ou esgotar as tentativas.

5. O Que Eles Descobriram?

Os pesquisadores testaram as IAs mais poderosas do mundo (como Claude, GPT-5, Gemini, etc.).

• O Resultado: Mesmo as IAs mais inteligentes do planeta tiveram um desempenho modesto. A melhor delas (Claude Opus 4.5) acertou apenas 33,5% dos problemas.
• A lição: A maioria das IAs ainda está muito longe de ser capaz de fazer matemática de nível de pós-graduação de forma totalmente confiável e verificada.
• O segredo do sucesso: As IAs que acertaram mais não foram as que mais pesquisaram no Google (Loogle). Foram aquelas que escreveram e testaram código repetidamente.
  • Analogia: É como aprender a cozinhar. Alguém que apenas lê receitas (pesquisa) erra muito. Alguém que coloca os ingredientes na panela, prova, vê que está salgado, ajusta e prova de novo (execução de código) é quem consegue fazer o prato perfeito.

6. Por Que Isso Importa?

Este teste é importante porque:

1. Não há "cola": Como o teste é privado e os problemas são formalizados especificamente para isso, as IAs não podem ter "decorado" as respostas na internet.
2. Verdadeira Verificação: Elimina a alucinação. Se a IA diz que provou algo, o computador confirma.
3. Futuro da Matemática: Se as IAs chegarem a um nível onde conseguem passar nesse teste com frequência, elas poderão se tornar parceiros reais para matemáticos, ajudando a provar teoremas complexos e acelerando a descoberta científica.

Resumo em uma frase:
O FormalProofBench é um exame final onde as IAs precisam construir pontes matemáticas sob a supervisão de um inspetor implacável; até agora, a maioria das pontes ainda cai, mas as que ficam de pé são construídas por quem testa e ajusta o código, não por quem apenas lê as instruções.

Resumo técnico

Resumo Técnico: FormalProofBench

1. O Problema

O avanço recente de Grandes Modelos de Linguagem (LLMs) em raciocínio matemático foi medido principalmente através de benchmarks de matemática em linguagem natural (como MATH, GSM8K ou AIME). No entanto, soluções em linguagem natural podem ocultar erros lógicos sutis que são difíceis de auditar, mesmo por revisores humanos ou outros LLMs. Um modelo pode gerar um argumento que soa plausível, mas omite casos críticos ou invoca lemas inexistentes.

Existe uma lacuna entre a competência matemática aparente e a competência verificada. Para preencher essa lacuna, é necessário um método de avaliação onde a correção seja binária e verificável por máquina: uma prova ou passa na verificação formal (type-checking) ou não. Além disso, a comunidade matemática tem adotado cada vez mais provadores de teoremas interativos (como Lean 4), mas faltam benchmarks rigorosos que avaliem se os modelos podem produzir provas formais verificáveis para matemática de nível avançado (graduação superior e pós-graduação).

2. Metodologia

O Benchmark (FormalProofBench):

• Objetivo: Avaliar a capacidade de modelos de IA de gerar provas matemáticas formais verificadas no nível de graduação avançada e pós-graduação.
• Estrutura das Tarefas: Cada tarefa consiste em:
  1. Um problema matemático em linguagem natural.
  2. A declaração formal correspondente em Lean 4 (incluindo cabeçalhos e contexto do Mathlib).
  3. O modelo deve gerar um termo de prova em Lean que seja aceito pelo kernel do Lean 4.
• Origem dos Dados: 200 problemas selecionados de exames de qualificação e livros-texto padrão.
• Domínios Matemáticos: Inclui análise real e funcional, álgebra e álgebra comutativa, geometria algébrica, teoria dos números, probabilidade/estocástica e lógica. A distribuição mais pesada é em Análise Real (56 problemas) e Teoria da Probabilidade (34 problemas).
• Garantia de Qualidade: Todos os formalismos foram escritos por especialistas (estudantes de doutorado e usuários experientes de Lean) e passaram por um processo de revisão secundária para evitar "misformalization" (declarações formais que não correspondem à intenção do problema natural). O benchmark é mantido privado para evitar contaminação dos dados de treinamento.

Ambiente de Avaliação (Agentic Harness):

• Configuração: Os modelos não geram a prova em uma única passada (one-shot). Eles operam em um ambiente de agente com até 40 turnos de interação por problema.
• Ferramentas Disponíveis:
  • lean_loogle: Ferramenta de busca para encontrar teoremas e definições no Mathlib.
  • lean_run_code: Permite executar código Lean, receber feedback de erros, tipos incompatíveis, metas não resolvidas e avisos.
  • submit_proof: Comando para submeter a prova final (iniciando com by).
• Critério de Sucesso: A prova deve compilar com sucesso no kernel Lean 4 (versão v4.25.2). O uso de axiomas locais ou sorry é rejeitado.

3. Principais Contribuições

1. Novo Benchmark Determinístico: Apresenta um benchmark desafiador, do mundo real, não contaminado e com avaliação determinística (compila ou não), eliminando a necessidade de graduação humana ou por modelo.
2. Avaliação de Nível de Pós-Graduação: É o primeiro a focar especificamente em problemas de nível de pós-graduação formalizados, indo além dos problemas de olimpíadas ou graduação básica.
3. Análise de Agentes Multiturno: Avalia modelos em um cenário realista de agente com ferramentas de busca e execução de código, permitindo até 40 iterações, em vez de apenas geração estática.
4. Análise de Custo e Latência: Fornece métricas detalhadas sobre o custo financeiro e o tempo de latência necessários para resolver esses problemas complexos.
5. Descoberta sobre Uso de Ferramentas: Identifica que a frequência de iteração via execução de código (lean_run_code) correlaciona-se fortemente com o sucesso, enquanto o uso excessivo de busca sem execução leva a falhas.

4. Resultados

O estudo avaliou modelos de ponta (Frontier Models) de provedores como Anthropic, OpenAI, Google, xAI, DeepSeek e Zhipu AI.

• Desempenho Geral:
  • O melhor modelo foi o Claude Opus 4.5 (Thinking), alcançando 33,5% de precisão.
  • Há uma queda acentuada de desempenho após o primeiro lugar. O segundo colocado (Gemini 3 Pro) atingiu 18,5%, e o terceiro (Claude Sonnet 4.5) 18,0%.
  • Modelos menores ou menos avançados (como GPT 5 Mini ou Grok 4.1 Fast) tiveram desempenho abaixo de 7-10%.
• Padrões de Uso de Ferramentas:
  • Modelos de alto desempenho tendem a executar código cedo para obter feedback imediato e usam a ferramenta de busca (lean_loogle) apenas para preencher lacunas específicas.
  • Modelos de baixo desempenho frequentemente entram em "espirais" de busca repetitiva tentando encontrar lemas inexistentes, sem executar o código para validar hipóteses.
• Custo e Latência:
  • O custo médio por teste variou de ~$0,10 a mais de $1,30.
  • A latência foi significativa, com médias de mais de uma hora por problema (ex: ~4000s para o Claude Opus 4.5), devido à natureza iterativa e complexa da geração de provas formais.

5. Significado e Implicações

• Validação da Competência Matemática: O benchmark demonstra que, embora os modelos tenham melhorado, ainda há uma grande lacuna entre a geração de argumentos plausíveis e a produção de provas formalmente corretas. A barreira de 33,5% indica que a automação completa de matemática de nível de pesquisa ainda não foi alcançada, mas estamos nos aproximando de um limiar de utilidade prática.
• Impacto na Prática Matemática: O sucesso em benchmarks como o FormalProofBench sugere que a IA pode se tornar uma ferramenta prática para matemáticos, permitindo a exploração rápida de estratégias de prova com feedback imediato de correção. Isso pode democratizar o acesso a métodos formais e acelerar a formalização de teoremas de pesquisa.
• Direções Futuras: O trabalho aponta para a necessidade de melhorar as interfaces de busca (atualmente o lean_loogle é menos eficaz que a execução de código), testar a ablação das declarações em linguagem natural para isolar a dificuldade de tradução vs. geração, e expandir o benchmark para teoremas de nível de pesquisa pura à medida que o Mathlib cresce.

Em resumo, o FormalProofBench estabelece um novo padrão ouro para avaliar a capacidade de raciocínio matemático de IA, focando na verificação rigorosa e na interação agêntica, revelando que a execução iterativa de código é a chave para o sucesso atual nesses sistemas.