PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Bodla Krishna Vamshi, Haizhao Yang

arXiv:2608.28639v1cs.AIcs.LGcs.LO

TL;DR

Formal theorem proving with language models needs efficient search while preserving reliable, comparable evaluation. This paper introduces a three-role MCTS framework that uses Lean compilation as a scalar reward oracle and evaluates it across mathematics and physics benchmarks under matched budgets. It reports improved benchmark results alongside reward-hacking findings that motivate kernel-level proof auditing.

  • Problem

    Efficiently navigating large proof search spaces remains challenging, while compiler-feedback methods and non-standard protocols limit context efficiency or direct baseline comparison.

  • Method

    A three-role MCTS framework uses Lean compilation only as a scalar reward for UCB-guided search, with separate generator, decomposer, and critic roles.

  • Results

    Across four benchmarks, the method reaches 87.1% on MiniF2F at PAB@256 and solves 26/659 PutnamBench problems at PAB@32 versus 18/659 for whole-proof sampling.

  • Takeaways & Limitations

    Kernel-level auditing is necessary because compiled proofs can pass standard checks while depending on sorryAx, and the framework reduces inference tokens under matched budgets.

  • Takeaways & Limitations

    The primary comparison is restricted to whole-proof sampling on the same frozen checkpoint to isolate inference-time search effects.

Abstract

from arXiv · show

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.

Introduction

Formal theorem proving with language models remains difficult because efficient exploration of large proof spaces is unresolved. The proposed three-role MCTS framework separates compiler verification from generation and evaluates search under matched, frozen-checkpoint comparisons.

  • Efficiently exploring large proof search spaces remains a fundamental challenge in formal theorem proving.
  • The framework uses Lean 4 compilation exclusively as a scalar reward oracle, avoiding compiler-error text in generation contexts.Compiler and critic rewards are backpropagated for UCB-guided search.
  • Primary comparisons use whole-proof sampling with the same frozen prover checkpoint to isolate inference-time search effects.
  • The evaluation spans four mathematics and physics benchmarks, three prover models, and proof attempt budgets from PAB@16 to PAB@256.
  • 26/659 PutnamBench problems are solved at PAB@32 with Goedel-Prover-V2-8B, versus 18/659 for base sampling at the same budget.
  • 87.1% is achieved on MiniF2F with Goedel-Prover-V2-8B at PAB@256, with performance improving as proof attempt budget increases.
  • The study identifies reward hacking by DeepSeek-Prover-V2-7B and argues that kernel-level auditing is necessary for compiler-verified evaluation.Auditing removes exploit-dependent proofs while the paper reports these counts without attributing them to the search procedure.

Related work

Prior work includes whole-proof generation, retrieval and compiler-guided tree search, and broader MCTS methods for reasoning. Evaluation infrastructure has evolved from REPL-based interfaces toward parallel proof servers supporting large-scale search.

  • Early neural theorem proving generated complete proofs or tactics, with retrieval augmentation supplying relevant Mathlib premises.
  • Formal-proving tree search includes MCTS with learned value functions, context-sensitive compiler feedback, and sketch-based proof decomposition.
  • MCTS has also been applied to broader LLM reasoning through tree search, planning, and AlphaZero-style mathematical self-play.
  • Reward hacking occurs when agents exploit unintended reward patterns, including documented Lean compiler behavior producing invalid-looking successful proofs.
  • LeanDojo provides REPL-based Lean interaction, proof-state extraction, tactic execution, and premise retrieval for benchmark evaluation.
  • LeanInteract supports parallel proof evaluation, while PyPantograph connects to the Lean kernel through Python-native FFI bindings.
  • Kimina Lean Server supports high-throughput concurrent proof compilation through persistent Lean REPL instances.

Search Methods

The search design distinguishes verification from generation: compiler results become scalar rewards rather than textual feedback, while search proceeds over natural-language proof plans.

  • The method treats the Lean verifier exclusively as a reward oracle, propagating scalar rewards through MCTS without inserting compiler messages into the LLM context.

Method

The framework combines three specialized roles with MCTS over natural-language proof-plan states, using UCB selection, temperature-decayed subgoal expansion, dual rewards, and backpropagation to allocate proof attempts.

  • Architecture: The search uses a generator, decomposer, and critic coordinated by MCTS over natural-language proof-plan states rather than formal Lean proof states.The tree starts from the original theorem and represents subgoal states by depth and child index.
  • Selection: UCB selection chooses child nodes using empirical rollout reward, visit counts, and an exploration constant, with unvisited nodes receiving infinite exploration value.Traversal continues until a terminal or incompletely expanded leaf is reached.
  • Expansion: Each expanded node generates K=4 natural-language child subgoals from the theorem and root-to-node trajectory, with temperature decayed by depth and iteration.The schedule starts at τ0=0.7, encouraging broad exploration early and more focused sampling later; removing decay degrades performance in ablations.
  • Evaluation: Each child receives a combined rollout reward rt = rc + rs from critic quality scores and normalized compiler success counts.The critic averages five low-temperature evaluations, while the server reward counts compiling, sorry-free attempts without feeding compiler messages into generation.
  • Backpropagation: MCTS backpropagates rollout rewards and visit updates along the selected path, enabling later UCB iterations to allocate effort across promising and underexplored subtrees.With N iterations and K×S rollouts per iteration, the proof-attempt budget is PAB@B = N × K × S = 4 × 4 × S.

Results

Across matched frozen-checkpoint comparisons, the framework outperforms whole-proof sampling on mathematical and physics benchmarks while also exceeding a compiler-feedback baseline on MiniF2F at a comparable budget.

  • Evaluation setup: The evaluation uses three specialized prover models across four benchmarks, with results averaged over 5 random seeds and matched proof-attempt budgets.Baselines use identical frozen checkpoints, prompts, and decoding configurations, differing only in search mechanism.
  • MiniF2F: 84.2 ± 0.5% at PAB@32 on MiniF2F with Goedel-Prover-V2-8B exceeds whole-proof sampling at 82.4%.The framework consistently outperforms whole-proof sampling across all three models at matched MiniF2F budgets.
  • MiniF2F: 87.1 ± 0.2% at PAB@256 on MiniF2F exceeds Prover Agent’s 86.2 ± 0.1% at its native sample budget of 260.Prover Agent uses direct compiler-error feedback in context, whereas this framework uses an oracle-only signal.
  • PutnamBench: 26/659 PutnamBench problems at PAB@32 and 36/659 at PAB@128 exceed whole-proof sampling’s 18/659 and 22/659, respectively.The comparison uses the same Goedel-Prover-V2-8B model.
  • Physics benchmarks: On PhysLeandata and LeanPhysBench, the method consistently outperforms whole-proof sampling at PAB@16 across all three models.Reported gains are +1.9% to +2.4% on PhysLeandata and +1.5% to +2.0% on LeanPhysBench with PhysLib context.

Inference-token efficiency

The framework reduces inference-token usage while maintaining strict proof-attempt matching, and its search quality depends on allocating iterations and branching carefully. Auditing also shows that compiled successes can depend on sorryAx, especially for DeepSeek-Prover-V2-7B on PutnamBench.

  • Inference-token efficiency: 32.84% lower total token consumption and 35.83% lower output-token generation are achieved on average across the three models than with whole-proof sampling.The reductions persist despite additional decomposer and critic computations under identical deployment settings.
  • Adaptive decomposer temperature: Removing temperature decay lowers performance across all three models, including a −2.3% drop for Goedel-Prover-V2-8B.The reported drops are −1.8% for Kimina-Prover-7B and −2.5% for DeepSeek-Prover-V2-7B.
  • Role assignment: 86.1 ± 0.3% is achieved with DeepSeek-Prover-V2-7B as critic, but changing the decomposer or both supporting roles can reduce performance.The heterogeneous critic improves over the homogeneous configuration by 1.9 percentage points, whereas using DeepSeek-Prover-V2-7B as both decomposer and critic reaches only 80.9 ± 0.3%.
  • Iteration–branching allocation: 84.2% success is reached with N = 4, K = 4, outperforming shallow configurations with the same fixed proof-attempt budget.N = 1, K = 16 and N = 2, K = 8 achieve 82.1% and 82.3%, respectively.
  • Iteration–branching allocation: 0.1 percentage points separate N = 16, K = 1 from N = 4, K = 4, while the narrowest configuration requires 2.8× the wall-clock time of N = 1, K = 16.Further increasing iterations therefore yields diminishing returns and exposes an accuracy–latency trade-off.
  • Kernel-level proof auditing: 11 and 19 MCTS solutions are removed at PAB@32 and PAB@128 after auditing DeepSeek-Prover-V2-7B proofs for sorryAx dependence on PutnamBench.Whole-proof sampling loses 4 and 8 solutions at the same budgets; successful exploit-dependent proofs are observed only for this model and benchmark.

Implementation details

The implementation pins a common evaluation environment, standardizes prompts and decoding, supplies physics-library context where applicable, and audits compiled proofs at the axiom level. The three roles use distinct prompting and decoding configurations, while exploit classification relies on sorryAx dependencies rather than lexical indicators alone.

  • Reproduction protocol: All baselines are rerun under a pinned Lean 4.15.0, Mathlib v4.15.0, and Kimina Lean Server 2.0.0 environment.The authors note that toolchain and prompt differences can materially change reported performance.
  • Physics context: LeanPhysBench is evaluated both with and without PhysLib, while applying the contrast identically to whole-proof sampling and MCTS.The with-PhysLib condition matches the original benchmark setting; the no-PhysLib condition tests proof generation without domain-specific definitions.
  • Prompting: The same prompt template is used across three prover models and four benchmarks, with theorem, trajectory, and domain-library fields substituted at inference time.The prompt templates differ by agent role, including generator, decomposer, and critic instructions.
  • Proof auditing: The audited example compiles and passes a sorry-token scan, but #print axioms reveals sorryAx and removing the flagged apply? branch makes compilation fail.This demonstrates why source-level scans can miss unproved obligations admitted through the documented Lean 4.9.0 interface behavior.

Datasets

The evaluation spans four Lean 4 benchmarks covering competition mathematics, undergraduate mathematics, college-level physics, and graduate-level theoretical physics. LeanPhysBench is additionally tested with and without its accompanying physics library context.

  • Benchmark suite: The study evaluates four publicly available Lean 4 benchmarks spanning competition mathematics and college- to graduate-level physics.The benchmark suite includes MiniF2F, PutnamBench, LeanPhysBench, and PhysLeanData.
  • Mathematics benchmarks: MiniF2F contains 244 competition problems spanning algebra, number theory, geometry, inequalities, combinatorics, induction, and analysis.Its problems are drawn from contests including the IMO and AIME.
  • Mathematics benchmarks: PutnamBench contains formally verified undergraduate theorems across algebra, analysis, geometry, combinatorics, number theory, and linear algebra.It is built from the William Lowell Putnam Mathematical Competition.
  • Physics benchmarks: LeanPhysBench contains formally verified college-level physics problems across mechanics, waves, electromagnetism, thermodynamics, and optics.The evaluation follows the benchmark protocol with and without the accompanying PhysLib context.
  • Physics benchmarks: PhysLeanData provides an out-of-distribution evaluation of graduate-level theoretical physics formalizations, including relativity, quantum mechanics, and quantum field theory.It also covers classical particle mechanics, classical string theory, and related advanced domains.

Conclusion and Limitations

The paper reports that reward-oracle MCTS improves matched-budget theorem-proving performance while reducing inference-token use, and that exhaustive axiom auditing exposes sorryAx-dependent successes. Its conclusions remain scoped to the evaluated models and benchmarks, with broader validation needed.

  • Conclusion: 87.1% on MiniF2F at PAB@256 is achieved by the proposed MCTS with Goedel-Prover-V2-8B, while using 32.8% fewer total inference tokens on average than whole-proof sampling.The reported gains are attributed to temperature-decayed decomposition and distributing budgets across multiple MCTS iterations.
  • Limitations and auditing: The exhaustive audit runs #print axioms on every successfully compiled proof across models, benchmarks, methods, and budgets, revealing sorryAx-dependent DeepSeek-Prover-V2-7B successes on PutnamBench.The audit is not limited to proofs containing previously reported lexical indicators.
  • Limitations and auditing: Kernel-level auditing is necessary for compiler-verified evaluation because some proofs compile and pass source-level sorry scans while depending on sorryAx.The paper reports the audited counts without attributing them to the search procedure.
Loading 2608.28639v1…