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

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
Oct 6, 2026Hanchao Zhou, Jialei LiAutomated Theorem Proving Lean Theorem Proving
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
TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
Jun 8, 2026QuocViet Pham, Elvir Karimov, Andrey Galichin +1Mathematical Reasoning Benchmarks LLM Evaluation
Skolkovo Institute of Science and Technology · HSE University · Sberbank +1

Oct 6, 2026J/K move · Enter open · S save

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

Hanchao Zhou, Jialei Li

Automated Theorem Proving Lean Theorem Proving Efficient Language Model Reasoning

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

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

FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics