用验证器反馈训练大模型，自动修正证明错误。
Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
- 引入验证器反馈强化学习，让模型自知推理对错。
- 在MiniF2F上提升3.2%（pass@128），优于前代模型。
- 适合形式化证明、程序验证等严谨领域研究者。
我们提出Leanabell-Prover-V2，一个70亿参数的大语言模型，可在Lean 4中生成形式化定理证明，采用集成验证器的长链式思维（CoT）方法。延续此前工作，我们通过持续预训练进一步提升强证明模型性能。在V2版本中，主要改进基于Lean 4验证器提供的反馈进行强化学习。关键在于，验证器反馈（如成功提示或具体错误信息）使LLM能“自我觉察”其推理正确性，并主动修正错误。该模型通过多轮验证交互直接优化推理轨迹，结合反馈掩码实现稳定强化学习训练与简单奖励策略。实验表明，在MiniF2F测试集上，相较于Kimina-Prover-Preview-Distill-7B提升3.2%（pass@128），相比DeepSeek-Prover-V2-7B提升2.0%。代码、数据与模型已开源：https://github.com/Leanabell-LM/Leanabell-Prover-V2。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。