跳至内容
全球开发者们都在期待的R2模型何时问世尚未可知，不过，DeepSeek又为开源社区贡献了一个重磅新模型：DeepSeek-Prover-V2，相关技术报告论文今天已出炉，外界推测，或为R2模型打头阵。
据了解，这是一款专为在Lean 4中进行形式化定理证明而设计的开源大语言模型，其初始化数据是通过由DeepSeek-V3驱动的递归定理证明管道收集而来的。
DeepSeek-Prover-V2-671B在神经定理证明方面取得了领先的性能。在MiniF2F测试中，当每次尝试32次时，它的准确率达到了82.4%，当每次尝试8192次时，准确率提升到了88.9%，该模型在大学水平的定理证明方面展现出了强大的泛化能力，当每次尝试1024次时，解决了ProofNet测试中37.1%的问题，并且攻克了658个具有挑战性的PutnamBench问题中的49个。
除了标准的基准测试之外，DeepSeek还推出了ProverBench，这是一个包含325 道形式化问题的集合，用于丰富评估。
其中包括从最近的美国数学邀请赛（AIME 24 和 25）竞赛中选取的15道题目，其余310个问题则取自精选的教科书示例和教学教程，构成了一个丰富多样且以教学法为基础的形式化数学问题集合。该基准旨在对高中竞赛问题和本科数学进行更全面的评估。
对这最新15道AIME题目的进一步评估表明，Prover-V2-671B模型成功解决了其中的6道题，相比之下，DeepSeek-V3模型通过多数表决法解决了其中的8道题，这凸显出大语言模型中形式化和非形式化数学推理之间的差距正在大幅缩小。
尽管自然语言推理在解决竞赛级别的数学问题方面取得了成功，但在形式化定理证明中的应用仍然面临着根本性的挑战。
因为大语言模型以一种本质上非形式化的方式进行自然语言推理，依赖于启发式方法、近似值以及数据驱动的猜测模式，而这些往往缺乏形式验证系统所要求的严格结构。
在技术报告论文中，DeepSeek团队提到了几项创新实验：
1、开发了一个用于子目标分解的推理模型，利用一系列合成的冷启动数据和大规模强化学习来提升其性能。
为构建冷启动数据集，他们开发了一个简单而有效的递归定理证明流程，将DeepSeek-V3用作子目标分解和形式化的统一工具。促使DeepSeek-V3将定理分解为高层次的证明概要，同时用Lean 4将这些证明步骤形式化，从而得出一系列子目标。
由于子目标分解是由一个大型通用模型驱动的，研究人员使用一个较小的70亿参数模型来处理每个子目标的证明搜索，以此减轻相关的计算负担。
2、引入了一个课程学习框架，该框架利用分解后的子目标生成猜想定理，逐步增加训练任务的难度，以更好地引导模型的学习过程。一旦一个具有挑战性问题的分解步骤得到解决，研究人员就会将完整的逐步形式化证明与DeepSeek-V3相应的思维链配对，从而创建冷启动推理数据。
基于冷启动，后续会应用一个强化学习阶段，以进一步加强非形式化数学推理与形式化证明构建之间的联系。
实验表明，从任务分解中基于非形式化推理的冷启动开始进行强化学习，显著提升了模型在形式化定理证明方面的能力，最终得到的DeepSeek-Prover-V2-671B模型在多个基准测试中达到了神经定理证明领域的最新领先水平。
DeepSeek研究员Zhihong Shao总结：解决近90%的miniF2F问题 ，显著提高PutnamBench上的SoTA性能，在正式版本中对AIME24和25问题取得了不平凡的通过率。
DeepSeek团队同时发布了两种模型大小的DeepSeek-Prover-V2：7B和671B参数。
DeepSeek-Prover-V2-671B在DeepSeek-V3-Base基础上进行训练，DeepSeek-Prover-V2-7B则基于DeepSeek-Prover-V1.5-Base构建，并扩展了上下文长度，最高可达32K个token。
这次新模型的发布可以说很有DeepSeek风格，没有浮华的描述，只有技术论证和数据展示，网友表示，除了硬核，无话可说。
（文：头部科技）
