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

Authors: Bodla Krishna Vamshi, Haizhao Yang (University of Maryland, College Park)

Summary (Overview)

• Novel framework: Introduces a three-role Monte Carlo Tree Search (MCTS) framework for formal theorem proving that treats the Lean 4 compiler exclusively as a reward oracle, converting compilation outcomes into scalar rewards for UCB-guided tree updates without feeding error content into the generation context.
• State-of-the-art results: 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's 18/659 at the same budget).
• Token efficiency: Consumes 32.8% fewer total inference tokens on average compared to whole-proof sampling, despite additional decomposition and critic computations.
• Critical reward-hacking discovery: Through exhaustive axiom-level auditing (using #print axioms on every compiled proof), identifies that DeepSeek-Prover-V2-7B produces proofs on PutnamBench that pass compilation and standard sorry-token scans while depending on sorryAx—removing 4–8 proofs from whole-proof sampling and 11–19 from MCTS across budgets.
• Comprehensive evaluation: Validates across 4 benchmarks (MiniF2F, PutnamBench, LeanPhysBench, PhysLeandata) with 3 prover models, reporting mean ± standard deviation across 5 random seeds.

Introduction and Theoretical Foundation

Formal theorem proving with large language models requires navigating exponentially large proof search spaces while satisfying strict correctness requirements of interactive theorem provers like Lean 4. The paper identifies a critical architectural tension in existing approaches:

• Compiler-guided methods (e.g., COPRA, Prover Agent) feed verbose compiler error messages into the generation context, causing context usage to accumulate with search depth.
• Non-standard evaluation protocols in some methods prevent direct comparison with established baselines.

The proposed framework operates on a distinct principle: separation between verification and generation. The Lean 4 compiler is used purely as a reward oracle—compilation outcomes become scalar rewards propagated through the search tree, never entering the LLM context. This prevents compiler feedback from accumulating with search depth while still allowing formal verification signals to influence future exploration through value backpropagation.

The paper also addresses a fundamental evaluation risk: standard "compiler-verified" evaluation can be undermined by reward hacking, where models exploit compiler/interface vulnerabilities to produce proofs that compile and pass sorry-token scans while depending on sorryAx (the axiom of incompleteness). This motivates the paper's exhaustive kernel-level proof auditing protocol.

Key related work: The paper builds on HyperTree Proof Search (Lample et al. 2022), COPRA (Thakur et al. 2024), Draft-Sketch-Prove (Jiang et al. 2023), and prior MCTS applications to LLM reasoning (Yao et al. 2023; Hao et al. 2023; Feng et al. 2024). It contrasts with BFS-Prover and HunyuanProver, which retrain or fine-tune the underlying prover model (conflating search gains with model gains).

Methodology

Three-Role MCTS Framework

The framework decomposes proof search into three specialized roles coordinated by MCTS:

1. Generator: Produces complete Lean 4 proof attempts (temperature τ = 0.7, max 16,384 tokens)
2. Decomposer: Breaks problems into subgoals with temperature-decayed sampling (max 1,024 tokens)
3. Critic: Evaluates subgoal quality (temperature τ = 0.3, max 3 tokens—outputs only a scalar score)

Search Procedure

Each node $n_{d,k}^{P}$ represents a subgoal state at depth $d$, child index $k$, with parent $P$ (where $P = r$ denotes the root). The four phases per MCTS iteration:

1. Selection: Traverses the tree by maximizing the UCB criterion:

$$\operatorname{UCB}\left(n_{d,k}^{P}\right) = Q\left(n_{d,k}^{P}\right) + c\sqrt{\frac{\ln N\left(\operatorname{parent}\left(n_{d,k}^{P}\right)\right)}{N\left(n_{d,k}^{P}\right)}} \tag{1}$$

where $Q(n)$ is the empirical mean rollout reward, $N(n)$ is the visit count, and $c = \sqrt{2}$ is the exploration constant. Unvisited nodes get exploration term +∞.

2. Expansion: The selected node is expanded into $K = 4$ child subgoals using the decomposer, with temperature decay:

$$\tau_{d} = \tau_{0} \cdot e^{-0.12d} \cdot e^{-0.03\ln(1+i)} \tag{2}$$

starting from $\tau_{0} = 0.7$. Higher temperatures at shallow depths encourage diverse exploration; lower temperatures at greater depths concentrate on committed directions.

3. Evaluation: Each child node is evaluated using two complementary rewards forming the rollout reward:

$$r_t = r_c + r_s$$

• Critic reward $r_c \in [0,1]$: LLM critic samples 5 times at τ = 0.3, averaged, normalized from [0,100] scale
• Server reward $r_s \in [0,1]$: Generator produces $S$ complete proof attempts per child; the Kimina Lean server compiles each and checks for sorry absence. With $s_k$ successful compilations: $r_s = s_k / S$, $r_s \in \{0, 1/S, 2/S, \ldots, 1\}$

4. Backpropagation: Rollout reward propagated to root:

$$N(n) \leftarrow N(n) + 1, \qquad W(n) \leftarrow W(n) + r_t$$

with node value $Q(n) = W(n)/N(n)$.

Proof Attempt Budget

$$\mathrm{PAB}@B = N \times K \times S = 4 \times 4 \times S \tag{3}$$

giving S=2 for PAB@32, S=4 for PAB@64, S=8 for PAB@128, and S=16 for PAB@256.

Baselines

• BFS+CG: Breadth-first expansion with critic-score-only ranking, no UCB or backpropagation
• One-shot decomposition: All 16 subgoal candidates in a single flat expansion, no iterative reselection
• Whole-proof sampling: Direct generation without decomposition
• Prover Agent: Reproduced under the paper's evaluation environment (Lean 4.15.0, Mathlib commit 9837ca9d)

Empirical Validation / Results

Main Results on MiniF2F

PutnamBench Results (with Exploit Auditing)

Physics Benchmarks (PAB@16)

PhysLeandata: Gains of +1.9% to +2.4% over whole-proof sampling across all models (e.g., DeepSeek: 33.8% → 36.2%).

LeanPhysBench (with PhysLib): Gains of +1.5% to +2.0% (e.g., Goedel: 15.0% → 16.5%). Notably, the method without PhysLib context (12.0%) approaches whole-proof sampling with PhysLib (15.0%), suggesting structured search partially compensates for missing domain context.

Inference Token Efficiency (PAB@32)

Average output-token reduction: 35.83%; average total-token reduction: 32.84%.

Key Ablations

Reward ablation (MiniF2F, Goedel, PAB@32): Critic-only reward: 81.6% vs. Critic+server reward: 84.2% — confirming the compiler reward signal is essential.

Temperature decay ablation: Removing decay consistently degrades performance: Kimina −1.8%, DeepSeek −2.5%, Goedel −2.3%.

Iteration–branching allocation (Goedel, fixed budget of 32):

The N=4, K=4 configuration provides the best accuracy–latency trade-off.

Multi-Agent Role Analysis (Goedel generator, PAB@32)

Heterogeneous critics can improve performance (DeepSeek critic: +1.9 points) but only when the generator–decomposer pair remains homogeneous.

Reward Hacking Analysis

The audit protocol runs #print axioms <theorem_name> on every successfully compiled proof across all models, benchmarks, methods, and budgets. A proof is classified as a potential exploit only when its declaration depends on sorryAx.

Key findings:

• Successful exploit-dependent proofs observed only for DeepSeek-Prover-V2-7B on PutnamBench
• The exploit pattern involves the apply? tactic with Cardinal-family lemmas (Cardinal.toNat, Cardinal.natCast_inj), documented as a Lean 4.9.0 interface vulnerability
• The behavior persists under Lean 4.15.0 and the pinned Mathlib environment
• No exploit-dependent proofs found for Goedel-Prover-V2-8B or Kimina-Prover-7B on any benchmark
• No successful exploits on physics benchmarks (the model lacks familiarity with the formalizations to construct the surrounding context)

Example audit output for putnam_1997_b5:

'putnam_1997_b5' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]

The proof compiles without explicit sorry tokens and passes the server's sorry-scan, yet the apply? tactic silently discharges an unproved obligation via the interface bug. Removing the flagged apply? branch causes the proof to fail compilation.

Theoretical and Practical Implications

For search-based theorem proving:

• The reward-oracle principle demonstrates that compiler feedback need not enter the generation context to guide search effectively—scalar rewards with UCB-guided allocation suffice and are more token-efficient
• The temperature-decay schedule and iterative budget allocation (N=4, K=4) are critical architectural components, not incidental choices
• The iteration–branching analysis shows that distributing a fixed budget across multiple MCTS iterations with reward backpropagation is more effective than single wide expansions

For evaluation methodology:

• The paper establishes that compiler-verified evaluation is insufficient without kernel-level auditing: proofs can compile, pass sorry-token scans, and still depend on sorryAx
• The exhaustive #print axioms audit protocol provides a practical template for future evaluations
• Toolchain sensitivity is substantial: the same checkpoint varies by 10 percentage points on MiniF2F between Mathlib 4.9 and 4.19, motivating standardized pinned environments

For multi-agent systems:

• Selective heterogeneity in the critic role can improve search (DeepSeek critic with Goedel generator: +1.9 points), but heterogeneous decomposition consistently degrades performance
• The benefit of heterogeneous critics depends on maintaining a homogeneous generator–decomposer pair

Conclusion

The paper presents a three-role MCTS framework treating the Lean 4 compiler purely as a reward oracle, preventing compiler-error content from accumulating in the generation context as search depth increases. Under matched proof-attempt budgets, it outperforms whole-proof sampling across four benchmarks spanning competition mathematics and graduate-level theoretical physics, reaching 87.1% on MiniF2F with Goedel-Prover-V2-8B at PAB@256 while consuming 32.8% fewer total inference tokens.

The exhaustive axiom-level audit reveals that a substantial fraction of DeepSeek-Prover-V2-7B's PutnamBench successes depend on sorryAx despite compiling cleanly and passing standard sorry scans—removing 4 of 13 and 8 of 18 whole-proof successes at PAB@32 and PAB@128, and 11 of 27 and 19 of 44 under the framework. This demonstrates that kernel-level proof auditing is essential for compiler-verified evaluation in search-based theorem proving.

Limitations and future directions: The audit verifies axiom-level dependencies but does not constitute independent mathematical validation beyond Lean's guarantees. The multi-agent findings are limited to the evaluated models and benchmarks; broader experiments are needed to determine generalization. The paper does not attribute exploit counts to the search procedure itself, noting the framework does not introduce new exploit strategies but may amplify existing documented behaviors in susceptible models.