# FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

arXiv: https://arxiv.org/abs/2605.10141 · HTML: https://mlsanity.com/paper/2605.10141/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Process reward models for reasoning, one of 10 directions in LLM alignment / RLHF / preference optimisation.
- Builds on 23 of its 36 references that are in the map.
- First posted on arXiv 11 May 2026.

## Placed in

- LLM alignment / RLHF / preference optimisation / [Process reward models for reasoning](https://mlsanity.com/alignment/process-reward-models-for-reasoning/)

## Builds on (most cited first, 23 of 23)

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement](https://mlsanity.com/paper/2409.12122/) (2024)
- [RewardBench: Evaluating Reward Models for Language Modeling](https://mlsanity.com/paper/2403.13787/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Justice or Prejudice? Quantifying Biases in LLM-as-a-Judge](https://mlsanity.com/paper/2410.02736/) (2024)
- [ProcessBench: Identifying Process Errors in Mathematical Reasoning](https://mlsanity.com/paper/2412.06559/) (2024)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Generative Reward Models](https://mlsanity.com/paper/2410.12832/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [PRMBench: A Fine-grained and Challenging Benchmark for Process-Level Reward Models](https://mlsanity.com/paper/2501.03124/) (2025)
- [GenPRM: Scaling Test-Time Compute of Process Reward Models via Generative Reasoning](https://mlsanity.com/paper/2504.00891/) (2025)
- [Verbosity Bias in Preference Labeling by Large Language Models](https://mlsanity.com/paper/2310.10076/) (2023)
- [Phenomenal Yet Puzzling: Testing Inductive Reasoning Capabilities of Language Models with Hypothesis Refinement](https://mlsanity.com/paper/2310.08559/) (2023)
- [Don't Overthink it. Preferring Shorter Thinking Chains for Improved LLM Reasoning](https://mlsanity.com/paper/2505.17813/) (2025)
- [CompassJudger-1: All-in-one Judge Model Helps Model Evaluation and Evolution](https://mlsanity.com/paper/2410.16256/) (2024)
- [Improve LLM-as-a-Judge Ability as a General Ability](https://mlsanity.com/paper/2502.11689/) (2025)
- [Direct Judgement Preference Optimization](https://mlsanity.com/paper/2409.14664/) (2024)
- [LMUnit: Fine-grained Evaluation with Natural Language Unit Tests](https://mlsanity.com/paper/2412.13091/) (2024)
- [A Study of LLMs' Preferences for Libraries and Programming Languages](https://mlsanity.com/paper/2503.17181/) (2025)

## Built on by (most cited first, 2 of 2)

- [BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://mlsanity.com/paper/2607.28110/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)

## Abstract (arXiv)

Recent neural theorem provers use reinforcement learning with verifiable rewards (RLVR), where proof assistants provide binary correctness signals. While verifiable rewards are cheap and scalable without reward hacking issues, they suffer from sparse credit assignment: models receive no learning signal from difficult problems where partial progress goes unrewarded. This motivates learned reward models that can evaluate proof quality beyond binary verification. However, comparing reward models is challenging since it typically requires expensive RL training ablations. To address this, we introduce FormalRewardBench, the first benchmark for evaluating reward models in formal theorem proving with Lean 4. Our benchmark consists of 250 preference pairs where correct proofs are paired with incorrect variants generated through five expert curated error injection strategies: forced mistakes, minimal single-point variations, verbose incorrect proofs, natural language justification, and Python code injection. We evaluate frontier LLMs (e.g., Claude Opus 4.5), judge LLMs (e.g., CompassJudger-1-14B), general-purpose LLMs (e.g., Qwen2.5-72B-Instruct), and specialized theorem proving models (e.g., DeepSeek-Prover-V2-7B). Our results reveal that frontier LLMs achieve the highest performance (59.8%) while specialized theorem provers perform the worst (24.4%), suggesting that theorem proving ability does not transfer to proof evaluation. We provide further insights on various error injection mechanisms, highlighting the challenging nature of most injection mechanisms. We release FormalRewardBench publicly to encourage more research on developing reward models in formal mathematics.