Leanabell-Prover-V2: 通过强化学习实现验证器集成的形式化定理证明推理
人工智能
2025-07-14 v1
摘要
我们介绍了 Leanabell-Prover-V2，一个 7B 参数的大语言模型（LLM），它能够生成 Lean 4 的形式化定理证明，并集成了验证器的长思维链（CoT）。继我们之前的工作 Leanabell-Prover-V1 之后，我们继续选择对现有的强证明器模型进行后训练以进一步提升性能。在我们的 V2 版本中，我们主要升级了强化学习（RL），使用 Lean 4 验证器提供的反馈。关键在于，验证器反馈（例如指示成功或详细说明特定错误）使 LLM 能够对其自身推理过程的正确性产生“自我意识”，并学会反射性地纠正错误。Leanabell-Prover-V2 通过多轮验证器交互直接优化 LLM 的推理轨迹，并结合用于稳定 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 获取。
引用
@article{arxiv.2507.08649,
title = {Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning},
author = {Xingguang Ji and Yahui Liu and Qi Wang and Jingyuan Zhang and Yang Yue and Rui Shi and Chenxi Sun and Fuzheng Zhang and Guorui Zhou and Kun Gai},
journal= {arXiv preprint arXiv:2507.08649},
year = {2025}
}
备注
23 pages, 13 figures