Research map / Large language models / Agents, code and math
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes APOLLO, a modular agentic pipeline that repairs LLM-generated Lean proofs using compiler feedback, sorry-based sub-lemma isolation, automated solvers, and recursive LLM re-invocation, reaching new miniF2F-test SOTA among sub-8B models.
Problem
Whole-proof generation with LLMs for formal theorem proving in Lean relies on many sampled proofs that are only binary-checked, wasting compiler feedback and requiring thousands of samples.
Approach
Use the Lean REPL's error messages to localize failing sub-lemmas, replace them with sorry, close easy goals with automated solvers, and recursively re-prompt the LLM on remaining sub-goals with small top-K budgets, then reassemble and reverify the proof.
Key results
- Apollo raises Goedel-V2-8B to 84.9% on miniF2F-test at sample budget ~63 (SOTA among sub-8B models per the paper).
- Apollo lifts Goedel-Prover-SFT from 64.7% to 65.6% on miniF2F-test while cutting samples from 25,600 to about 362 on average.
- o4-mini accuracy rises from 7.0% to 46.7% on miniF2F-test with Apollo (full module set, recursion depth 4).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Apply Apollo repair | Goedel-SFT · miniF2F-test | accuracy: 64.7% -> 65.6% | Helped |
| Apply Apollo repair | Kimina-Preview · miniF2F-test | accuracy: 70.8% -> 75.0% | Helped |
| Apply Apollo repair | Goedel-V2 · miniF2F-test | accuracy: 84.0% -> 84.9% | Helped |
| Apply Apollo repair | o3-mini · miniF2F-test | accuracy: 24.6% -> 40.2% | Helped |
| Apply Apollo repair | o4-mini · miniF2F-test | accuracy: 7.0% -> 46.7% | Helped |
| Apply Apollo repair | Kimina-Preview · PutnamBench | valid proofs: 10/658 -> 11/658 | Helped |
| Apply Apollo repair | Kimina-Preview · ProofNet | accuracy: 11.3% -> 18.3% | Helped |
| Add Syntax Refiner (ablation) | Apollo with o4-mini, without other modules · miniF2F-test | accuracy: 7.0% -> 7.4% | Helped |
| Add Syntax Refiner (ablation) | Apollo with Kimina-7B, without other modules · miniF2F-test | accuracy: 63.1% -> 63.1% | No clear effect |
| Add Auto Solver (ablation) | Apollo with o4-mini, without other modules · miniF2F-test | accuracy: 7.0% -> 7.0% | No clear effect |
| Add LLM Re-Invoker (ablation) | Apollo with Kimina-7B, without other modules · miniF2F-test | accuracy: 63.1% -> 69.3% | Helped |
| Add Syntax Refiner and Auto Solver (ablation) | Apollo with o4-mini, without LLM Re-Invoker · miniF2F-test | accuracy: 7.0% -> 20.5% | Helped |
Surprising findings
- Syntax Refiner and Auto Solver alone yield little gain; the largest gains come from combining Auto Solver with LLM re-invocation on sub-goals.
- Apollo-fixed proofs are at least twice as long on average as those the base model proves unaided.
Limitations
- Evaluation limited to whole-proof generation models; not integrated with tree-search provers.
- Performance depends on quality of the base model's initial proof sketch.
Experimental setup
Datasets: miniF2F PutnamBench ProofNet
Benchmarks: miniF2F-test PutnamBench ProofNet
Metrics: accuracy sample budget token budget
Baselines: Goedel-Prover-SFT Kimina-Prover-Preview-Distill-7B Goedel-V2 o3-mini o4-mini Hypertree Proof Search BFS-Prover STP RMaxTS Leanabell-GD-RL DeepSeek-R1-Distill-Qwen-7B
Builds on: Lean REPL Draft, Sketch, and Prove Baldur ReProver
Closest papers by meaning
- HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs (ICML 2026 · similarity 0.92)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.91)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.90)
- MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving (ICML 2025 · similarity 0.90)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.90)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.