mlsanityData to 14 Oct 2026

Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning

arXiv 2507.08649 ↗First posted 11 Jul 2025cs.AIcited by 27

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

We introduce our Leanabell-Prover-V2, a 7B large language models (LLMs) that can produce formal theorem proofs in Lean 4, with verifier-integrated Long Chain-of-Thoughts (CoT). Following our previous work Leanabell-Prover-V1, we continual to choose to posttrain existing strong prover models for further performance improvement. In our V2 version, we mainly upgrade the Reinforcement Learning (RL) with feedback provided by the Lean 4 verifier. Crucially, verifier feedback, such as indicating success or detailing specific errors, allows the LLM to become ``self-aware'' of the correctness of its own reasoning process and learn to reflexively correct errors. Leanabell-Prover-V2 directly optimizes LLM reasoning trajectories with multi-turn verifier interactions, together with feedback token masking for stable RL training and a simple reward strategy. Experiments show that Leanabell-Prover-V2 improves performance by 3.2% (pass@128) with Kimina-Prover-Preview-Distill-7B and 2.0% (pass@128) with DeepSeek-Prover-V2-7B on the MiniF2F test set. The source codes, curated data and models are available at: https://github.com/Leanabell-LM/Leanabell-Prover-V2.

Key facts. Cited by 27 papers in the map (data through 14 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 25 of its 39 references that are in the map. First posted on arXiv 11 Jul 2025.

Builds on

25 of 39 references.

Closest ancestors · 6

Same direction, newest first

  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition30 Apr
  2. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning15 Apr
  3. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoning8 Apr
  4. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan
  5. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts3 Jul
  6. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models5 Feb

Other references · 19

  1. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,330
  2. 2025DAPO: An Open-Source LLM Reinforcement Learning System at Scalecited by 2,810
  3. 2025Search-R1: Training LLMs to Reason and Leverage Search Engines with Reinforcement Learningcited by 1,444
  4. 2025Kimi k1.5: Scaling Reinforcement Learning with LLMscited by 1,210
  5. 2025ReTool: Reinforcement Learning for Strategic Tool Use in LLMscited by 392
  6. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  7. 2025ToolRL: Reward is All Tool Learning Needscited by 362
  8. 2025R1-Searcher: Incentivizing the Search Capability in LLMs via Reinforcement Learningcited by 336
  9. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  10. 2022TALM: Tool Augmented Language Modelscited by 197
  11. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  12. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
7 more
  1. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  2. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  3. 2025Not All Rollouts are Useful: Down-Sampling Rollouts in LLM Reinforcement Learningcited by 84
  4. 2025Acting Less is Reasoning More! Teaching Model to Act Efficientlycited by 80
  5. 2024Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Modelscited by 73
  6. 2024LLM-based Rewriting of Inappropriate Argumentation using Reinforcement Learning from Machine Feedbackcited by 7
  7. 2025Offline RLAIF: Piloting VLM Feedback for RL via SFOcited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 14; 2026: 13.

27 papers.

Sort:

By area:

  1. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 205
  2. 2025A Survey of Reinforcement Learning for Large Reasoning Modelscited by 180
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  4. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 44
  5. 2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 22
  6. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 16
  7. 2025StepFun-Prover Preview: Let's Think and Verify Step by Stepcited by 13
  8. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficultycited by 7
  9. 2025Autoformalizer with Tool Feedbackcited by 7
  10. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 7
  11. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 7
  12. 2026Process-Verified Reinforcement Learning for Theorem Proving via Leancited by 7
15 more
  1. 2025Conflict-Aware Fusion: Mitigating Logic Inertia in Large Language Models via Structured Cognitive Priorscited by 5
  2. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 5
  3. 2026Scaling Large Reasoning Models beyond Human Supervision: A Path toward Superintelligencecited by 5
  4. 2025Putting on the Thinking Hats: A Survey on Chain of Thought Fine-tuning from the Perspective of Human Reasoning Mechanismcited by 4
  5. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 4
  6. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematicscited by 4
  7. 2025IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touchcited by 3
  8. 2025EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Provingcited by 1
  9. 2025Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Trainingcited by 1
  10. 2026GDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learningcited by 1
  11. 2026Internalizing Agency from Reflective Experiencecited by 1
  12. 2026A Theoretical Framework for Self-Play Theorem Proving Algorithmscited by 1
  13. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  14. 2026ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Provingcited by 0
  15. 2026Let the Library Speak: Self-Advertised Method Selection for Formal Provingcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Theorem Prover as a Judge for Synthetic Data Generation
  2. 2025VerifyBench: A Systematic Benchmark for Evaluating Reasoning Verifiers Across Domains
  3. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  4. 2026FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
  5. 2026Distilling LLM Feedback for Lean Theorem Proving
  6. 2025Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
  7. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
  8. 2024Lean-STaR: Learning to Interleave Thinking and Proving