Resumo Técnico: Falhas em Nosso Benchmarking Formal

Declaração do Problema

Embora os Grandes Modelos de Linguagem (LLMs) tenham avançado na prova de teoremas automatizada em Lean, a confiabilidade dos benchmarks utilizados para avaliá-los está comprometida. Uma intuição comum sugere que os benchmarks de Lean são "autoverificáveis" porque o kernel do Lean certifica cada artefato de prova; no entanto, este artigo argumenta que o kernel apenas certifica que uma prova estabelece um dado enunciado formal, não verificando se o enunciado formal codifica fielmente o problema informal pretendido, nem se o ambiente de avaliação é robusto a soluções triviais ou adversariais.

Consequentemente, as pontuações dos benchmarks podem ser enganosas devido a:

1. Erros de Especificação: O enunciado formal omite hipóteses ou restrições necessárias, tornando os problemas mais fáceis ou vacuamente verdadeiros.
2. Erros de Formalização: A tradução do processamento de linguagem natural para Lean representa incorretamente o problema (ex: domínios errados, quantificadores incorretos).
3. Brechas de Avaliação: Falhas no ambiente de avaliação permitem que modelos "passem" sem demonstrar capacidade genuína (ex: explorando sorry, táticas inseguras ou bugs de kernel).
4. Degradação de Manutenção: A evolução rápida do Lean e de suas bibliotecas (mathlib) causa deriva de versão, tornando os conjuntos de dados não compiláveis ou semanticamente deslocados ao longo do tempo.

Metodologia

Os autores conduziram uma auditoria em escala de corpus de cinco benchmarks de prova de teoremas em Lean amplamente utilizados e seus forks: miniF2F, ProofNet, FormalMath, CombiBench e ProverBench (cobrindo aproximadamente 10.000 variantes de problemas).

A metodologia envolveu três componentes primários:

1. Desenvolvimento de Taxonomia de Falhas: Os autores categorizaram os defeitos com base em onde eles entram no pipeline de benchmarking: Problemas de Fidelidade (durante a formalização), Brechas de Avaliação (durante a verificação/relato da prova) e Problemas de Manutenção (erros de origem e deriva de versão).
2. Verificadores Estáticos Automatizados: Eles implementaram 12 metaprogramas de Lean 4 para detectar perigos mecânicos. Estes verificadores utilizam prova de guarda semântica (via táticas como omega, assumption e simp) para identificar questões como:
   • Contraexemplos (valores concretos que refutam o teorema).
   • Teoremas vacuos (hipóteses insatisfatórias).
   • Axiomas sem fundamentação ou uso de sorry em provas.
   • Perigos aritméticos específicos do Lean (divisão por zero, subtração de naturais truncada, violações de domínio analítico).
3. Auditoria Semântica Assistida por LLM: Reconhecendo que a análise estática não pode detectar desalinhamentos semânticos (ex: hipóteses ausentes que são matematicamente implicadas mas não estão sintaticamente presentes), os autores avaliaram LLMs em um conjunto de desafio rotulado de 92 problemas. Eles utilizaram prompting de poucos disparos (few-shot) para classificar erros em seis categorias (ex: erros de especificação, desalinhamentos de domínio, erros de formalização).

Principais Resultados

A auditoria revelou 4.833 achados nos conjuntos de dados, sendo 398 portadores de um certificado de não provabilidade ou vacuidade verificável por máquina.

• Distribuição de Defeitos:
  • FormalMath: 3.250 achados (dominados por divisão por zero e problemas de subtração de naturais).
  • ProverBench: 370 achados (alta taxa de uso de axiomas e contraexemplos).
  • Variantes do miniF2F: 135–193 achados por variante, destacando problemas de formalização incompleta e proliferação de versões.
  • ProofNet: 67–82 achados, frequentemente relacionados à subespecificação.
• Verificação por LLM: Os verificadores estáticos produziram falsos positivos quando as guardas estavam incorporadas em definições de tipos ou estruturas. A filtragem por LLM (usando modelos como Gemini 3.0 Flash e GPT-5.2) reduziu os achados em ~35% no ProverBench, preservando todos os verdadeiros positivos confirmados, atingindo ~83% de precisão.
• Desempenho da Auditoria Semântica: Os LLMs alcançaram alta revocação (0.80–0.91), mas baixa precisão (0.20–0.30) na detecção de erros semânticos. Eles foram significativamente melhores em detectar erros de especificação explícitos (F1 ~0.51) do que erros profundos de formalização (F1 ~0.18), que exigem compreensão da intenção matemática.
• Impacto nas Pontuações: Os autores demonstraram que os defeitos têm efeitos bidirecionais nas pontuações reportadas dos provadores:
  • Deflação: Enunciados não prováveis ou falsos (devido a erros de origem) adicionam itens impossíveis ao denominador, baixando artificialmente as pontuações.
  • Inflação: Formalizações enfraquecidas (falta de hipóteses) tornam os problemas mais fáceis, inflando artificialmente as pontuações.
  • Exemplo: Corrigir 20 problemas falhos em um subconjunto permitiu que o DeepSeek-Prover-V2-7B resolvesse 3/20 e o Kimina-Prover-8B resolvesse 2/20, enquanto eles resolveram 0/20 nos enunciados originais falhos. Inversamente, reparar enunciados enfraquecidos no ProofNet reduziu as taxas de aprovação dos provadores testados.

Principais Contribuições

1. Auditoria Abrangente: Uma auditoria sistemática e de larga escala dos cinco principais benchmarks de Lean, revelando que os defeitos são sistemáticos e não anedóticos.
2. Taxonomia de Falhas: Uma classificação estruturada dos defeitos de benchmark nas categorias de Fidelidade, Avaliação e Manutenção, esclarecendo que diferentes intervenções são necessárias para cada uma (ex: análise estática para perigos de codificação vs. revisão humana para intenção semântica).
3. Conjunto de Ferramentas:
   • Verificadores Estáticos: Um conjunto de 12 verificadores automatizados implementados como metaprogramas de Lean 4.
   • Prompts de Auditoria: Um conjunto de prompts orientados à revocação para LLMs auxiliarem na auditoria semântica.
   • Snapshots Corrigidos: Lançamento de variantes corrigidas dos conjuntos de dados e resultados da auditoria.
4. Padrões de Lançamento: Propostas para a criação de benchmarks confiáveis, incluindo:
   • Usar proof wanted em vez de sorry para evitar que o sorry atue como um axioma.
   • Desativar autoImplicit para forçar declarações de tipo explícitas.
   • Proibir axiomas nos arquivos de problemas.
   • Fixar versões do Lean/mathlib para evitar a deriva.

Significância e Alegações

O artigo alega que, embora o kernel do Lean forneça certeza matemática sobre a relação entre uma prova e um enunciado formal, ele não garante a validade do benchmark em si. Os autores argumentam que o estado atual do benchmarking formal sofre de um "hiato de confiança", onde a fidelidade da especificação e a robustez da avaliação são frequentemente negligenciadas.

A significância deste trabalho reside na:

• Reprodutibilidade: Destacar que a proliferação de versões e os forks não documentados tornam as comparações entre artigos pouco confiáveis.
• Integridade da Avaliação: Demonstrar que as pontuações reportadas em prova de teoremas automatizada são frequentemente artefatos de defeitos nos conjuntos de dados, e não uma capacidade genuína do modelo.
• Remediação Acionável: Fornecer um kit de ferramentas prático (verificadores, prompts, padrões) para ajudar os criadores de benchmarks a identificar e corrigir defeitos antes do lançamento, melhorando assim a qualidade dos dados de treinamento e a confiabilidade dos resultados de avaliação.

Os autores permanecem modestos, reconhecendo que sua auditoria não é uma enumeração completa verificada por humanos de todos os defeitos e que alguns problemas exigem profundo conhecimento matemático ou de Lean para serem resolvidos. No entanto, eles afirmam que sua taxonomia e ferramentas são suficientes para prevenir falhas de alto impacto e guiar a futura gestão de conjuntos de dados.