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

arXiv: https://arxiv.org/abs/2608.18084 · HTML: https://mlsanity.com/paper/2608.18084/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 22 of its 32 references that are in the map.
- First posted on arXiv 4 Jun 2026.

## Builds on (most cited first, 22 of 22)

- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMs](https://mlsanity.com/paper/2406.01297/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://mlsanity.com/paper/2507.15225/) (2025)
- [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://mlsanity.com/paper/2410.15700/) (2024)
- [LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction](https://mlsanity.com/paper/2502.17925/) (2025)
- [RLMEval: Evaluating Research-Level Neural Theorem Proving](https://mlsanity.com/paper/2510.25427/) (2025)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [LeanArchitect: Automating Blueprint Generation for Humans and AI](https://mlsanity.com/paper/2601.22554/) (2026)
- [The Debugging Decay Index: Rethinking Debugging Strategies for Code LLMs](https://mlsanity.com/paper/2506.18403/) (2025)
- [Adaptive Proof Refinement with LLM-Guided Strategy Selection](https://mlsanity.com/paper/2510.25103/) (2025)

## Abstract (arXiv)

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