Research map / Large language models / Reasoning and chain of thought
MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving
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 MA-LoT, a prover-corrector model-collaboration framework in which a single Long-CoT Lean4 model (LoT-Solver) writes whole proofs and then corrects them from Lean verifier errors, trained via a system-prompt-based LoT-Transfer Learning pipeline without Long-CoT Lean data.
Problem
Single-LLM Lean4 theorem proving either relies on tree search (costly, lacking high-level NL planning) or whole-proof generation (no verifier feedback or error analysis), so neither balances NL reasoning with formal verification.
Approach
Separate proof writing (prover with NL plan in Long CoT) from error-driven correction (corrector using Lean error messages in Long CoT), and induce Lean-specific Long CoT in LLMs via LoT-Transfer Learning: general NL Long-CoT SFT, then Lean SFT and correction data trained with the Long-CoT switched off by system prompt and a placeholder, switched on at inference.
Key results
- MA-LoT with Godel-Prover reaches 61.07% on MiniF2F-Test, versus 55.33% for Godel-Prover (pass@32) and 50.70% for InternLM2.5-StepProver.
- DeepSeek-Prover + MA-LoT reaches 54.51% on MiniF2F-Test, beating its RL variant baseline (DeepSeek-Prover-v1.5-RL 48.36%).
- Corrector rounds fix on average 11.55% of theorems the prover failed on across the first three correction rounds (per the corrector study).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Apply MA-LoT instead of LoT whole-proof generation | DeepSeek-Prover · MiniF2F-Test | accuracy: 52.05% -> 54.51% | Helped |
| Apply MA-LoT instead of LoT whole-proof generation | Godel-Prover · MiniF2F-Test | accuracy: 57.79% -> 61.07% | Helped |
| Add corrector refinement rounds (ablation) | DS-Prover-v1.5 · MiniF2F-Test | accuracy: 51.64% -> 53.28% -> 54.51% -> 55.33% | Helped |
| Add corrector refinement rounds (ablation) | Godel-Prover-SFT · MiniF2F-Test | accuracy: 54.92% -> 59.43% -> 61.07% -> 61.89% | Helped |
| Use the prover as corrector instead of an expert corrector (ablation) | Godel-Prover-SFT · MiniF2F-Test | accuracy: 54.92% -> 56.15% -> 57.38% | Hurt |
| Switch off Long CoT at inference (ablation) | LoT-Solver · MiniF2F-Test | accuracy: 51.64% -> 49.18% | Hurt |
| Remove Long CoT training and fine-tune the RL model (ablation) | DeepSeek-Prover-v1.5-RL · MiniF2F-Test | accuracy: 48.36% vs 51.64% | Hurt |
| Add Long CoT training only (ablation) | DeepSeek-Prover-v1.5-SFT · MiniF2F-Test | accuracy: 46.31% -> 46.72% | No clear effect |
| Add SFT data after Long CoT training (ablation) | DeepSeek-Prover-v1.5-SFT · MiniF2F-Test | accuracy: 46.72% -> 50.00% | Helped |
| Add correction-data training after Long CoT and SFT training (ablation) | DeepSeek-Prover-v1.5-SFT · MiniF2F-Test | accuracy: 50.00% -> 51.64% | Helped |
| Increase LoT-Solver training steps (ablation) | LoT-Solver · MiniF2F-Test | accuracy: 32.79% -> 35.25% -> 45.08% -> 47.54% -> 51.64% | Helped |
| Apply MA-LoT instead of the base model at the reported efficiency-study budgets | Godel-Prover-SFT · MiniF2F-Test | accuracy: 58.20% -> 61.07% | Helped |
Surprising findings
- Using the prover model itself to correct proofs dropped performance, as it tended to repeat the wrong proof instead of analyzing the error.
- Training only on general NL Long-CoT data gave minimal improvement on Lean theorem proving (46.72% vs 46.31% base).
Limitations
- Evaluation is expensive (11 GPU days) because vLLM could not be used, forcing reduced-precision or slower inference; some baseline numbers were re-run and differ from originals.
- Long CoT increases token generation by 33% and GPU hours by 70% relative to the base model.
- Evaluated mainly on MiniF2F; ProofNet results are small-scale.
Experimental setup
Datasets: OpenO1-SFT-Pro DeepSeek-Prover-v1 dataset Lean-Workbook MiniF2F MATH
Benchmarks: MiniF2F-Test MiniF2F-Valid ProofNet
Metrics: accuracy (pass@k)
Baselines: InternLM2.5-StepProver Godel-Prover DeepSeek-Prover-v1.5-RL DeepSeek-V3 Lean-STaR Expert Iteration Llemma ReProver STP-Lean TheoremLlama GPT-4-Turbo Gemini-1.5-pro
Builds on: Lean4 DeepSeek-Prover-v1.5 Goedel-Prover OpenO1-SFT-Pro Expert Iteration
Closest papers by meaning
- Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · similarity 0.91)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.90)
- Lean Workbook: A large-scale Lean problem set formalized from natural language math problems (NeurIPS 2024 · similarity 0.89)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.89)
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data (ICLR 2024 · similarity 0.88)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.88)
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.