mlsanityData to 7 Oct 2026

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

arXiv 2608.18084 ↗First posted 4 Jun 2026cs.CL cs.PLcited by 0

Not on the map. Why?

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

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

Builds on

22 of 32 references.

References · 22

  1. 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,355
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  3. 2023Teaching Large Language Models to Self-Debugcited by 963
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  6. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  7. 2024When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMscited by 230
  8. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  9. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  10. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  11. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  12. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
10 more
  1. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  2. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  3. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  4. 2024InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Searchcited by 34
  5. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 9
  6. 2025RLMEval: Evaluating Research-Level Neural Theorem Provingcited by 6
  7. 2026Learning to Repair Lean Proofs from Compiler Feedbackcited by 6
  8. 2025The Debugging Decay Index: Rethinking Debugging Strategies for Code LLMscited by 5
  9. 2026LeanArchitect: Automating Blueprint Generation for Humans and AIcited by 5
  10. 2025Adaptive Proof Refinement with LLM-Guided Strategy Selectioncited by 4

Built on by

Not cited yet.