Technical Summary: FormalRewardBench

Problem Statement

Recent advancements in neural theorem provers rely heavily on Reinforcement Learning with Verifiable Rewards (RLVR). In this paradigm, proof assistants (such as Lean 4) provide binary correctness signals (pass/fail) based on type checking. While these signals are scalable and immune to reward hacking, they suffer from sparse credit assignment: models receive no learning signal for partial progress on difficult problems, as a proof that fails at the final step receives the same zero reward as a completely incorrect approach.

To mitigate this, researchers have proposed learned reward models capable of evaluating proof quality beyond binary verification. However, comparing these reward models is currently challenging because it typically requires expensive Reinforcement Learning (RL) training ablations. Furthermore, existing benchmarks for reward models (e.g., RewardBench, ProcessBench) focus on informal natural language reasoning and do not address the syntactic precision, type correctness, and logical soundness required for formal theorem proving. There is currently no benchmark to directly evaluate reward models on formal proofs without training runs.

Methodology

The authors introduce FormalRewardBench, the first benchmark designed to evaluate reward models for formal theorem proving in Lean 4. The benchmark consists of 250 preference pairs, where each pair contains a formally verified correct proof and an incorrect variant.

Dataset Construction

The dataset is derived from MiniF2F, a collection of 488 olympiad-level mathematical problems formalized in Lean 4. The authors employ a controlled error injection pipeline to generate incorrect proofs that satisfy three criteria:

1. Syntactic Validity: The incorrect proof must parse as valid Lean code.
2. Semantic Plausibility: Errors must not be trivial (e.g., undefined variables) but rather reflect realistic failure modes.
3. Realistic Error Patterns: Mistakes should mirror actual failures of Large Language Models (LLMs).

Error Injection Strategies

Five expert-curated strategies are used to generate incorrect variants, implemented via prompts to a frontier LLM (Claude Opus 4.5):

1. Minimal Single-Point Variations: Surgical modifications to correct proofs (e.g., swapping hypotheses, changing a single variable or lemma name) that cause semantic failure while maintaining syntactic validity.
2. Natural Language Justification: Augmenting incorrect proofs with misleading natural language comments that justify the flawed reasoning, testing for "verbosity bias."
3. Python Code Injection: Replacing formal Lean proof steps with executable Python code that may solve the problem computationally but fails the requirement for a formal proof (testing task adherence).
4. Forced LLM Mistakes: Generating proofs containing common formal errors identified in previous model outputs, such as incorrect tactic application, wrong hypothesis selection, or incorrect lemma instantiation.
5. Verbose Incorrect Proofs: Generating unnecessarily long proofs with sophisticated structures and intermediate lemmas that camouflage fundamental logical flaws.

Evaluation Protocol

The benchmark evaluates models in two settings:

• Pointwise: The model scores each proof independently; accuracy is measured if the score for the correct proof exceeds the incorrect one.
• Pairwise: The model compares two proofs and outputs a preference. To mitigate position bias, accuracy is only counted if the model consistently identifies the correct proof across both orderings (correct-first and correct-second).

Key Results

The authors evaluated four categories of models: Frontier LLMs, Judge LLMs, General-Purpose LLMs, and Theorem Proving Specialized Models.

1. Performance Hierarchy: Frontier LLMs (e.g., Claude Opus 4.5) achieved the highest performance (59.8% pairwise accuracy). Judge LLMs (trained on preference data) substantially outperformed specialized theorem provers among open-weight models (52.8% vs. 12.8% for some specialized models).
2. The Generation-Evaluation Gap: Specialized theorem proving models (e.g., DeepSeek-Prover-V2-7B, Gödel-Prover-V2-8B) performed the worst (ranging from 0.0% to 24.4%). Despite achieving state-of-the-art pass@k metrics on MiniF2F, these models struggle to evaluate proofs. The authors attribute this to a lack of training on error detection; these models are optimized to generate correct proofs via SFT and RLVR but have not learned to identify or critique errors.
3. Error Difficulty Gradient:
   • Easiest: Python Code Injection (S3), where detection relies on language identification rather than proof understanding.
   • Hardest: Verbose Incorrect Proofs (S5) and Forced Mistakes (S4). Even the best models achieved only ~60% on S5 and ~50% on S4.
   • Judge Model Limitations: Judge models showed a bimodal pattern: near-perfect performance on Python injection but collapsing to near-zero on verbose proofs, suggesting their preference training develops surface-level discrimination rather than deep formal reasoning.
4. Position Bias: Significant position bias was observed across all categories, particularly in specialized provers (e.g., DeepSeek-Prover-V2-7B preferred the first proof 94.9% of the time regardless of correctness).

Significance and Claims

The paper claims three primary contributions:

1. FormalRewardBench: A novel benchmark enabling the direct comparison of reward models for formal theorem proving without the need for expensive RL training ablations.
2. Methodology: A reusable set of five error injection strategies for generating realistic incorrect formal proofs, applicable to other proof assistants, data augmentation, or curriculum design.
3. Empirical Insight: The finding that general reward modeling capabilities (found in frontier and judge models) transfer more effectively to proof evaluation than domain-specific training in theorem proving.

The authors emphasize that while developing effective reward models could accelerate mathematical discovery and verification, current models have significant limitations. They highlight that formal verification remains the ultimate arbiter of correctness, as imperfect reward models carry risks of overreliance. The benchmark is released publicly to encourage further research into reward models for formal mathematics.

The paper concludes by noting limitations, including reliance on automatic verification for most examples, focus solely on Lean 4, and the exclusion of process-level or step-by-step evaluation. Future work is suggested to focus on hybrid approaches combining learned reward models with formal verification and extending the benchmark to other proof assistants like Coq and Isabelle.