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

2025/07/11 by Ji, Xingguang, Liu, Yahui, Wang, Qi +7 · 9 citations
#Artificial Intelligence (cs.AI) #FOS: Computer and information sciences

paper · doi:10.48550/arxiv.2507.08649

Abstract

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.

Citations

• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
• Not All Rollouts are Useful: Down-Sampling Rollouts in LLM Reinforcement Learning
• ToolRL: Reward is All Tool Learning Needs
• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
• ReTool: Reinforcement Learning for Strategic Tool Use in LLMs
• Leanabell-Prover: Posttraining Scaling in Formal Reasoning
• DAPO: An Open-Source LLM Reinforcement Learning System at Scale
• Search-R1: Training LLMs to Reason and Leverage Search Engines with Reinforcement Learning
• R1-Searcher: Incentivizing the Search Capability in LLMs via Reinforcement Learning
• Offline RLAIF: Piloting VLM Feedback for RL via SFO
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
• STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
• Kimi k1.5: Scaling Reinforcement Learning with LLMs
• DeepSeek-R1 incentivizes reasoning in LLMs through reinforcement learning
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
• PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models
• LLM-based Rewriting of Inappropriate Argumentation using Reinforcement Learning from Machine Feedback
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
• BioXP-0.5B: Explainable Medical-AI via RL-GRPO
• Gorilla: Large Language Model Connected with Massive APIs
• Reflexion: Language Agents with Verbal Reinforcement Learning
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
• Toolformer: Language Models Can Teach Themselves to Use Tools
• Distributing Accountability, Not Capability: Phase Separation and the LLM Workflow Quadrant in Autonomous AI Agent Architectures
• TALM: Tool Augmented Language Models
• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• Reinforcement Learning for POMDP: Partitioned Rollout and Policy Iteration with Application to Autonomous Sequential Repair Problems
• Acting Less is Reasoning More! Teaching Model to Act Efficiently

Cited by

• Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
• IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
• Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
• Putting on the Thinking Hats: A Survey on Chain of Thought Fine-tuning from the Perspective of Human Reasoning Mechanism
• Autoformalizer with Tool Feedback
• EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty
• EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving
• Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
• StepFun-Prover Preview: Let's Think and Verify Step by Step
• Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs

Related

• Leanabell-Prover: Posttraining Scaling in Formal Reasoning
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
• Lean-STaR: Learning to Interleave Thinking and Proving
• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning