DeepSeek AI宣布发布DeepSeek-Prover-V2，这是一个突破性的开源大型语言模型，专门为Lean 4环境中的形式化定理证明而设计。最新版本在之前工作的基础上，引入了一种创新的递归定理证明流程，利用DeepSeek-V3的强大功能生成自身高质量的初始化数据。由此产生的模型在神经定理证明方面实现了最先进的性能，并伴随着ProverBench的推出，这是一个用于评估数学推理能力的新基准。开创性的冷启动推理数据生成DeepSeek-Prover-V2的关键创新在于其独特的冷启动训练过程。该过程首先提示强大的DeepSeek-V3模型将复杂的数学定理分解成一系列更易于管理的子目标。同时，DeepSeek-V3将这些高级证明步骤形式化到Lean 4中，有效地创建了一系列结构化的子问题。为了处理每个子目标的计算密集型证明搜索，研究人员采用了较小的70亿参数模型。一旦某个具有挑战性问题的分解步骤全部成功证明，完整的逐步形式化证明将与DeepSeek-V3相应的思维链推理配对。这种巧妙的方法允许模型从一个综合的数据集中学习，该数据集集成了非正式的高级数学推理和严格的形式化证明，为后续的强化学习提供了强大的冷启动。强化学习增强推理在合成冷启动数据的基础上，DeepSeek团队精心挑选了一系列具有挑战性的问题，70亿参数的证明模型无法端到端地解决这些问题，但所有子目标都已成功解决。通过组合这些子目标的形式化证明，构建了原始问题的完整证明。然后，该形式化证明与DeepSeek-V3的

---

原文链接: https://syncedreview.com/2025/04/30/deepseek-unveils-deepseek-prover-v2-advancing-neural-theorem-proving-with-recursive-proof-search-and-a-new-benchmark/