继昨日放出新开源模型 Prover V2 之后，DeepSeek 在今天又公布了它的技术报告。
这份报告长达 34 页，披露了更多该模型的重要技术细节和基准测试表现，让我们有机会进一步了解它的创新之处。
两个模型都已经开源，可以在开源社区 Hugging Face 上找到。技术论文则是在 GitHub 上（模型和论文链接在文末）。
据论文介绍，DeepSeek Prover V2 是一个专为 Lean 4 形式定理证明设计的开源大型语言模型。其最大创新点在于，能将非形式化的数学推理能力与严格的形式化证明过程结合在一起，实现了两种思维模式的有效融合。
你可以想象一下，当我们要解决一道数学题时，脑海中往往先有一个大致的思路，然后再一步步填充细节。这种从整体到局部、从思路到步骤的过程，对人类来说很自然，但对AI却是一项艰巨的挑战。
在 AI 发展历程中，GPT 和 Claude 等大语言模型（LLM，Large Language Model）已经展示出令人印象深刻的数学问题求解能力。它们能够通过“思维链”（CoT，Chain-of-Thought）方法，像人类一样逐步思考问题，甚至能解决一些竞赛级别的难题。
然而，在更为严格的数学领域——形式化定理证明方面，AI 的表现却相对逊色。
原因在于两种思维模式的本质差异：自然语言推理是灵活的、启发式的，允许一定程度的模糊性和跳跃性思维；而形式化证明则要求百分百的精确性和严谨性，每一个推理步骤都必须经过严格验证，不允许任何隐含假设和细节省略。
就像两种不同的语言，虽然表达的是同一个数学世界，但规则和要求却大相径庭。
为了解决这一挑战，DeepSeek-Prover-V2 采用了一种创新的“递归定理证明流程”，这一流程的灵感源自人类数学家解决复杂问题的方法——将困难问题分解为一系列更容易解决的子问题。
首先，研究团队利用 DeepSeek-V3 模型担任“分解专家”的角色，构建定理证明系统的基础框架。
当面对一个复杂的数学定理时，DeepSeek-V3 会用自然语言分析和理解问题，提出高层次的证明思路，将整个证明分解为一系列较小的子目标，最后将每个子目标翻译成严格的 Lean 4 形式语言表达，由 have…sorry 语句组成，也就是需要解决的子目标。
这种方法也是人类所用的证明构建方式，即将复杂定理逐步简化为一系列更易管理的引理。
一旦复杂问题被分解为多个子目标，研究团队就会使用更小的 7B 参数模型作为解题专家，逐一攻克这些子目标。这种方法不仅提高了效率，还大幅降低了计算资源的消耗。
DeepSeek 采用递归求解策略系统地解决每个中间证明步骤。他们从 have 语句中提取子目标表达式，用它们替代原始问题中的目标，并将前面的子目标作为前提条件。
这种构建使后续子目标能够利用早期步骤的中间结果，从而促进更局部化的依赖结构，有助于开发更简单的引理。
为了减少大量证明搜索的计算开销，使用专门优化的小型 7B 证明模型处理分解后的引理。成功解决所有分解步骤后，原始定理的完整证明就可以自动推导出来。
在这个过程中，证明模型的训练需要大型形式语言问题集，但从人类编写文本形式化获得的训练信号通常较为稀疏，因为大部分计算尝试都不会产生成功的证明，因此不提供积极的奖励信号。
为了产生更密集的训练信号，DeepSeek 利用子目标扩展用于模型训练的形式语句范围，生成两类子目标定理：一类将前面的子目标作为前提条件，另一类则不包含前提条件。
这两类子目标被整合到专家迭代阶段，建立一个课程（curriculum），逐步引导证明模型系统地解决精心策划的一系列挑战性问题。
随后，研究团队挑选了一些 7B 证明模型无法“端到端（完全）解决”，但“所有子目标均已成功解决”的挑战性问题。通过组合所有子目标的证明，他们构建了原始问题的完整形式证明。这个证明再与 DeepSeek-V3 的自然语言推理过程配对，创建了“冷启动推理数据”。
“这使我们能够收集数百个高质量的合成冷启动数据，作为训练 DeepSeek-Prover-V2 的基础。”论文写道。
这些冷启动数据之所以珍贵，是因为它们同时包含了两种形式的数学推理：直观的自然语言思考链和严格的形式化证明步骤。就像是给 AI 提供了一本内容丰富的“双语教材”，帮助它学习如何在两种表达方式之间自如转换。
有了冷启动数据后，研究团队通过面向推理的强化学习（Reasoning-oriented Reinforcement Learning）进一步优化模型性能。在这个阶段，DeepSeek-Prover-V2 会学习如何更好地连接非形式推理与形式证明构建，特别注重保持证明结构与初始分解思路的一致性。
这个过程类似于学生在掌握基本思路后，通过不断练习和反馈来提升解题能力，逐渐形成自己的解题风格和策略。
在训练阶段，DeepSeek-Prover-V2 采用了两阶段训练策略，建立了两种互补的证明生成模式：
高效非链式思维（non-CoT）模式：快速生成简洁的形式 Lean 证明代码，不包含明确的中间推理步骤。高精度链式思维（CoT）模式：系统地阐述中间推理步骤，强调透明度和逻辑进展，构建最终形式证明。
训练过程中，研究团队使用“专家迭代”方法不断提升模型能力。每次迭代中，用当前最佳模型（策略）尝试解决之前未能解决的问题，成功的证明被添加到训练数据中，用于改进模型。
此外，在强化学习阶段，DeepSeek 使用了“群体相对策略优化”的算法，相比传统 PPO 效果更好、效率更高。
性能方面，DeepSeek-Prover-V2 在多个主流基准测试中都取得了不错的成绩。
即使是参数较少的 DeepSeek-Prover-V2-7B 也超越了以往所有开源定理证明模型。
更加令人惊讶的是，研究团队发现较小的 7B 模型在某些特定问题上甚至超越了 671B 的大模型，成功解决了 13 个大模型未能攻克的问题，将总解题数提升至 62 题。
在更全面的 CombiBench 测试中，DeepSeek-Prover-V2 在 77 个问题中解决了 12 个。虽然这一数字看似不高，但考虑到模型主要在数论和代数领域训练，这一表现已经展示了其良好的跨领域泛化能力。
研究团队认为这一对比结果很有趣，因为它表明形式数学证明与非形式数学推理之间的能力差距正在显著缩小。
最后，DeepSeek 团队计划将创造 DeepSeek-Prover-V2-671B 的经验扩展称一个类似 AlphaProof 的系统，最终目标是挑战国际数学奥林匹克级别的数学问题。