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

📄 arXiv: 2507.08649v1 📥 PDF

作者: Xingguang Ji, Yahui Liu, Qi Wang, Jingyuan Zhang, Yang Yue, Rui Shi, Chenxi Sun, Fuzheng Zhang, Guorui Zhou, Kun Gai

分类: cs.AI

发布日期: 2025-07-11

备注: 23 pages, 13 figures

🔗 代码/项目: GITHUB

💡 一句话要点

Leanabell-Prover-V2：通过强化学习和验证器集成推理，提升形式化定理证明能力

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化定理证明 强化学习 大型语言模型 验证器集成 自我纠错

📋 核心要点

  1. 现有形式化定理证明方法依赖人工设计规则或符号搜索，难以处理复杂定理，且泛化性不足。
  2. Leanabell-Prover-V2利用验证器反馈的强化学习，使LLM具备自我纠错能力，优化推理轨迹。
  3. 实验结果表明，Leanabell-Prover-V2在MiniF2F测试集上，相比现有模型性能提升了2.0%-3.2% (pass@128)。

📝 摘要（中文）

本文介绍了Leanabell-Prover-V2，一个70亿参数的大型语言模型（LLM），它能够使用Lean 4生成形式化定理证明，并集成了验证器反馈的长链思维（CoT）。延续之前的工作Leanabell-Prover-V1，本文继续选择对现有的强大证明器模型进行后训练，以进一步提高性能。V2版本主要升级了强化学习（RL），利用Lean 4验证器提供的反馈。至关重要的是，验证器反馈（例如指示成功或详细说明特定错误）使LLM能够“自我感知”其自身推理过程的正确性，并学习反身纠正错误。Leanabell-Prover-V2通过多轮验证器交互直接优化LLM推理轨迹，同时采用反馈token掩码来实现稳定的RL训练和简单的奖励策略。实验表明，在MiniF2F测试集上，Leanabell-Prover-V2使用Kimina-Prover-Preview-Distill-7B时性能提高了3.2%（pass@128），使用DeepSeek-Prover-V2-7B时性能提高了2.0%（pass@128）。源代码、整理的数据和模型可在https://github.com/Leanabell-LM/Leanabell-Prover-V2获取。

🔬 方法详解

问题定义：论文旨在解决形式化定理证明中，现有方法难以有效利用反馈信息进行自我纠错，导致证明效率和成功率受限的问题。现有方法通常依赖人工设计的规则或符号搜索，缺乏从错误中学习的能力，难以处理复杂定理，泛化性较差。

核心思路：论文的核心思路是利用Lean 4验证器提供的反馈信息，通过强化学习训练LLM，使其能够“自我感知”推理过程的正确性，并学习反身纠正错误。通过多轮验证器交互，LLM可以不断优化推理轨迹，提高证明的成功率。

技术框架：Leanabell-Prover-V2的技术框架主要包含以下几个模块：1) LLM推理模块：负责生成定理证明的步骤；2) Lean 4验证器：用于验证LLM生成的证明步骤是否正确，并提供反馈信息；3) 强化学习模块：根据验证器的反馈信息，调整LLM的推理策略，优化推理轨迹。整个流程是一个迭代过程，LLM不断生成证明步骤，验证器进行验证，强化学习模块根据反馈信息进行调整，直到证明成功或达到最大迭代次数。

关键创新：论文最重要的技术创新点在于将验证器反馈集成到强化学习训练中，使LLM具备了自我纠错能力。与现有方法相比，Leanabell-Prover-V2能够直接优化LLM的推理轨迹，并利用多轮验证器交互来提高证明的成功率。此外，论文还提出了反馈token掩码技术，用于稳定RL训练。

关键设计：在强化学习训练中，论文采用了一种简单的奖励策略，即成功证明获得正向奖励，失败则获得负向奖励。为了稳定RL训练，论文采用了反馈token掩码技术，即在训练过程中，对验证器反馈的token进行掩码，以避免LLM过度依赖反馈信息。具体的参数设置和网络结构细节在论文中未详细描述，属于未知信息。

🖼️ 关键图片

fig_0

📊 实验亮点

Leanabell-Prover-V2在MiniF2F测试集上取得了显著的性能提升。使用Kimina-Prover-Preview-Distill-7B作为基础模型时，pass@128指标提高了3.2%；使用DeepSeek-Prover-V2-7B作为基础模型时，pass@128指标提高了2.0%。这些结果表明，验证器集成的强化学习方法能够有效提高形式化定理证明的性能。

🎯 应用场景

该研究成果可应用于形式化验证、软件工程、人工智能安全等领域。通过自动生成和验证定理证明，可以提高软件和系统的可靠性和安全性。未来，该技术有望应用于更复杂的数学问题和实际工程问题，推动相关领域的发展。

📄 摘要（原文）

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.