PaperlayerView exact revision on arXiv

Source-linked AI summary

Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving

Zhuo Liu, Ding Yu, Hangfeng He

arXiv:2608.18084v1cs.CLcs.PL

TL;DR

Context-dependent Lean 4 theorem proving remains difficult, and independent sampling discards failed proofs that may contain useful partial progress. This paper introduces compiler-guided adaptive search combining dual-model exploration with current-best refinement, improving average pass rate by 12.8 percentage points while reducing LLM calls by 21.9% within pass@32.

  • Problem

    Project-level Lean proofs depend on surrounding context, while pass@k sampling treats the compiler as a final filter and discards potentially useful failed proofs.

  • Method

    The framework combines complementary dual-model proof generation with compiler-guided current-best refinement and stagnation-triggered resampling.

  • Results

    12.8 percentage points higher average pass rate and 21.9% fewer LLM calls than the two base models within the pass@32 budget.

  • Takeaways & Limitations

    The results suggest extending whole-proof generation beyond independent sampling toward adaptive search using compiler-grounded process signals to retain, refine, or abandon proof states.

  • Takeaways & Limitations

    The comparison module relies on an LLM judge that may not always reflect true proof progress.

Abstract

from arXiv · show

Theorem proving in real-world Lean 4 projects is challenging because proofs often depend on project-specific context. While iterative refinement can use compiler errors to repair failed proofs, reusing failed attempts requires careful search control: some proofs provide better starting points than others, and later revisions may degrade a partially correct proof. We propose a compiler-guided proof search framework that balances exploration and exploitation. It explores diverse starting points through dual-model generation and stagnation-triggered resampling, while exploiting promising proof states through current-best refinement guided by compiler-grounded pairwise comparison. Experiments on seven real-world Lean 4 projects from miniCTX-v2 show that our method achieves a better effectiveness--efficiency tradeoff than pass@k baselines. Within the pass@32 budget, our method improves average pass rate by 12.8 percentage points while reducing LLM calls by 21.9%.

1 Introduction

Project-level Lean theorem proving remains difficult because proofs depend on surrounding context, while independent sampling discards useful partial progress. The proposed framework addresses this exploration–exploitation challenge through complementary models, current-best refinement, and stagnation-triggered resampling.

  • Motivation: Project-level Lean proofs depend on local definitions, lemmas, naming conventions, and surrounding proof patterns, challenging even strong provers.These context dependencies distinguish real-world projects from simpler formal reasoning benchmarks.
  • Motivation: Independent sampling treats the compiler as a final filter, discarding failed proofs that may contain useful partial progress.The paper identifies this limitation of pass@k-style candidate generation.
  • Motivation: Revision can fix one error while introducing another or degrading a partially correct proof, making refinement sensitive to the starting proof.These failures motivate balancing exploration of new proofs with exploitation of promising intermediate states.
  • Method: The framework combines specialist and generalist models for exploration with current-best refinement and stagnation-triggered resampling.Specialist models provide precise tactic sequences, whereas generalist models better leverage project context but more often generate ill-typed tactics.
  • Evaluation: The framework is evaluated on seven Lean 4 projects from miniCTX-v2 and 84 formalization problems from RLMEval-FLT3, targeting a better pass rate–LLM call tradeoff.The paper also analyzes proof trajectories, emphasizing starting proofs and preservation of useful intermediate proof states.

2 Related Work

Prior work spans context-dependent theorem-proving benchmarks, whole-proof generation with verifier-guided repair, and tactic-level search. This work searches over whole-proof candidates, combining diverse generation with compiler-grounded refinement of promising proof states.

  • Context-dependent theorem proving: Context-dependent theorem proving targets proofs whose validity depends on surrounding project context, with miniCTX built from seven real-world Lean projects.RLMEval evaluates neural theorem proving and proof autoformalization on research-level Lean theorems from Lean Blueprint projects.
  • Whole-proof generation: Whole-proof systems generate complete proofs in one pass, and verifier- or compiler-guided repair uses failed attempts for later refinement.AlphaProof and AlphaGeometry achieved medal-level performance on IMO problems, while other systems repair failed complete proofs using verifier or compiler errors.
  • Positioning of this work: Unlike tactic-level search, this work searches over whole-proof candidates, using complementary models for diverse starting points and compiler-grounded comparison to preserve promising states.Its search combines exploration from multiple proof generators with refinement of promising proof states.
  • Tactic-level proof search: Tactic-level systems predict the next tactic from the current proof state and guide search with best-first, tree-search, or progress-based methods.Examples include AlphaZerostyle hypertree search, LeanProgress, and BFS-Prover’s preference optimization over state–tactic pairs with length normalization.

3 Compiler-Guided Adaptive Proof Search

The framework treats Lean proof generation as compiler-guided search over proof candidates, balancing exploration of diverse starting points with exploitation of a protected current-best proof. Dual-model resampling, structured compiler feedback, automatic solving, and pairwise comparison control refinement and restart when progress stagnates.

  • Search overview: The system maintains a single current-best proof state and alternates between exploration and exploitation.Exploration proposes starting points, while exploitation refines the current-best proof using compiler feedback.
  • Exploitation: Pairwise comparison selects stronger initial, refined, or resampled proofs based on compiler errors, progress, error severity, and proof strategy.Rejected proposals preserve the old current-best proof and increase the stagnation counter, whereas accepted proposals reset it.
  • Compiler guidance: Structured compiler errors are aligned to tactic lines and supplied to both the repair model and comparison controller.An AUTOSOLVE module can close trivial goals with deterministic tactics or builtin lemma search without any model call.
  • Exploration: Two complementary models provide diverse starting points: a generalist suited to project context and a specialist aligned with Lean syntax and tactics.Each candidate is verified immediately; if neither succeeds, pairwise comparison selects the initial current-best proof.
  • Search control: Starting-proof choice and refinement trajectories strongly affect success: some wrong proofs are repaired quickly, while others rarely succeed, and identical starts can diverge.These effects are reported as larger variation across starting proofs than across repeated runs from the same start, with different runs sometimes reaching success or drifting into failure.
  • Restart: When stagnation reaches threshold N, the system resamples from both models, verifies fresh candidates, selects a new current-best proof, and resumes refinement.Resampling both models exposes different proof strategies and helps avoid repeatedly exploring the same bad region.

4 Experimental Setup

The evaluation uses miniCTX-v2 and RLMEval-FLT3, with dual-model and ReAct-style baselines under standardized Lean 4 verification. It measures pass rate against average LLM calls per theorem, with additional dollar-cost analysis.

  • Benchmarks: miniCTX-v2 comprises seven real-world Lean 4 projects spanning different mathematical domains, proof styles, and dependency structures.Results are reported on its test split.
  • Benchmarks: FLT3 contains 84 theorems from a Lean 4 formalization of Fermat’s Last Theorem for n = 3, evaluated with all project lemmas available.Each theorem is paired with a natural-language proof, following RLMEval’s easy setting.
  • Models: DeepSeek-Prover-V2-7B serves as the specialist, while GPT-5-mini serves as generalist, repair model, and pairwise judge.These roles apply unless otherwise noted.
  • Baselines: Single-model baselines use standard pass@k with k independent candidates, whereas Dual_Model combines k samples from each model at a 2k-call budget.Success requires at least one verifying candidate.
  • Metrics: The main evaluation plots pass rate against average LLM calls per theorem to capture the effectiveness–efficiency tradeoff.Dollar costs are additionally broken down in Figure 4.
  • Implementation: The method interacts with Lean 4 through lean-interact, using low reasoning effort for the generalist and temperature 1 with top-p 0.95 for the specialist.The specialist settings encourage diverse proofs.

5 Results

The method achieves the strongest effectiveness–efficiency tradeoff across projects by combining exploration with compiler-guided exploitation. It also remains effective with informal proofs, an alternative model pairing, and lower average cost than GPT-5-mini pass@32.

  • Overall results: 12.8 percentage points: within pass@32, the method improves average pass rate over the two base models while reducing LLM calls by 21.9%.The method is consistently at or near the top of the pass-rate curve across projects.
  • Exploration and exploitation: Dual-model generation and stagnation-triggered resampling explore diverse candidates, while compiler-guided refinement exploits the current-best proof with structured error feedback.Dual-model generation already outperforms either single model, and the method continues improving at higher call budgets while CARLESON plateaus at 0.50 after about 16 calls.
  • Controller comparison: The method outperforms the ReAct-style baseline on every project despite using a simpler controller.The results suggest that explicit exploration–exploitation scheduling benefits context-dependent Lean proving.
  • Cost: $1.96: the method’s average cost versus $2.43 for GPT-5-mini pass@32, while achieving a higher pass rate.Comparison calls occur at similar frequency to generalist proof calls but are cheaper because they produce short decision outputs.
  • RLMEval-FLT3: 39.3% pass rate: on RLMEval-FLT3, the method reaches this result at 13.5 calls per theorem, exceeding Generalist pass@32 at 36.9% and Specialist pass@32 at 28.6%.Informal proofs are provided to the generation, refinement, and pairwise comparison modules.
  • Model pairing: 52.86% average pass rate: with Gemini-2.5-Flash replacing the generalist, the method outperforms both base models on every project under a 16-call budget.Results with an alternative generalist-specialist pair in Appendix D further confirm the finding.

6 Analysis

The analysis shows that performance comes from allocating calls across complementary generation, refinement, comparison, and restart stages, with each component improving search. Pairwise comparison preserves strong proof states amid unstable refinement, while N = K/4 balances restart timing.

  • Component contributions: Every ablation shifts the pass rate–LLM calls curve downward, showing that specialist generation, autosolve, resampling, and pairwise comparison each improve search.The gain therefore comes from call allocation across generation, refinement, comparison, and restart, not simply from making more model calls.
  • Pairwise comparison: Generalist proof calls increase from 6.54 to 10.08 per theorem without comparison, indicating that pairwise comparison improves proof-state selection.Comparison selects a better initial state and preserves stronger intermediate states, preventing weaker proposals from overwriting useful trajectories.
  • Preserved proof states: 50.4% of refinement proposals are rejected on average even on successful trajectories, showing that refinement frequently introduces errors or abandons promising directions.Without comparison, these unstable updates would overwrite the current proof state at every step.
  • Preserved proof states: 39.5% of solved trajectories ending after comparison are verified when comparison selects the existing current-best state rather than the newest refinement proposal.Successful refinement therefore depends not only on generating revisions but also on preserving useful proof states.
  • Complementary search stages: 30.37% of solved theorems are first found during refinement, while generalist and specialist generation contribute different solved cases.The decomposition indicates complementary search stages and recoverable partial progress after failed proofs.
  • Restart threshold: N = K/4 achieves the best restart balance, reaching 60.00% pass rate with 24.42 calls.Smaller N causes premature restarts and unnecessary resampling, whereas larger N delays needed restarts on exhausted trajectories.

7 Conclusion

The work presents adaptive proof search for context-dependent theorem proving by combining dual-model exploration with current-best refinement. It suggests extending whole-proof generation beyond independent sampling through compiler-grounded process signals.

  • The framework combines dual-model generation for exploration with current-best refinement for exploitation.This combination is designed to preserve and improve better proof states.
  • Adaptive proof search extends whole-proof generation beyond independent sampling.The conclusion frames this extension as a broader implication of the work.
  • Future provers may benefit from compiler-grounded process signals, rather than relying only on stronger prover training.

Limitations · A Algorithm

The paper identifies limitations in model specialization, tactic-level search, inference-time learning, and verifier-grounded process rewards. Algorithm 1 alternates exploration and refinement, with threshold N controlling the balance and current-best proofs updated through accepted proposals or resampling.

  • Limitations: The framework uses complementary models for generation and a generalist model for refinement, leaving larger or specialized model pools and role assignments for future study.Future work could study model assignments for generation, refinement, comparison, and resampling.
  • Limitations: The method searches at the whole-proof level rather than explicitly exploring tactic-level proof states.Future work could combine trajectory-level control with tactic-based search.
  • Limitations: The framework relies on pretrained inference-time LLMs and does not train models through multi-turn interaction with Lean feedback.Reinforcement learning or other verifier-guided interaction training methods remain future directions.
  • Limitations: The LLM judge used to keep or replace proof states may not always reflect true proof progress.Verifier-grounded process reward models could provide more reliable guidance for keeping, refining, or restarting proof trajectories.
  • A Algorithm: Algorithm 1 alternates exploration and refinement: resampling replaces the current-best proof with a fresh exploratory proof, while refinement changes it only after accepting a proposal.The procedure includes verification checks for generated, specified, and refined proofs.
  • A Algorithm: The threshold N controls switching frequency: smaller N encourages more exploration, whereas larger N allocates more budget to refinement.This threshold determines the search’s exploration–refinement balance.

B Analysis of Randomness in Iterative Refinement · C LLM Calls Breakdown

The analysis finds that starting-point quality contributes more to refinement variability than repeated stochastic reruns, while LLM-call usage is dominated by inexpensive pairwise comparisons and varies with project difficulty.

  • B Analysis of Randomness in Iterative Refinement: Each wrong-proof refinement run is repeated 5 times to separate starting-point effects from inherent stochasticity.The analysis measures variation across reruns of the same wrong proof and across different wrong proofs within each theorem.
  • B Analysis of Randomness in Iterative Refinement: Intra-WP std measures run-to-run randomness across reruns of one wrong proof.It is defined as the standard deviation of success iterations across multiple reruns of the same wrong proof.
  • B Analysis of Randomness in Iterative Refinement: Inter-WP std measures starting-point effects across different wrong proofs within the same theorem.It is defined as the standard deviation of success iterations across different wrong proofs within one theorem.
  • B Analysis of Randomness in Iterative Refinement: Failed runs without a verified proof within 32 iterations are assigned 32.This convention applies to runs that do not produce a verified proof within the iteration limit.
  • B Analysis of Randomness in Iterative Refinement: Heatmaps show that some starting points consistently fail across random seeds, whereas others succeed reliably.Entire rows marked with × indicate consistent failure for starting points such as WP4 and WP6, while WP9 succeeds reliably.
  • B Analysis of Randomness in Iterative Refinement: 3.36 average inter-WP std exceeds 2.41 average intra-WP std across 9 randomly chosen theorems with non-trivial variance.The comparison indicates that different starting points create more variation than repeated runs of the same starting point.
  • C LLM Calls Breakdown: Pairwise comparison calls comprise the largest share of LLM calls across all projects, but each judge call produces only a short binary decision.Their low cost contrasts with their high share of total calls.
  • C LLM Calls Breakdown: 8.4 calls on Seymour rises to over 31 on Carleson and ConNF, reflecting earlier resolution on Seymour and greater refinement needs on harder projects.These figures are the average number of LLM calls per theorem for each project.

D Alternative Model Pair: GPT5.4-mini and Goedel-Prover-V2-8B · E Implementation Details

With GPT5.4-mini and Goedel-Prover-V2-8B, the individual models plateau at 48% and 44%, whereas the method exceeds 56% on HepLean, supporting model-diverse exploration. The implementation uses lean-interact with cached Lean environments, AutoSolve tactics, robust pairwise-decision parsing, compiler-error extraction, and specified model hardware.

  • D Alternative Model Pair: GPT5.4-mini and Goedel-Prover-V2-8B: Model diversity benefits the complementary exploration strategy beyond the specific strengths of a single model pair.The alternative pair is formed by replacing both the generalist and specialist models.
  • D Alternative Model Pair: GPT5.4-mini and Goedel-Prover-V2-8B: Over 56% pass rate is reached by our method on HepLean with GPT5.4-mini as Generalist and Goedel-Prover-V2-8B as Specialist, while the individual models plateau at 48% and 44%.The generalist plateaus at 48% and the specialist at 44%; our method continues improving with additional calls.
  • E Implementation Details: lean-interact interfaces with the Lean 4 REPL, validating surrounding source context and caching an environment E for proof verification.Context validation uses timeout = 360, proof verification uses timeout = 120, and main results normally use a single run per method and budget.
  • E Implementation Details: Lean v4.16.0 is used for miniCTX-v2, while Lean v4.7.0-rc2 is used for RLMEval-FLT3.These versions define the Lean environments used for the two evaluation settings.
  • E Implementation Details: AutoSolve attempts to close each theorem before any LLM call using deterministic closers and library-search tactics whose suggestions are compiler-verified.Deterministic tactics include rfl, simp, omega, linarith, norm_num, ring, and decide; search-based tactics include exact? and hint.
  • E Implementation Details: Pairwise-judge outputs are parsed through cascading JSON, regex, single-character, and default-choice fallbacks.If all parsing methods fail, the system defaults to the current proof, choice A.
  • E Implementation Details: Compiler errors are aligned to tactic lines and formatted with surrounding context for the repair model and comparison judge.Each report contains one line of surrounding context and the error message, producing a compact line-level diagnostic.
  • E Implementation Details: The self-hosted specialist runs on a local server with two NVIDIA L40S GPUs, each with 48GB of memory, while the generalist is accessed through an API.The hardware configuration separates local specialist inference from API-based generalist access.

F Additional Analysis of Judge Behavior … I Artifact Use

The analysis finds that the judge conservatively filters refinements and moderately favors GPT5-mini when selecting between candidate proofs. The paper also specifies context-aware prompting, examines context length effects on success, and documents artifact use under relevant terms.

  • F Additional Analysis of Judge Behavior: 52.3% average keep-current rate across 294 refinement steps shows that the judge rejects roughly half of proposed refinements.This indicates moderately conservative refinement selection.
  • F Additional Analysis of Judge Behavior: 58.6% GPT5-mini selection rate across 391 pairwise comparisons indicates a moderate, consistent preference, strongest on FLT at 78.1% and HepLean at 71.1%.Comparisons occur when both GPT5-mini and DeepSeek-prover-v2 produce candidate proofs.
  • G Prompt Templates: Prompt templates include the theorem statement, surrounding Lean project context, and compiler feedback for refinement and comparison prompts.The templates cover proof generation, refinement, and pairwise comparison.
  • G.1 Specialist Proof Generation: Specialist proof generation asks Lean 4 to complete code with explanatory comments preceding each line.The prompt includes context and a declaration placeholder.
  • G.2 Generalist Proof Generation: Generalist proof generation supplies Lean 4 context and asks the model to prove the specified theorem.The prompt separates the context and theorem declaration.
  • G.3 Error-Guided Repair: Error-guided repair presents context, target theorem, an erroneous proof, and compiler errors, requesting only a corrected Lean 4 proof.The repair prompt uses the failed attempt and its errors as inputs.
  • G.4 Pairwise Proof Comparison: Pairwise proof comparison asks the model to choose between failed proofs using fixability, progress, and strategy.It requires a JSON response containing only choice A or B.
  • H Effect of Context Length on Success Rate: Across most projects, failures become more prevalent at longer contexts, especially in Carleson, where contexts exceeding 40k characters are predominantly unsolved.FLT and Seymour have compact contexts, whereas Carleson spans over 140k characters; the analysis uses max refinement K = 16.
Loading 2608.18084v1…