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

1. Problem Statement

While Large Language Models (LLMs) have achieved significant success in mathematical reasoning through Reinforcement Learning with Verifiable Rewards (RLVR), current approaches face a critical bottleneck: Verification Asymmetry.

• The Asymmetry: In many math benchmarks (e.g., GSM8K, MATH), verifying the final answer (a number or option) is trivial and automatable, while solving the problem is hard. This allows for scalable RL training.
• The Limitation: High-level mathematical problems (e.g., USAMO, IMO, research-level math) are predominantly proof-based. Verifying a full proof requires step-by-step logical checking, ensuring theorem applicability, and validating the logical flow. This process is complex, lacks simple "ground truth" answers, and currently requires expensive human expert annotation.
• The Consequence: Existing RLVR methods often fail on proof-based tasks because they rely on answer matching. Models may produce "correct answers with incorrect proofs" (hallucinated theorems, logical gaps) or fail to generalize to diverse proof styles. There is an urgent need for a Proof Reward Model (ProofRM) capable of reading, understanding, and verifying entire natural language proofs to enable scalable RL for advanced math.

2. Methodology

The authors propose a three-stage pipeline to build a scalable and generalizable ProofRM: Data Collection, Labeling, and Stable RL Training.

A. Scalable Data Construction Pipeline

To overcome the scarcity of diverse proof data, the authors designed an automated pipeline (Figure 1) that generates high-quality Question-Proof-Check (QPC) triplets with minimal human effort.

1. Multi-Dimensional Diversity Expansion (Step 1):

   • Sources: Aggregates problems from Olympiads (IMO, USAMO, Putnam), college entrance exams, and authentic student scripts.
   • Generation Methods: Uses LLMs to generate proofs via various strategies: Proof (generate from scratch), Rephrase (rewrite existing proofs), Mask (fill in masked key steps of ground truth), and Augment (change wording).
   • Model Diversity: Utilizes multiple LLMs (DeepSeek-R1, DeepSeek-V3.1, GPT-5-mini, Gemini-2.5-Flash) to ensure diverse reasoning styles, verbosity levels, and error types.
   • Result: Creates a dataset spanning difficulty levels, linguistic styles, and error modes (logical gaps, hallucinations, missing conditions).

2. LLM-Aided Consistent Labeling with Hierarchical Human Check (Step 2):

   • LLM Consensus: Three different LLMs check each proof 5 times total. A label (True/False) is accepted only if there is unanimous agreement.
   • Composition-Level Human Check: To ensure LLM labels align with human judgment without annotating every sample:
     • Data is partitioned into "combinations" based on source, method, and LLM.
     • Humans sample 0.5%–2.5% of each combination.
     • If LLM and human consistency exceeds a threshold (up to 90%), the entire combination is treated as "silver-standard" (reliable). Otherwise, the combination is discarded.
   • Efficiency: This pipeline generated 21,000 QPC training samples in ~100 hours, achieving a >12x efficiency boost compared to one-by-one human annotation.

B. Stable RL Training Algorithm

Training a ProofRM using binary (True/False) supervision on long reasoning traces often leads to model collapse (repetitive tokens, syntactic incoherence, or hasty assertions). The authors introduce two key stabilizers:

1. LLM-as-a-RM-for-RM: An auxiliary LLM evaluates the fluency and behavioral consistency of the ProofRM's output (checking for repetition, loops, or irrelevant tokens) without checking the math content. If the generation is "noisy," the reward is set to 0 regardless of the final verdict. This prevents the model from learning to "game" the system with gibberish that happens to get the right T/F label.
2. Balanced Token Weighting: Standard RL algorithms (like GRPO or DAPO) bias the model toward either very short or very long responses. The authors propose a weighted average strategy:
   $$\text{Weight} = \frac{\eta}{N|o_i|} + \frac{1-\eta}{\sum |o_i|}$$
   This balances the gradient contribution between short and long responses, preventing the model from collapsing into hasty assertions or indecisive rambling.

3. Key Contributions

• Problem Analysis: Identified the lack of verification asymmetry in proof-based math as a barrier to RLVR and argued for direct proof verification models.
• Data Pipeline: Proposed a scalable, diversity-driven data collection pipeline that combines real-world sources with LLM-augmented generation and rigorous, hierarchical human auditing.
• Training Recipe: Developed a stable RL training framework for ProofRMs, featuring an "LLM-as-a-RM-for-RM" for fluency supervision and a balanced token weighting strategy to prevent model collapse.
• Performance: Demonstrated that ProofRM significantly outperforms base models and frontier LLMs in proof verification accuracy and generalization.

4. Experimental Results

The model was trained on DeepSeek-R1 distilled models (8B, 14B, 32B) and evaluated on multiple benchmarks.

• Reward Accuracy:
  • On the internal test set, ProofRM-32B achieved 82.4% accuracy, outperforming the base model (72.5%) and frontier models like GPT-5-mini (74.6%) and DeepSeek-V3.1 (69.6%).
  • It showed significant improvements in identifying complex logical errors (e.g., incomplete logic flow, misused assumptions) compared to baselines.
• Generalization:
  • On the OPC (Open Proof Corpus) test set (out-of-distribution data), ProofRM-32B reached 81.3% accuracy, surpassing DeepSeek-R1 (80.9%) and approaching Gemini-2.5-Flash (82.7%).
  • It maintained strong performance across different proof styles (textbook, forum, research article).
• Test-Time Scaling (Best-of-k):
  • In a Best-of-k setting (selecting the best proof from 48 generated candidates), ProofRM demonstrated superior discrimination ability, achieving a higher Area Under the Curve (AUC) than baselines. This indicates its utility as a guide for test-time compute scaling and data filtering.

5. Significance

• Enabling Advanced Math RL: This work provides a practical pathway to apply Reinforcement Learning to high-level, proof-based mathematics, a domain previously inaccessible due to the lack of scalable verifiable rewards.
• Scalability: The proposed data pipeline proves that high-quality, diverse proof datasets can be constructed without prohibitive human costs, making the training of specialized math verifiers feasible.
• Stability in RL: The "LLM-as-a-RM-for-RM" and balanced token weighting techniques offer a blueprint for stabilizing RL training on complex, long-horizon reasoning tasks where binary supervision is noisy.
• Trustworthiness: By directly verifying the process (the proof) rather than just the outcome, ProofRM helps mitigate "shortcut learning" and hallucinations, leading to more trustworthy and robust mathematical reasoning in LLMs.