Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Lazar Milikic; Etienne Bamas; Emmanuel Abbe; Viktor Kunčak

cs.LGOct 15, 2026

Learning Lean Feedback for Efficient Proof-Candidate Evaluation on GPUs

Authors: Lazar Milikic, Etienne Bamas, Emmanuel Abbe, Viktor Kunčak

Organizations: EPFL, Lausanne, Switzerland

Abstract

Training language models for formal theorem proving requires large numbers of verifier calls. Slow checks and timeouts often leave GPUs waiting and withhold rewards from potentially correct proofs. We train neural evaluators to predict Lean 4 verdicts and compiler feedback on GPUs using 4.84M labelled programs. We compare two validity classifiers with a feedback model that annotates proof attempts with predicted goal states and error messages. A two-stage evaluator that screens candidates with a classifier and scores its positive predictions with the feedback model reaches 87.8% accuracy in predicting whether Lean accepts a candidate proof, evaluated on a 68,932-program benchmark collected from public provers. The combined evaluator processes 3.5 candidates per second on one H100, 4.2x the throughput of our 64-worker Lean baseline with environment reuse. Finally, we combine our evaluator with Lean verdicts to obtain a hybrid reward system that shortens GRPO training steps by approximately 31%. After one GRPO epoch with hybrid rewards, the prover achieves nearly the same miniF2F pass@1 as with Lean-only rewards (62.2% versus 62.4%) and a pass@32 of 72.4% versus 71.3%.

Figures & tables

Figure 1: Hybrid rewards from concurrent Lean and GPU evaluation. Each batch contains 1,024 candidate proofs, checked by 64 Lean workers with a 60 s timeout per proof. Lean-only batch scoring takes approximately 420 s on average. Hybrid scoring ends when GPU evaluation finishes (90 s on average), retaining completed Lean verdicts and using model predictions for unfinished checks, which are cancelled. The Lean curve beyond this point shows the Lean-only reference. The 3.6% timeout share is measured over the 24,359 candidates with extractable code in the replay cohort (Appendix E ). Curves and phase durations are schematic; flat neural regions represent loading and warmup.

Data	Programs	Valid fraction
Training corpus	4.84M	44.8%
In-house validation (miniF2F and ProofNet)	27,210	38.9%
miniF2F benchmark candidates	41,638	61.7%
ProofNet benchmark candidates	27,294	9.0%
Combined benchmark (deduplicated)	68,932	40.8%

Table 1: Training, validation, and benchmark data. Benchmark rows combine Pythagoras [ 22 ] , Goedel [ 18 ] , and DeepSeek [ 23 ] outputs. Valid fractions describe the proof correctness rate over all candidate programs, not theorem-level pass rates.

	Encoder	One-token	Feedback
Backbone	ModernBERT-large (395M)	Qwen3-8B	Qwen3-4B
Pretraining task	Predict masked tokens (30% masking)	Predict next token	Predict next token
Supervised target	Binary validity label	One true / false token	Source annotated with feedback
Context (tokens)	8,192	32,768	32,768
Learning rate	$2\times 10^{-5}$	$10^{-5}$	$10^{-5}$
Batch size	64	8	8

Table 2: Evaluator training. Models first receive continued pretraining on approximately 130M Lean tokens, then one supervised epoch. Context lengths and optimization settings below refer to supervised training.

Evaluator	Accuracy	Macro F1	MCC	AUROC
Cascade, SC feedback stage @4/5	0.888	0.887	0.783	—
Cascade, calibrated gate (0.82) †	0.887	0.885	0.778	—
Cascade: one-token $\to$ feedback	0.878	0.877	0.772	—
Cascade, FP8 feedback stage	0.877	0.876	0.770	—
Feedback 4B, 5-sample SC @4/5	0.874	0.873	0.762	0.919
Feedback 4B	0.851	0.851	0.733	—

Table 3: Verdict prediction on the full evaluation benchmark. Self-consistency (SC) samples five traces at temperature 0.8 and requires four valid votes; all other feedback settings use greedy decoding.

\dagger

: threshold selected on in-house validation data; other classifier and gate thresholds are 0.5. Best values in each metric are bold.

Prover	Valid fraction	Feedback	One-token	Cascade
Goedel-Prover-V2-8B	0.530	0.867	0.819	0.893
DeepSeek-Prover-V2-7B	0.408	0.843	0.765	0.878
Pythagoras-Prover-4B	0.328	0.848	0.688	0.865

Table 4: Accuracy by prover on the evaluation benchmark. Each row combines miniF2F and ProofNet outputs; their proportions and the fraction of valid candidates differ across provers.

Metric	Overall	Valid	Invalid
Block F1, exact	0.796	0.969	0.623
Anchored block F1	0.795	0.969	0.621
Token F1	0.852	0.983	0.721
Error-presence agreement	0.840	0.974	0.707

Table 5: Predicted feedback compared with Lean v4.15.0 annotations on 2,004 evaluation-benchmark programs, balanced by prover and validity label. Appendix D defines all metrics.

Evaluator	Candidates/s	Seconds/candidate
ModernBERT	264	0.0038
One-token 8B	4.9	0.204
Feedback 4B, no speculation	0.73	1.37
Feedback 4B $+$ speculation	3.27	0.306
Cascade	3.48	0.287
Cascade, FP8 feedback stage	3.59	0.279

Table 6: Neural throughput on one H100 and Lean throughput on CPUs. Feedback uses greedy decoding. Cascade timings include loading and model transitions; standalone timings exclude warmup and tokenization. The Lean REPL pool runs the benchmark verification pipeline with 64 workers and environment reuse.

Checkpoint / reward source	Pass@1 (%)	Pass@32 (%)	Step time (s)
Initial checkpoint (shared)	$53.8\pm 0.6$	$72.8\pm 0.3$	—
GRPO, Lean-only, 60 s timeout	$62.4\pm 0.6$	$71.3\pm 0.8$	1,050
GRPO, hybrid rewards	$62.2\pm 0.8$	$72.4\pm 0.4$	720
GRPO, Lean-only, 13 s timeout	$59.8\pm 0.6$	$69.7\pm 1.1$	720

Table 7: Prover performance and training time. Pass@1 and pass@32 on all 488 miniF2F validation and test problems, before and after one epoch of GRPO. Values are mean

\pm

standard deviation across five evaluations for pass@1 and three for pass@32. Step times are approximate and include generation, reward scoring, and policy updates. Timeouts in the row labels apply to each proof during reward scoring.

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Prover	Benchmark	Lean	Rows	Valid
Pythagoras-Prover-4B	miniF2F	v4.15.0	14,903	0.574
Pythagoras-Prover-4B	ProofNet	v4.15.0	10,335	0.039
Goedel-Prover-V2-8B	miniF2F	v4.15.0	13,706	0.715
Goedel-Prover-V2-8B	ProofNet	v4.15.0	6,205	0.155
DeepSeek-Prover-V2-7B	miniF2F	v4.15.0	15,408	0.620
DeepSeek-Prover-V2-7B	ProofNet	v4.15.0	11,182	0.124

Appendix

Table 8: Per-run composition before cross-run deduplication.

Setting	Value
Training prompts / rollouts per prompt	128 / 8
PPO minibatch / actor microbatch	128 prompts / 1 sequence per GPU
PPO clip ratio / update epochs per rollout batch	0.2 / 1
Optimizer / $(\beta_{1},\beta_{2})$	AdamW / $(0.9,0.999)$
Weight decay / gradient clipping	0.01 / 1.0
Learning rate / warmup	$3\times 10^{-6}$ / 25 updates

Appendix

Table 9: GRPO settings shared by all three reward conditions. Each run trains for one epoch; reward-scoring timeouts are specified above.

Checkpoint / reward source	Pass@1 (%)	Pass@32 (%)
Initial checkpoint (shared)	$53.8\pm 0.6$	$72.8\pm 0.3$
GRPO, hybrid rewards (cascade)	$62.2\pm 0.8$	$72.4\pm 0.4$
GRPO, hybrid rewards (cascade), second seed	$62.7\pm 0.7$	$72.1\pm 0.6$
GRPO, hybrid rewards (one-token, threshold 0.86)	$57.6\pm 0.8$	$70.3\pm 0.4$
GRPO, hybrid rewards (ModernBERT, threshold 0.5)	$48.4\pm 0.6$	$63.1\pm 0.4$
GRPO, cascade predictions only, no Lean	$59.0\pm 0.6$	$70.7\pm 0.1$

Appendix

Table 10: Additional GRPO runs on all 488 miniF2F problems after one epoch. Values are mean

\pm

standard deviation across five evaluations for pass@1 and three for pass@32. The first two rows repeat Table 7 for reference.

Evaluator in hybrid run	Step	Accuracy	FPR	Lean share
Cascade	25	87.9	17.8	42.8
	125	81.9	25.7	42.8
	250	81.7	28.9	43.7
One-token 8B (threshold 0.86)	25	81.1	37.0	41.9
	125	68.0	56.9	40.2
	250	59.6	74.1	40.1

Appendix

Table 11: Evaluator accuracy on the rollouts of hybrid GRPO training, against Lean labels. Each evaluator is measured in its own hybrid run. All values are percentages.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 160 papers

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
May 11, 2026Zeynel A. Uluşan, Burak S. Akbudak, Can S. Erer +1Reward Modeling Automated Theorem Proving
Koç University, Department of Computer Science and Engineering · Codeway Studios · Bo˘gaziçi University, Department of Computer Engineering +1
Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
Jun 10, 2026Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian +5Automated Theorem Proving Efficient Language Model Training
Imperial College London · University of Edinburgh · Nanyang Technological University +1
LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification
Oct 13, 2026Rodney Lafuente-Mercado, Salman Rahman, Jingyan Shen +3Process Supervision Process Reward Models
University of Texas at Austin · University of California, Los Angeles · New York University

May 11, 2026J/K move · Enter open · S save

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

Zeynel A. Uluşan, Burak S. Akbudak, Can S. Erer, Gözde Gül Şahin

Koç University, Department of Computer Science and Engineering · Codeway Studios · Bo˘gaziçi University, Department of Computer Engineering+1

Reward Modeling Automated Theorem Proving Process Reward Models Lean Theorem Proving Reward Model Evaluation

Open paper AskPDF 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.

Abstract

Automated Theorem Proving

Explore similar work

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification