Resumo Técnico: FormalRewardBench

Declaração do Problema

Avanços recentes em provadores de teoremas neurais dependem fortemente de Aprendizado por Reforço com Recompensas Verificáveis (RLVR). Neste paradigma, assistentes de prova (como Lean 4) fornecem sinais binários de correção (passagem/falha) baseados em verificação de tipos. Embora esses sinais sejam escaláveis e imunes a manipulação de recompensas, eles sofrem de atribuição de crédito esparsa: os modelos não recebem sinal de aprendizado para progresso parcial em problemas difíceis, pois uma prova que falha no passo final recebe a mesma recompensa zero que uma abordagem completamente incorreta.

Para mitigar isso, pesquisadores propuseram modelos de recompensa aprendidos capazes de avaliar a qualidade da prova além da verificação binária. No entanto, comparar esses modelos de recompensa é atualmente desafiador, pois tipicamente requer ablações de treinamento de Aprendizado por Reforço (RL) dispendiosas. Além disso, benchmarks existentes para modelos de recompensa (por exemplo, RewardBench, ProcessBench) focam em raciocínio em linguagem natural informal e não abordam a precisão sintática, correção de tipos e validade lógica exigidas para a prova formal de teoremas. Atualmente, não há nenhum benchmark para avaliar diretamente modelos de recompensa em provas formais sem execuções de treinamento.

Metodologia

Os autores introduzem o FormalRewardBench, o primeiro benchmark projetado para avaliar modelos de recompensa para prova formal de teoremas em Lean 4. O benchmark consiste em 250 pares de preferência, onde cada par contém uma prova formalmente verificada como correta e uma variante incorreta.

Construção do Conjunto de Dados

O conjunto de dados é derivado do MiniF2F, uma coleção de 488 problemas matemáticos de nível olímpico formalizados em Lean 4. Os autores empregam um pipeline controlado de injeção de erros para gerar provas incorretas que satisfazem três critérios:

1. Validade Sintática: A prova incorreta deve ser analisada como código Lean válido.
2. Plausibilidade Semântica: Os erros não devem ser triviais (por exemplo, variáveis indefinidas), mas sim refletir modos de falha realistas.
3. Padrões de Erro Realistas: Os erros devem espelhar falhas reais de Modelos de Linguagem de Grande Escala (LLMs).

Estratégias de Injeção de Erros

Cinco estratégias curadas por especialistas são usadas para gerar variantes incorretas, implementadas via prompts para um LLM de ponta (Claude Opus 4.5):

1. Variações Únicas Mínimas: Modificações cirúrgicas em provas corretas (por exemplo, trocar hipóteses, alterar um único nome de variável ou lema) que causam falha semântica enquanto mantêm a validade sintática.
2. Justificativa em Linguagem Natural: Aumentar provas incorretas com comentários em linguagem natural enganosos que justificam o raciocínio falho, testando o "viés de verbosidade".
3. Injeção de Código Python: Substituir passos de prova formais em Lean por código Python executável que pode resolver o problema computacionalmente, mas falha no requisito de uma prova formal (testando a adesão à tarefa).
4. Erros Forçados de LLM: Gerar provas contendo erros formais comuns identificados em saídas anteriores de modelos, como aplicação incorreta de táticas, seleção errada de hipóteses ou instanciação incorreta de lemas.
5. Provas Incorretas Verbosas: Gerar provas desnecessariamente longas com estruturas sofisticadas e lemas intermediários que camuflam falhas lógicas fundamentais.

Protocolo de Avaliação

O benchmark avalia modelos em dois cenários:

• Pontual: O modelo pontua cada prova independentemente; a precisão é medida se a pontuação para a prova correta exceder a da incorreta.
• Par a Par: O modelo compara duas provas e emite uma preferência. Para mitigar o viés de posição, a precisão é contabilizada apenas se o modelo identificar consistentemente a prova correta em ambas as ordenações (correta-primeira e correta-segunda).

Resultados Principais

Os autores avaliaram quatro categorias de modelos: LLMs de Ponta, LLMs Julgadores, LLMs de Propósito Geral e Modelos Especializados em Prova de Teoremas.

1. Hierarquia de Desempenho: LLMs de Ponta (por exemplo, Claude Opus 4.5) alcançaram o melhor desempenho (59,8% de precisão par a par). LLMs Julgadores (treinados em dados de preferência) superaram substancialmente provadores de teoremas especializados entre modelos de pesos abertos (52,8% vs. 12,8% para alguns modelos especializados).
2. A Lacuna Geração-Avaliação: Modelos especializados em prova de teoremas (por exemplo, DeepSeek-Prover-V2-7B, Gödel-Prover-V2-8B) tiveram o pior desempenho (variando de 0,0% a 24,4%). Apesar de alcançarem métricas state-of-the-art de pass@k no MiniF2F, esses modelos lutam para avaliar provas. Os autores atribuem isso à falta de treinamento em detecção de erros; esses modelos são otimizados para gerar provas corretas via SFT e RLVR, mas não aprenderam a identificar ou criticar erros.
3. Gradiente de Dificuldade dos Erros:
   • Mais Fácil: Injeção de Código Python (S3), onde a detecção depende da identificação de linguagem em vez de compreensão da prova.
   • Mais Difícil: Provas Incorretas Verbosas (S5) e Erros Forçados (S4). Mesmo os melhores modelos alcançaram apenas ~60% no S5 e ~50% no S4.
   • Limitações do Modelo Julgador: Modelos julgadores mostraram um padrão bimodal: desempenho quase perfeito na injeção de Python, mas colapsando para quase zero em provas verbosas, sugerindo que seu treinamento de preferência desenvolve discriminação superficial em vez de raciocínio formal profundo.
4. Viés de Posição: Um viés de posição significativo foi observado em todas as categorias, particularmente em provadores especializados (por exemplo, DeepSeek-Prover-V2-7B preferiu a primeira prova 94,9% das vezes, independentemente da correção).

Significado e Alegações

O artigo alega três contribuições principais:

1. FormalRewardBench: Um benchmark inovador que permite a comparação direta de modelos de recompensa para prova formal de teoremas sem a necessidade de ablações de treinamento de RL dispendiosas.
2. Metodologia: Um conjunto reutilizável de cinco estratégias de injeção de erros para gerar provas formais incorretas realistas, aplicável a outros assistentes de prova, aumento de dados ou design de currículo.
3. Insight Empírico: A descoberta de que capacidades gerais de modelagem de recompensa (encontradas em modelos de ponta e julgadores) transferem-se mais efetivamente para a avaliação de provas do que o treinamento específico de domínio em prova de teoremas.

Os autores enfatizam que, embora o desenvolvimento de modelos de recompensa eficazes possa acelerar a descoberta e verificação matemática, os modelos atuais têm limitações significativas. Eles destacam que a verificação formal permanece o árbitro final da correção, pois modelos de recompensa imperfeitos carregam riscos de superconfiança. O benchmark é lançado publicamente para encorajar pesquisas adicionais sobre modelos de recompensa para matemática formal.

O artigo conclui notando limitações, incluindo a dependência de verificação automática para a maioria dos exemplos, o foco exclusivo no Lean 4 e a exclusão de avaliação em nível de processo ou passo a passo. Sugere-se trabalho futuro focado em abordagens híbridas combinando modelos de recompensa aprendidos com verificação formal e na extensão do benchmark para outros assistentes de prova como Coq e Isabelle.