Resumo Técnico: Avaliando Provas Matemáticas de Nível de Pesquisa via Verificação Estrita ao Nível de Passo

Declaração do Problema

Grandes Modelos de Linguagem (LLMs) e agentes de IA demonstraram capacidades significativas na resolução de problemas matemáticos; no entanto, eles têm dificuldade em verificar rigorosamente provas complexas de nível de pesquisa. Abordagens de avaliação global padrão sofrem de "envenenamento de contexto", onde afirmações superficialmente plausíveis mascaram falhas lógicas sutis, levando os agentes a alucinar validade ou a exibir excesso de ceticismo. Embora sistemas de verificação formal (ex: Lean) ofereçam garantias absolutas, sua aplicação é limitada pela necessidade de infraestrutura construída por humanos e bibliotecas mantidas manualmente, limitando sua utilidade para verificar matemática nova ou de fronteira em linguagem natural. Os agentes atuais carecem da capacidade intrínseca de distinguir o raciocínio sólido da lógica falha durante fases exploratórias sem depender de formalização externa.

Metodologia

O artigo propõe uma mudança da detecção de anomalias global para a verificação estrita ao nível de passo via elaboração construtiva. A metodologia central envolve o reenquadramento da tarefa de verificação: em vez de pedir a um LLM que detecte falhas em um texto monolítico, o agente é incumbido de expandir explicitamente cada passo dedutivo em uma derivação de granularidade mais fina.

O Framework de Explicação Tripartite

Para impor rigor e prevenir alucinações, o framework modela as dependências lógicas de qualquer passo dedutivo $s_i$ usando uma arquitetura tripartite $(\Gamma_i, \Sigma_i, T_i)$:

1. Contexto Local ($\Gamma_i$): Um conjunto finito de afirmações (teoremas, definições, hipóteses) originadas diretamente do texto da prova $S$.
2. Conhecimento Externo ($\Sigma_i$): Afirmações não triviais extraídas da literatura externa ou do consenso de domínio estabelecido. O agente deve explicitamente citar ou provar estas afirmações para evitar a alucinação de teoremas inexistentes.
3. Teoria de Base ($T_i$): Afirmações triviais, axiomas lógicos fundamentais (ex: Modus Ponens) e regras de reescrita necessárias para a derivação sintática. Este componente permite a manipulação direta de afirmações sólidas sem hierarquias algébricas rígidas.

Um passo é considerado válido apenas se existir uma explicação tal que $\Gamma_i \cup \Sigma_i \vdash_{T_i} a_i$, onde $a_i$ é a asserção do passo.

Fluxo de Trabalho Agêntico Baseado em Estados

O processo de verificação é implementado como um agente autônomo, orientado por estados, operando sobre um estado cognitivo discreto $c_i \in \{OPEN, VERIFIED, FLAWED\}$ para cada passo:

• Inicialização: Todos os passos começam como $OPEN$.
• Elaboração: O agente tenta expandir um passo $OPEN$ em uma derivação detalhada, extraindo explicitamente $(\Gamma_i, \Sigma_i, T_i)$.
• Transições de Estado:
  • $OPEN \to VERIFIED$: Ocorre apenas se a elaboração for logicamente fechada e todos os itens externos em $\Sigma_i$ forem suportados por subprovas diretas ou citações precisas.
  • $OPEN \to FLAWED$: Ocorre apenas quando uma "testemunha de falha" explícita (ex: uma afirmação falsa, inferência inválida ou teorema mal aplicado) é identificada.
  • Confirmação de Falha: Para evitar o excesso de rejeição pedante, qualquer estado $FLAWED$ preliminar aciona uma investigação adversarial. Se a falha percebida for determinada como uma ambiguidade epistêmica (ex: uma convenção de domínio não declarada) em vez de uma quebra lógica, o passo retorna para $OPEN$.
• Critérios de Parada: O processo termina após aceitação global (todos os passos $VERIFIED$), rejeição definitiva (uma falha é confirmada) ou exaustão (cinco iterações consecutivas sem progresso).

O agente mantém um Livro de Registro de Teoremas para rastrear o status de reivindicações externas, garantindo que o raciocínio subsequente não seja validado com base em suposições não verificadas.

Principais Contribuições

1. Mudança de Paradigma Metodológico: O artigo reenquadra a verificação de provas em linguagem natural de detecção de anomalias de caixa-preta para elaboração constutiva. Ao forçar os agentes a rastrear explicitamente as dependências lógicas através do framework $(\Gamma_i, \Sigma_i, T_i)$, a abordagem mitiga o pareamento de padrões superficial e o envenenamento de contexto.
2. Fluxo de Trabalho de Verificação Autônomo: É proposto um framework agêntico orientado por estados que prioriza a solidez lógica sobre a completude. Equipado com uma fase de confirmação fixa e critérios de parada robustos, o sistema aproveita efetivamente o computo em tempo de inferência para isolar erros sutis.
3. Insights Empíricos via Micro-benchmarking: O estudo introduz um conjunto de diagnóstico curado de 21 provas de nível de pesquisa (extraídas do desafio FirstProof) com verdade fundamental inequívoca. A avaliação revela que, enquanto os baselines padrão falham em detectar erros camuflados em provas inválidas, o framework proposto atinge zero falsos aceites. Inversamente, as rejeições de provas válidas são atribuídas principalmente a uma "hiper-rigidez pedante" em relação a convenções de domínio não declaradas, destacando uma vulnerabilidade específica nos modelos base em vez de uma falha na lógica de verificação.

Resultados

O framework foi avaliado em um conjunto de 21 provas contendo 11 provas válidas e 10 inválidas.

• Desempenho do Baseline: Avaliadores globais padrão (Global GPT-5.4, Global Codex) e ablações frase a frase demonstraram vulnerabilidades sistêmicas severas. Eles frequentemente aceitaram provas inválidas (Falsos Negativos) por serem enganados por textos estruturalmente rigorosos, mas matematicamente vacuos, e rejeitaram provas válidas (Falsos Positivos) ao alucinar lacunas em convenções notacionais padrão.
• Desempenho do Agente: O Agente de Verificação Construtiva identificou e isolou com sucesso falhas dedutivas fatais em 100% das provas inválidas. Nas provas válidas, ele verificou corretamente 8 de 11 casos. As 3 rejeições de provas válidas não se deveram a déficits lógicos, mas sim à incapacidade do agente de inferir convenções implícitas de domínio (ex: a linearidade de subgrupos em contextos específicos de grupos de Lie) que especialistas humanos assumem por padrão.
• Robustez: Diferente dos baselines que mostraram variância entre tentativas, o agente demonstrou consistência macroestrutural, produzindo vereditos finais idênticos em execuções independentes.

Significância e Alegações

O artigo alega que instruir agentes a organizar notas de verificação de maneira cautelosa, semelhante a um matemático humano, melhora substancialmente sua capacidade de distinguir provas rigorosas de falhas. A principal significância reside em demonstrar que a própria elaboração detalhada atua como um mecanismo para amplificar a descoberta de erros lógicos sutis que o raciocínio padrão negligencia.

Os autores enfatizam que este trabalho não visa reinventar assistentes de prova formal ou o Vernáculo Matemático (MV). Em vez disso, estabelece uma base teórica para sistemas automatizados de revisão de provas que operam em linguagem natural. Os achados sugerem que, ao forçar um modelo a escrever explicitamente os detalhes subjacentes, os agentes podem efetivamente podar caminhos sem saída e reduzir alucinações em conceitos matemáticos de fronteira. O artigo conclui que, embora os modelos base permaneçam vulneráveis a convenções não declaradas, o framework proposto oferece um paradigma generalizável para integrar a verificação rigorosa ao nível de passo nos processos de raciocínio interno de futuros agentes matemáticos de linguagem natural.