Proof-RM: A Scalable and Generalizable Reward Model for Math Proof

Resumo Técnico: Proof-RM

1. O Problema

Embora os Grandes Modelos de Linguagem (LLMs) tenham demonstrado capacidades notáveis em raciocínio matemático através do Aprendizado por Reforço com Recompensas Verificáveis (RLVR), a maioria dos problemas matemáticos avançados (como Olimpíadas e pesquisa) baseia-se em provas completas, e não apenas em respostas finais numéricas.

• Assimetria de Verificação: Em problemas de múltipla escolha ou numéricos, verificar a resposta é simples (comparação de strings), mas gerar a solução é difícil. No entanto, em provas matemáticas, essa assimetria desaparece: verificar se uma prova está correta exige um entendimento profundo da lógica, teoremas e condições, sendo tão complexo quanto gerá-la.
• Limitações do RLVR Atual: O RLVR tradicional depende de recompensas baseadas apenas no resultado final (correto/incorreto). Isso leva a modelos que podem produzir "respostas corretas com provas incorretas" (usando indução incompleta, conjecturas não provadas ou teoremas inexistentes), degradando a qualidade do raciocínio.
• Custo de Anotação: A verificação humana de provas de alto nível é extremamente cara e não escalável, exigindo especialistas que gastam horas por problema.

2. Metodologia

O artigo propõe o Proof-RM, um Modelo de Recompensa (RM) treinado para avaliar o processo completo de uma prova matemática (Question-Proof-Check), utilizando um pipeline escalável e generalizável.

A. Coleta de Dados Escalável (Pipeline QPC)
Para treinar o modelo, é necessário um conjunto de dados diversificado de triplas (Questão, Prova, Verificação T/F). O pipeline proposto envolve:

1. Geração de Diversidade: Utilização de LLMs para gerar provas a partir de questões de fontes diversas (Olimpíadas, USAMO, Putnam, soluções oficiais e scripts de alunos).
2. Variação de Métodos: Aplicação de diferentes técnicas de geração, como:
   • Rephrase: Reescrever provas existentes.
   • Proof: Gerar provas do zero.
   • Mask: Ocultar passos-chave de uma prova correta e pedir ao LLM para preenchê-los (gerando erros sutis).
   • Augment: Alterar a linguagem mantendo o conteúdo.
3. Rótulos Consistentes (LLM + Humano):
   • Filtragem por Consenso: Três LLMs diferentes verificam cada prova 5 vezes. Apenas amostras com consenso unânime são mantidas inicialmente.
   • Verificação Humana Hierárquica: Para evitar viés dos LLMs, amostras de cada "combinação" (fonte + método + modelo gerador) são verificadas por humanos. Se a concordância entre LLM e humano for alta (>90% em uma amostra de 2.5%), todo o bloco é aceito como "padrão-prateado" (silver-standard). Caso contrário, o bloco é descartado.
   • Resultado: Um conjunto de dados de ~21.000 amostras gerado em ~100 horas, economizando mais de 90% do tempo em comparação com a verificação humana item a item.

B. Treinamento Estável do RM (RLVR)
O treinamento do RM enfrenta instabilidades (colapso do modelo) devido à supervisão binária (Verdadeiro/Falso) em processos de raciocínio longos.

• LLM-as-a-RM-for-RM: Um segundo LLM (auxiliar) monitora a fluência e o comportamento superficial da saída do RM. Se o RM apresentar repetição de tokens, loops lógicos ou incoerência sintática, a recompensa é zerada, independentemente da resposta final. Isso previne o reforço de comportamentos acidentais.
• Pesagem de Tokens Balanceada: Para evitar que o modelo aprenda a gerar respostas excessivamente longas (para justificar erros) ou curtas demais, os autores propõem uma estratégia de pesagem de tokens que combina médias intra-amostra e inter-amostra ($\eta/(N|o_i|) + (1-\eta)/\sum |o_i|$), estabilizando o comprimento da saída durante o treinamento.

3. Contribuições Principais

1. Análise da Assimetria: Identificação clara de que a verificação de provas completas carece da assimetria necessária para o RLVR tradicional, exigindo um RM capaz de ler e validar a lógica.
2. Pipeline de Coleta de Dados: Um método escalável para criar dados de "Questão-Prova-Verificação" com alta diversidade (fontes, estilos, tipos de erro) e qualidade, minimizando o custo humano através de verificação por amostragem combinatória.
3. Receita de Treinamento Estável: Técnicas inovadoras para treinar RMs de prova via RL, incluindo o uso de um verificador de fluência (LLM-as-a-RM-for-RM) e pesagem de tokens balanceada, permitindo treinar modelos por mais de 300 passos sem colapso.

4. Resultados Experimentais

O Proof-RM foi avaliado em múltiplas frentes:

• Precisão de Recompensa: O Proof-RM superou significativamente os modelos base (DeepSeek-R1, GPT-5-mini, Gemini) e outros baselines, alcançando 82.4% de precisão no modelo de 32B (vs. 72.5% do modelo base).
• Generalização: O modelo demonstrou forte capacidade de generalização em conjuntos de dados fora da distribuição (Out-of-Distribution), como o conjunto OPC (Open Proof Corpus), superando modelos fechados de ponta como o o3 e o DeepSeek-R1.
• Escalabilidade em Tempo de Teste (Best-of-k): Ao atuar como um guia para seleção de melhores respostas entre múltiplas gerações, o Proof-RM melhorou a taxa de sucesso (Best-of-k) em problemas de Olimpíadas, superando modelos de raciocínio avançados.
• Detecção de Erros: O modelo aprendeu a identificar erros sutis de lógica, como uso indevido de "Sem Perda de Generalidade" (WLOG), falhas em premissas e lacunas no fluxo lógico, onde modelos base frequentemente falham.

5. Significado e Impacto

• Avanço no Raciocínio Matemático: O trabalho fornece uma ferramenta prática para melhorar a capacidade de raciocínio de LLMs em matemática de alto nível, indo além da simples verificação de respostas finais.
• Viabilidade Econômica: Demonstra que é possível construir conjuntos de dados de alta qualidade para verificação de provas em escala, reduzindo drasticamente a dependência de anotação humana cara.
• Infraestrutura para Agentes Matemáticos: O Proof-RM serve como um componente crítico para agentes de IA que precisam gerar, verificar e refinar provas matemáticas complexas, habilitando aplicações em educação, pesquisa e resolução de problemas competitivos.

Em suma, o Proof-RM estabelece um novo padrão para a verificação de provas matemáticas por IA, combinando engenharia de dados inovadora com técnicas de treinamento de RL estáveis para superar as limitações atuais dos modelos de linguagem em tarefas de raciocínio profundo.