FormalRewardBench

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

---

Recent neural theorem provers use reinforcement learning with verifiable rewards (RLVR), where proof assistants provide binary correctness signals. While accurate and scalable, this binary feedback suffers from sparse credit assignment: a proof attempt that makes substantial progress but fails at the final step receives the same zero reward as a completely wrong approach. This motivates learned reward models that can evaluate proof quality beyond binary verification.

FormalRewardBench is the first benchmark for evaluating reward models in formal theorem proving with Lean 4. It consists of 250 preference pairs where correct proofs are paired with incorrect variants generated through five expert-curated error injection strategies. Rather than measuring pass@k proof generation ability, it directly measures whether a model can distinguish valid from invalid proofs.

Key Results

Frontier LLMs achieve the highest performance (Claude Opus 4.5: 70.1% pointwise, 59.8% pairwise), while specialized theorem provers perform the worst despite achieving state-of-the-art pass@k on MiniF2F. This generation–evaluation asymmetry arises because provers train exclusively on correct proofs, never developing the capacity to identify errors. Judge models trained on preference data transfer this capability to formal proofs even without Lean-specific training.

Overall Performance

Model	Pointwise	Pairwise
Frontier LLMs
Claude Opus 4.5	70.1	59.8
Claude Sonnet 4.5	62.0	45.7
Gemini 2.5 Flash	50.9	25.2
GPT-5.2	48.9	39.7
GPT-4.1	44.0	32.1
Judge LLMs
Con-J-Qwen2-7B	52.8	—
Selene-1-70B	46.8	44.4
LMUnit-72B	41.2	36.8
CompassJudger-14B	40.3	35.2
General-Purpose LLMs
Qwen2.5-72B-Instruct	39.8	—
Qwen2.5-Coder-32B	36.4	37.6
DeepSeek-Coder-V2-Lite	38.3	28.0
Theorem Proving Specialized
Gödel-Prover-V2-32B	36.4	24.4
DeepSeek-Prover-V2-7B	13.7	9.4
DeepSeek-Prover-V1.5-RL	11.7	9.2
Gödel-Prover-V2-8B	0.0	0.4

Performance by Error Strategy (Pairwise %)

Model	S1 Complex	S2 Minimal	S3 NL Justif.	S4 Forced	S5 Python
Claude Opus 4.5	60	46	52	50	72
Claude Sonnet 4.5	42	42	32	42	56
Selene-1-70B	20	44	44	18	96
CompassJudger-14B	2	28	34	12	100
Gödel-V2-32B	22	8	28	18	46
DS-Prover-V2-7B	10	16	24	20	48

S5 (Python Injection) is easiest — most frontier models score 94–100% since detection requires only language identification. S1 (Complex Incorrect) and S4 (Forced Mistakes) are hardest; even the best model achieves only 60% on S1. Judge models show a sharply bimodal pattern: near-perfect on S5 but collapsing to 0–2% on S1.

Dataset

The benchmark is built from MiniF2F, a dataset of 488 olympiad-level problems formalized in Lean 4 (algebra, number theory, combinatorics from AMC, AIME, and IMO). Each preference pair contains one formally verified correct proof and one incorrect but plausible variant.

250 preference pairs — 50 per error strategy:

Strategy	Description
S1 Minimal Single-Point Variations	Surgical single-point edits with maximal semantic impact: swap one lemma name (add_comm → mul_comm), one hypothesis (h1 ↔ h2), one operator (≤ → <), or one tactic (ring → omega). Looks nearly identical to the correct proof.
S2 Natural Language Justification	Incorrect proofs augmented with misleading comments that justify the flawed reasoning as if it were correct. Tests whether models rely on surface-level explanations or verify proof correctness.
S3 Python Code Injection	Lean tactics replaced with Python code that may correctly solve the problem computationally — but using Python when Lean is required is fundamentally wrong. Tests task adherence.
S4 Forced LLM Mistakes	Common formal proof errors made by language models: incorrect tactic application, wrong hypothesis selection, incorrect lemma instantiation. Errors are semantic, not syntactic.
S5 Complex Incorrect Proofs	Long, sophisticated-looking proofs with many steps and intermediate lemmas. Tests whether reward models can track correctness over extended reasoning or are deceived by superficial complexity.

Quality control: For S1–S4, every correct proof passes Lean's type checker and every incorrect proof fails it. A triviality filter rejects superficial errors (e.g., "unexpected token") while accepting semantic errors (e.g., "type mismatch"). S5 bypasses Lean validation as Python code does not parse as Lean.

Evaluation Protocol

Pointwise: The model scores each proof independently (0–20). A sample is correct if score(chosen) > score(rejected).

Pairwise: The model directly compares both proofs. To mitigate position bias, each sample is evaluated in both orderings — a prediction is correct only when correct in both:

Correct_consistent = Correct(normal order) ∧ Correct(reversed order)

This is why pairwise scores are consistently lower than pointwise scores.

Repository Structure

formal_rewardbench/
├── src/formal_rewardbench/
│   ├── evaluation/
│   │   ├── evaluate.py          # Unified inference: Anthropic / OpenAI / Gemini / vLLM
│   │   ├── score_pairwise.py    # Aggregates normal+reversed runs → pairwise accuracy
│   │   └── score_pointwise.py  # Aggregates chosen+rejected runs → pointwise accuracy
│   ├── core/
│   │   └── vllm_sampler.py      # vLLM batched inference with LoRA and resume support
│   └── utils.py                 # Answer extraction and grading utilities
├── dataset/
│   ├── rewardbench_dataset.zip  # Curated 250-pair benchmark (default)
├── scripts/
│   ├── run_benchmark_pairwise.sh
│   ├── run_benchmark_pointwise.sh
└── prompts.yaml                                 # Prompt templates (v0/v1, pairwise/pointwise)

Installation

cd formal_rewardbench
pip install -e .

Requires Python >=3.13. For local inference: CUDA + vLLM-compatible GPUs.

Quick Start

cd scripts

# Pairwise benchmark
bash run_benchmark_pairwise.sh

# Pointwise benchmark
bash run_benchmark_pointwise.sh

# Scaling-law experiments
bash run_scaling_pairwise.sh
bash run_scaling_pointwise.sh

Inference CLI

evaluate supports Anthropic, OpenAI, Gemini, and local vLLM backends. Provider is auto-detected from --model_name:

Prefix	Provider
claude-*	Anthropic
gpt-*, o1-*, o3-*, o4-*	OpenAI
gemini-*	Google Gemini
anything else	vLLM (local)

Example — pairwise evaluation:

evaluate \
  --model_name "ZiyiYe/Con-J-Qwen2-7B" \
  --task_name "benchmark_unified_random_normal_v1" \
  --task_type "reward_model_evaluation_v1" \
  --prompts_path "../prompts.yaml" \
  --data "../dataset/rewardbench_dataset.zip" \
  --data_keys formal_statement chosen rejected \
  --output_path "results/pairwise_results/"

Example — multiple models via script override:

cd scripts
MODELS="org/model-a org/model-b" TASK_VERSION="v1" bash run_benchmark_pairwise.sh

Scoring

Aggregate pairwise results (normal + reversed):

score-pairwise \
  --model_name "ZiyiYe/Con-J-Qwen2-7B" \
  --input_path "results/pairwise_results/" \
  --output_path "results/pairwise_results/"

Aggregate pointwise results (chosen + rejected):

score-pointwise \
  --model_name "ZiyiYe/Con-J-Qwen2-7B" \
  --input_path "results_pointwise/" \
  --output_path "results_pointwise/"

Environment Variables

Variable	Description
MODELS	Space-separated list of model names
TASK_VERSION	Prompt version (v0 or v1)
N_PER_TYPE	Samples per task type for scaling experiments
CUDA_DEVICES	Visible CUDA devices
TENSOR_PARALLEL_SIZE	vLLM tensor parallelism
GPU_MEMORY_UTILIZATION	vLLM GPU memory fraction
BATCH_SIZE	Inference batch size
DATA / DATASET_DIR	Dataset path override
OUTPUT_PATH	Results output directory
PROMPTS_PATH	Path to prompts.yaml
HF_TOKEN	HuggingFace token for gated models

Output Files

File	Description
<model>_<task_name>	Raw inference output
<model>_pairwise_score	Aggregated pairwise accuracy
<model>_<chosen_task>_pointwise_score.json	Aggregated pointwise accuracy

Citation

@article{formalrewardbench2026,
  title   = {FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models},
  year    = {2026},
  note    = {}
}