Benchmarking Testing in Automated Theorem Proving

1. Formulação do Problema

O avanço rápido dos Modelos de Linguagem de Grande Escala (LLMs) melhorou sua capacidade de gerar provas formais em sistemas como o Lean. No entanto, os métodos de avaliação atuais sofrem de uma falha crítica: eles confundem validade sintática com correção semântica.

• A Limitação da Compilação: Benchmarks existentes (por exemplo, MiniF2F, ProofNet) avaliam principalmente os modelos verificando se um teorema gerado compila. Embora a compilação verifique que o código é sintaticamente válido e logicamente consistente isoladamente, ela não garante que o teorema capture o significado matemático pretendido.
• O Problema da "Tautologia": Um modelo pode gerar uma tautologia trivial (por exemplo, $a + b = a + b$) que compila com sucesso, mas falha em provar a afirmação não trivial pretendida (por exemplo, a comutatividade $a + b = b + a$).
• Insuficiência de Proxies: As tentativas existentes de medir a correção semântica dependem de proxies não confiáveis, como sobreposição léxica (pontuações BLEU) contra referências anotadas manualmente ou inspeção humana. Esses métodos são ou ruidosos, exigem trabalho humano dispendioso ou falham em distinguir entre significados semânticos corretos e incorretos.

2. Metodologia

Os autores propõem uma mudança de paradigma inspirada em testes de integração na engenharia de software. Em vez de avaliar um teorema isoladamente, eles o avaliam com base em como ele interage com o restante da base de código.

Conceito Central: Teste de Teoremas (T2)

Baseando-se na correspondência de Curry-Howard (onde provas correspondem a programas), os autores tratam um teorema gerado como uma função e os teoremas que dependem dele como "casos de teste".

• Grafo de Dependência: Eles constroem um grafo de dependência onde um teorema-alvo ($t_{GT}$) possui predecessores (definições/lemas que utiliza) e sucessores (teoremas que invocam ou constroem sobre ele).
• Lógica de Teste de Integração: Se um teorema gerado ($t_{fl}$) for semanticamente incorreto (por exemplo, se definir uma tautologia em vez da propriedade pretendida), qualquer teorema sucessor que dependa dele falhará ao compilar.
• Analogia da Eliminação de Corte: O processo é formalmente fundamentado no princípio lógico de Eliminação de Corte. Se uma cadeia de provas ($X \to Y \to Z \to W$) falhar quando o lema intermediário ($Y$) é substituído por um candidato gerado, o candidato é semanticamente incorreto.

O Benchmark T2

Os autores construíram um benchmark de grande escala, o T2, para facilitar essa avaliação:

• Fonte: Extraído de 5 repositórios reais do Lean 4 (abrangendo álgebra, topologia, teoria dos números, etc.).
• Escala: 2.206 problemas, cada um emparelhado com uma média de 41 teoremas sucessores.
• Subconjunto Difícil: Um subconjunto de 389 problemas "Difíceis" onde o modelo deve gerar tanto a proposição (afirmação) quanto a prova, em vez de apenas preencher uma prova para uma afirmação dada.
• Automação: O pipeline de extração é totalmente automatizado, não exigindo anotação humana para a estrutura de dependência. Descrições em linguagem natural (NL) foram geradas por um LLM forte (Claude Sonnet 4.5) e verificadas manualmente para uma amostra.

A Métrica: Precisão de Teste (TA)

O artigo introduz a Precisão de Teste (TA) como a métrica de avaliação primária:
$$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compila}(t^{(i)}_{succ} \mid t_{fl}) \right]$$
Um teorema gerado passa apenas se todos os seus teoremas sucessores dependentes compilarem com sucesso quando o teorema original é substituído pelo gerado.

3. Principais Contribuições

1. Benchmark T2: O primeiro benchmark de grande escala e rico em dependências para prova formal de teoremas que vai além de problemas isolados para contextos de repositórios do mundo real.
2. Precisão de Teste (TA): Uma métrica nova, automática e livre de referências que verifica diretamente a correção semântica através da compilação de módulos dependentes.
3. Análise de Lacuna Empírica: Avaliação abrangente de 18 modelos de última geração (tanto de código aberto quanto fechados), revelando uma desconexão massiva entre sucesso na compilação e correção semântica.
4. Insights Contextuais: Demonstrou que fornecer teoremas sucessores como contexto melhora significativamente a correção semântica, enquanto fornecer apenas provas em linguagem natural não o faz.

4. Resultados Experimentais

Os autores avaliaram 18 modelos (incluindo GPT-5, Claude-Sonnet-4.5, Llama-3.1 e modelos matemáticos especializados como DeepSeek-Prover) no benchmark T2.

• A Lacuna Semântica:

  • Precisão de Compilação: Os modelos alcançaram altas taxas de compilação (por exemplo, Claude-Sonnet-4.5: 80,3% no conjunto completo).
  • Precisão de Teste (TA): Os mesmos modelos alcançaram pontuações de TA drasticamente menores (por exemplo, Claude-Sonnet-4.5: 38,9% no conjunto completo; 4,5% no conjunto Difícil).
  • Falsos Positivos: Até 93,1% dos teoremas compiláveis foram encontrados semanticamente incorretos quando testados contra sucessores.

• Falha das Métricas Existentes:

  • BLEU: Alta similaridade léxica (pontuações BLEU) mostrou quase nenhuma correlação com a correção semântica (Correlação: 0,123). Os modelos podiam gerar provas textualmente semelhantes, mas logicamente erradas.
  • Modelos Especializados: Modelos ajustados especificamente para prova de teoremas frequentemente alcançaram taxas de compilação mais altas, mas performaram pior ou de forma similar aos modelos de propósito geral na TA, sugerindo que eles se sobrecarregaram na sintaxe em vez da semântica.

• Impacto do Contexto:

  • Fornecer Teoremas Sucessores como contexto de entrada melhorou consistentemente a TA (por exemplo, +4,9% para Claude-Sonnet-4.5).
  • Fornecer apenas Provas em NL sem sucessores não melhorou o desempenho e às vezes o degradou.
  • Prompting com poucos exemplos e refinamento iterativo (usando feedback do compilador) produziram melhorias negligenciáveis no conjunto Difícil, indicando que a dificuldade reside no raciocínio semântico profundo, e não apenas na formatação da tarefa.

5. Significado e Conclusão

Este artigo desafia fundamentalmente o estado atual da avaliação de Prova Automatizada de Teoremas (ATP).

• Redefinindo o Sucesso: Ele prova que a "compilação" é uma condição necessária, mas insuficiente, para a geração de teoremas. Um modelo pode ser sintaticamente perfeito, mas semanticamente inútil.
• Confiabilidade: O benchmark T2 e a métrica TA fornecem uma maneira rigorosa e automática de avaliar se um LLM realmente entende conceitos matemáticos ou está meramente alucinando código sintaticamente válido.
• Direção Futura: O trabalho sugere que futuros sistemas de ATP devem ser avaliados com base em sua capacidade de integrar-se a bases de código existentes (geração consciente de dependências) em vez de resolver quebra-cabeças isolados. Também destaca que fornecer o "conjunto de testes" (teoremas sucessores) ao modelo durante a geração é uma estratégia crucial para melhorar o alinhamento semântico.

Em resumo, o artigo argumenta que o teste de integração é o elo perdido na avaliação de LLMs para matemática formal, revelando que os modelos de última geração atuais estão longe de alcançar correção semântica confiável na prova de teoremas.