Resumo Técnico: Pseudo-Formalização para Verificação Automática de Provas

Declaração do Problema

A verificação automática confiável de provas matemáticas permanece um gargalo crítico para o treinamento e a avaliação de sistemas de IA em raciocínio matemático complexo. Embora provas totalmente formais (por exemplo, em Lean ou Isabelle) sejam fáceis de verificar devido à sua precisão semântica e modularidade, a maioria das provas — particularmente aquelas geradas por IA ou escritas por humanos em linguagem natural — carece dessas propriedades. A tradução de provas em linguagem natural para linguagens totalmente formais é frequentemente inviável para matemática de ponta devido a bibliotecas formais incompletas e ao imenso esforço especializado requerido. Consequentemente, os métodos de verificação atuais, como "LLM como juiz" (avaliação direta de provas em linguagem natural), lutam com precisão e recall, frequentemente falhando em identificar erros específicos em argumentos longos e complexos.

Metodologia: Pseudo-Formalização e Verificação por Blocos

Os autores propõem Pseudo-Formalização (PF) combinada com Verificação por Blocos (BV) como um arcabouço para preencher a lacuna entre a flexibilidade da linguagem natural e a verificabilidade de provas formais.

1. Formato de Prova Pseudo-Formal

Uma prova Pseudo-Formal decompõe um argumento em linguagem natural em uma sequência de módulos autocontidos (lemas, proposições, afirmações). Cada módulo é uma tupla $(P, c, \pi)$ representando:

• Premissas ($P$): Assunções explicitamente declaradas e contexto herdado.
• Conclusão ($c$): A afirmação específica sendo provada.
• Prova ($\pi$): O argumento em linguagem natural que estabelece $c$ a partir de $P$.

A estrutura é governada por dois grafos:

• Grafo de Dependência ($G$): Um Grafo Acíclico Direcionado (DAG) onde uma aresta existe se um módulo invocar a conclusão de outro. Isso previne raciocínio circular.
• Floresta de Herança de Escopo ($T$): Uma estrutura de floresta organizando módulos hierarquicamente (por exemplo, lemas dentro de uma proposição), permitindo que o contexto (definições, assunções) seja herdado sem reafirmação.

Os autores definem "Provas Pseudo-Formais Boas" como aquelas que aderem a dois desideratos: concisão (provas curtas invocando poucos outros nós) e profundidade de escopo limitada (árvores de herança rasas). Teoricamente, verificar tais provas permite que o comprimento de contexto necessário para cada etapa de verificação permaneça independente do tamanho total da prova, mitigando a "podridão de contexto" (a degradação do desempenho de LLMs com o aumento do comprimento de entrada).

2. O Pipeline de Verificação (PF+BV)

O processo de verificação envolve quatro etapas, todas utilizando LLMs prontos sem ajuste fino:

1. Tradução: Um LLM traduz a prova original em linguagem natural $\Pi$ em uma prova Pseudo-Formal $\hat{\Pi}$. Um loop opcional de auto-reparo verifica $\hat{\Pi}$ contra $\Pi$ para garantir fidelidade.
2. Verificação por Blocos: Um LLM verificador verifica cada módulo de $\hat{\Pi}$ independentemente. Ele recebe as premissas completas do módulo (incluindo contexto herdado), a conclusão, a prova e as conclusões verificadas de quaisquer módulos filhos invocados. Ele emite um veredito de aceitação ou uma descrição específica do erro.
3. Calibração: Um LLM calibrador agrega relatórios de erro por módulo em um veredito final. Ele pode aplicar limiares de rigor configuráveis e mapear erros de nível de bloco de volta para a estrutura da prova original (por exemplo, identificando etapas ou lemas específicos).
4. Escalonamento Paralelo: Todo o pipeline é executado $k$ vezes independentemente. Uma prova é aceita apenas se todas as $k$ execuções a aceitarem (agregação pessimista). Isso permite trocar precisão e recall variando $k$.

Principais Contribuições

1. Pseudo-Formalização (PF): Um novo formato de prova que mantém a flexibilidade da linguagem natural enquanto impõe a modularidade e a estrutura explícita de premissa-conclusão necessárias para uma verificação confiável.
2. Verificação por Blocos (BV): Um algoritmo que verifica provas decompondo-as em blocos independentes, reduzindo teoricamente os requisitos de contexto e melhorando empiricamente a detecção de erros.
3. ArxivMathGradingBench: Um novo benchmark composto por 35 artigos de matemática de nível de pesquisa do arXiv que contêm erros conhecidos e corrigidos pelos autores. Este conjunto de dados preenche uma lacuna em benchmarks existentes ao testar a verificação em provas de pesquisa do mundo real, em vez de problemas de nível de competição.
4. Justificativa Teórica: Os autores fornecem um teorema (Teorema 1) demonstrando que, para provas Pseudo-Formais "Boas", a verificação bloco a bloco pode ser simulada por um Transformer de tamanho fixo com comprimento de contexto independente do tamanho da prova, contrastando com o crescimento linear de contexto necessário para a verificação da prova inteira.

Resultados Experimentais

O método foi avaliado em dois benchmarks: Hard2Verify (problemas de nível de Olimpíada/Putnam) e ArxivMathGradingBench (artigos de nível de pesquisa).

• Desempenho vs. Baselines: Em ambos os benchmarks, PF+BV Pareto-domina a baseline "LLM como juiz". Isso significa que, para qualquer nível dado de recall (capacidade de encontrar erros), PF+BV alcança maior precisão (menos falsos alarmes), e vice-versa.
• Hard2Verify: PF+BV igualou a baseline em recall (~90%), mas reduziu significativamente o número de erros falsos sinalizados por prova (mais de 40% menos falsos positivos em $k=8$).
• ArxivMathGradingBench: O benchmark provou ser desafiador, com ambos os métodos deixando ~50% dos erros anotados não detectados em $k=8$. No entanto, PF+BV superou consistentemente a baseline em recall, taxas de falso alarme e na fração de artigos onde todos os erros anotados foram detectados.
• Análise Qualitativa: Estudos de caso (por exemplo, IMO 2024 P6) ilustram que PF+BV tem sucesso ao isolar saltos lógicos em blocos locais. Isso permite que o verificador detecte quando uma prova fortalece incorretamente uma premissa (por exemplo, inferindo "mesmo sinal" a partir de "nenhum $d$ e $-d$") sem precisar reavaliar todo o argumento global.

Significado e Alegações

O artigo alega que a Pseudo-Formalização oferece uma alternativa prática à autoformalização (tradução para Lean/Isabelle) para verificar pesquisa matemática moderna. Embora a autoformalização forneça garantias de correção mais fortes, ela é frequentemente intratável para a pesquisa atual devido à incompletude das bibliotecas. PF+BV sacrifica a certeza absoluta da verificação formal em troca de aplicabilidade a uma gama mais ampla de domínios matemáticos, aproveitando o vocabulário rico e as técnicas padrão da linguagem natural enquanto impõe uma estrutura que torna os erros mais fáceis de localizar.

Os autores posicionam este trabalho como um passo em direção à supervisão escalável do raciocínio de IA, fornecendo um mecanismo para gerar sinais de recompensa confiáveis para treinar LLMs em matemática difícil e auxiliar matemáticos humanos na revisão de provas. Eles reconhecem limitações, observando que produzir uma reescrita Pseudo-Formal fiel não é trivial e que trabalhos futuros poderiam envolver o treinamento de modelos para gerar provas diretamente neste formato.