FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

• URL: http://arxiv.org/abs/2605.10141v1
• Date: Mon, 11 May 2026 07:51:15 GMT
• Title: FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
• Abstract summary: We introduce textbfFormalRewardBench, the first benchmark for evaluating reward models in formal theorem proving with Lean 4.<n>Our results reveal that frontier LLMs achieve the highest performance (59.8%%) while specialized theorem provers perform the worst (24.4%)<n>We release textbfFormalRewardBench publicly to encourage more research on developing reward models in formal mathematics.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 \textbf{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 \textbf{FormalRewardBench} publicly to encourage more research on developing reward models in formal mathematics.

Related papers

• AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification [41.90353470982016]
  Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics.<n>Existing benchmarks fall short in both scope and evaluation granularity.<n>We introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities.
  arXiv  Detail & Related papers  (2026-07-13T17:38:22Z)
• Learning to Reason Efficiently with A* Post-Training [119.18396754931602]
  We investigate whether large language models can learn to generate correct and efficient proofs with guidance from A* search.<n> Empirically, we find that Llama-3.2 models in the 1B--3B range benefit substantially from A* post training.<n>On larger search spaces, models trained with imperfects exhibit superior accuracy.
  arXiv  Detail & Related papers  (2026-05-23T14:28:57Z)
• SPARK: Stepwise Process-Aware Rewards for Reference-Free Reinforcement Learning [39.1720897614261]
  Process reward models (PRMs) that provide dense, step-level feedback have shown promise for reinforcement learning.<n>We propose SPARK: a three-stage framework where in the first stage a generator model produces diverse solutions and a verifier model evaluates them.<n>We show that aggregating multiple independent verifications at the step level produces training data for process reward models that surpass ground-truth outcome supervision.
  arXiv  Detail & Related papers  (2025-12-02T21:30:47Z)
• Hilbert: Recursively Building Formal Proofs with Informal Reasoning [38.36481253622752]
  Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions often contain errors that cannot be automatically verified.<n>We introduce Hilbert, an agentic framework that combines the complementary strengths of informal reasoning and formal verification.<n>Our system orchestrates four components: an informal LLM that excels at mathematical reasoning, a specialized prover LLM optimized for Lean 4 tactics, a formal verifier, and a semantic theorem retriever.
  arXiv  Detail & Related papers  (2025-09-26T18:24:23Z)
• Generalist Reward Models: Found Inside Large Language Models [50.7432354447554]
  We show that a powerful reward model is already latently present within any Large Language Models (LLMs) trained via standard next-token prediction.<n>We prove that this endogenous reward is not a reward function learned through offline inverse reinforcement learning.<n>We also prove that subsequent reinforcement learning using this endogenous reward leads to a policy with a provably superior error bound compared to the base model.
  arXiv  Detail & Related papers  (2025-06-29T13:45:54Z)
• Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening [36.81125165911328]
  Reinforcement learning is emerging as a primary driver for improving language model reasoning capabilities.<n>We investigate whether current reinforcement learning algorithms merely sharpen the base model's distribution around problems it can already solve.<n>We show that unlikeliness reward mitigates rank bias and improves pass@$N$ across a large range of $N$ in both synthetic and real theorem proving settings.
  arXiv  Detail & Related papers  (2025-06-03T01:15:15Z)
• Exploring the Limit of Outcome Reward for Learning Mathematical Reasoning [65.2421542320293]
  Reasoning abilities are crucial components of general intelligence.<n>Recent advances by proprietary companies, such as o-series models of OpenAI, have made remarkable progress on reasoning tasks.<n>This paper proposes a new RL framework, termed OREAL, to pursue the performance limit that can be achieved through textbfOutcome textbfREwtextbfArd-based reinforcement textbfLearning for mathematical reasoning tasks.
  arXiv  Detail & Related papers  (2025-02-10T18:57:29Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  This paper focuses on improving LLMs' ability to write proofs in formal languages that permit automated proof verification/evaluation. We work in a more natural setup where the lemmas that are directly relevant to the theorem are not given to the theorem prover at test time. We design an RL-based training algorithm that encourages the model to decompose a theorem into lemmas, prove the lemmas, and then prove the theorem by using the lemmas.
  arXiv  Detail & Related papers  (2024-11-04T05:57:40Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• RewardBench: Evaluating Reward Models for Language Modeling [100.28366840977966]
  We present RewardBench, a benchmark dataset and code-base for evaluation of reward models. The dataset is a collection of prompt-chosen-rejected trios spanning chat, reasoning, and safety. On the RewardBench leaderboard, we evaluate reward models trained with a variety of methods.
  arXiv  Detail & Related papers  (2024-03-20T17:49:54Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.