Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing

Bodla Krishna Vamshi; Haizhao Yang

cs.AIAug 11, 2026

Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing

Authors: Bodla Krishna Vamshi, Haizhao Yang

Organizations: University of Maryland, College Park

Abstract

Formal theorem proving with large language models remains challenging due to the difficulty of navigating large proof search spaces efficiently. Existing tree search approaches either feed verbose compiler error messages directly into the generation context, increasing context usage during search, or employ non-standard evaluation protocols that prevent direct comparison with established baselines. We propose a three-role Monte Carlo Tree Search (MCTS) framework that treats the Lean 4 compiler purely as a reward oracle using compiler output as a scalar signal for UCB-guided tree updates without feeding error content into the generation context. Our framework decomposes proof search into three roles: a generator for proof attempts, a decomposer for subgoal decomposition, and a critic for subgoal quality evaluation. We evaluate across 4 benchmarks spanning competition mathematics and physics (MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata) with three prover models at standard proof attempt budgets (PAB@16 to PAB@256). Our method achieves 87.1% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 surpassing base sampling 18/659 at same proof attempt budget. Through an exhaustive axiom-level audit of every compiled proof, we further identify reward hacking in search-based theorem proving: DeepSeek-Prover-V2-7B produces proofs on PutnamBench that pass compilation and the standard sorry-token scan while depending on sorryAx. The audit removes 4 and 8 such proofs from whole-proof sampling at PAB@32 and PAB@128, and 11 and 19 from MCTS. We do not attribute these counts to the search procedure; we report them to establish that kernel-level auditing is necessary for compiler-verified evaluation.

Figures & tables

Method	Search	Search	Generator Receives	LLM	Search	Reward
	Representation	Strategy	Compiler Feedback	Critic	Allocation	Backprop.
COPRA	Formal proof state	Sequential refinement	✓ Compiler text	–	Fixed	–
Prover Agent	Proof attempts	Tree refinement	✓ Compiler text	–	Heuristic expansion	Method-specific
BFS+CG	Natural-language plans	Breadth-first	$\times$ (scalar evaluation only)	✓	Breadth-first	–
One-shot decomposition	Natural-language plans	Single expansion	$\times$ (scalar evaluation only)	✓	Flat expansion	–
Reward-Oracle MCTS (Ours)	Natural-language proof plans	UCB-guided MCTS	$\times$ Scalar reward only	✓	Adaptive	✓

Table 1: Architectural comparison between our framework and closely related inference-time search methods. “Compiler usage” refers to how Lean verification is incorporated into the search process.

Figure 1: Overview of the proposed search framework. Each node $n^{P}_{d,N}$ represents the $k$ -th child at depth $d$ , with parent $P$ : $P$ = $r$ denotes the root.

Model	Method	Size	Generator	Decomposer	Critic	Success (%)
			completions	completions	completions
Kimina	BFS+CG	7B	$4\times 2\times 4$	$4\times 4$	$4\times 4$	$62.5\pm 0.6$
	One-shot decomposition		$16\times 2\times 1$	$16\times 1$	$16\times 1$	$61.3\pm 0.6$
	Agent (ours)		$4\times 2\times 4$	$4\times 4$	$4\times 4$	$\mathbf{64.3\pm 0.8}$
DeepSeek	BFS+CG	7B	$4\times 2\times 4$	$4\times 4$	$4\times 4$	$75.4\pm 0.6$
	One-shot decomposition		$16\times 2\times 1$	$16\times 1$	$16\times 1$	$74.5\pm 0.3$

Table 2: Results on the miniF2F test set for different methods. All results are averaged over 5 random seeds.

Model	Method	Size	Budget	Success (%)
Kimina	Whole-proof	7B	32	$62.8\pm 0.8$
	Whole-proof		64	$65.1\pm 0.3$
	Agent (ours)		32	$64.3\pm 0.8$
	Agent (ours)		64	$\mathbf{66.9\pm 0.2}$
DeepSeek	Whole-proof	7B	32	$75.2\pm 0.5$
	Whole-proof		64	$76.3\pm 0.7$

Table 3: Results on miniF2F test set for different proof attempt budgets and methods. All results are averaged over 5 random seeds. Prover Agent is reproduced under our evaluation setting at a proof attempt budget of 260, since only at this budget does its full iterative-refinement pipeline execute.

Model	Method	Size	PAB	Success (%)
DeepSeek	Agent (critic only)	7B	32	$73.7\pm 0.7$
	Agent (critic only)		64	$74.2\pm 0.3$
	Agent (critic+reward)		32	$77.1\pm 0.3$
			64	$79.3\pm 0.4$
			128	$81.4\pm 0.2$
			256	$82.6\pm 0.1$

Table 4: Results on miniF2F test set for reward ablations. All results are averaged over 5 random seeds.

Model	Method	Size	PAB	#Solved
DeepSeek	Whole-proof	7B	32	9/659
DeepSeek	Whole-proof	7B	32 ∗	$\mathbf{13/659}$
			128	10/659
			128 ∗	$\mathbf{18/659}$
	Agent (ours)		32	16/659
			32 ∗	$\mathbf{27/659}$

Table 5: Results on PutnamBench for different methods and proof attempt budgets. Following prior PutnamBench evaluations, results are reported as a single benchmark run over all 659 problems

Model	Method	Size	PAB	Success (%)
Kimina	Whole-proof	7B	16	$25.2\pm 0.6$
Kimina	Agent (critic+reward)	7B	16	$\mathbf{27.5\pm 0.6}$
DeepSeek	Whole-proof	7B	16	$33.8\pm 0.5$
DeepSeek	Agent (critic+reward)	7B	16	$\mathbf{36.2\pm 0.6}$
Goedel	Whole-proof	8B	16	$31.9\pm 0.7$
Goedel	Agent (critic+reward)	8B	16	$\mathbf{33.8\pm 0.4}$

Table 6: Results on PhysLeandata test set. Results are averaged across 5 random seeds.

Model	Method	Success (%)
Kimina	Whole-proof	$9.3\pm 0.3$
	Whole-proof (w/ PhysLib)	$13.5\pm 0.7$
	Agent (ours, no PhysLib)	$11.5\pm 0.6$
	Agent (ours, w/ PhysLib)	$\mathbf{15.0\pm 0.7}$
DeepSeek	Whole-proof	$11.5\pm 0.2$
	Whole-proof (w/ PhysLib)	$14.5\pm 0.2$

Table 7: Results on LeanPhysBench (proof attempt budget (PAB@B) = 16). Results are averaged across 5 random seeds. The PhysLib library is directly passed as context. Critic+server rewards used for all our method configurations.

Model	Role/Method	Input	Output	Total
Goedel-Prover-V2-8B	Decomposer	1,438	1,449	2,887
	Critic	4,126	196	4,322
	Generator	4,231	203,580	207,811
	Whole-proof	117	317,420	317,537
DeepSeek-Prover-V2-7B	Decomposer	1,347	1,392	2,739
	Critic	4,021	187	4,208

Table 8: Role-level inference-token usage at PAB@32, averaged across five runs. Token counts are cumulative across all role completions in one complete benchmark run.

Model	Method	Success (%)
Kimina	Agent (ours, w/ temp. variation)	$\mathbf{64.3\pm 0.8}$
Kimina	Agent (ours, w/o temp. variation)	$62.5\pm 0.5$
DeepSeek	Agent (ours, w/ temp. variation)	$\mathbf{77.1\pm 0.3}$
DeepSeek	Agent (ours, w/o temp. variation)	$74.6\pm 0.3$
Goedel	Agent (ours, w/ temp. variation)	$\mathbf{84.2\pm 0.5}$
Goedel	Agent (ours, w/o temp. variation)	$81.9\pm 0.3$

Table 9: Results with and without temperature variation on miniF2F test set (proof attempt budget = 32; critic + server rewards used for all configurations). Results are averaged across 5 random seeds.

Generator	Decomposer	Critic	Success (%)
Goedel	Kimina	Kimina	$81.4\pm 0.4$
Goedel	Kimina	Goedel	$82.2\pm 0.5$
Goedel	Goedel	Kimina	$82.7\pm 0.4$
Goedel	DeepSeek	DeepSeek	$80.9\pm 0.3$
Goedel	Goedel	DeepSeek	$\mathbf{86.1\pm 0.3}$
Goedel	DeepSeek	Goedel	$83.8\pm 0.4$

Table 10: Multi-agent analysis with different models in different roles on miniF2F test set with sampling budget PAB@32. Results are averaged across 5 random seeds.

$N$	$K$	$S$	Success (%)	Rel. Wall-Clock
1	16	2	$82.1\pm 0.4$	$1.0\times$
2	8	2	$82.3\pm 0.3$	$1.2\times$
4 †	4	2	$\mathbf{84.2\pm 0.5}$	$1.5\times$
8	2	2	$83.7\pm 0.4$	$2.1\times$
16	1	2	$84.3\pm 0.2$	$2.8\times$

Table 11: Effect of the iteration–branching-factor allocation under a fixed proof-attempt budget on MiniF2F with Goedel-Prover-V2-8B. We fix

S=2

proof attempts per child and vary the number of MCTS iterations

N

and children per expansion

K

, such that

NKS=32

for all configurations. Wall-clock time is reported relative to the

N=1,K=16

configuration. Results are averaged over five random seeds.

Explore similar work

Oct 6, 2026

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.

Hanchao Zhou, Jialei Li

Automated Theorem Proving Lean Theorem Proving Efficient Language Model Reasoning

Ask PDF

May 11, 2026

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 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.

Zeynel A. Uluşan, Burak S. Akbudak, Can S. Erer +1

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

Ask PDF

Jun 8, 2026

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.

QuocViet Pham, Elvir Karimov, Andrey Galichin +1

Skolkovo Institute of Science and Technology · HSE University · Sberbank +1

Mathematical Reasoning Benchmarks LLM Evaluation Automated Theorem Proving Benchmark Design Lean Theorem Proving

Ask PDF