深夜突袭，DeepSeek-Prover-V2加冕数学王者！671B数学推理逆天狂飙
来源：新智元
【新智元导读】就在刚刚，DeepSeek-Prover-V2技术报告也来了！34页论文揭秘了模型的训练核心——递归+强化学习，让数学推理大提升。有人盛赞：DeepSeek已找到通往AGI的正确路径！
就在刚刚，DeepSeek-Prover-V2正式发布。
此次DeepSeek-Prover-V2提供了两种模型尺寸：7B和671B参数。
DeepSeek-Prover-V2-671B：在DeepSeek-V3-Base基础上训练，推理性能最强。
DeepSeek-Prover-V2-7B：基于DeepSeek-Prover-V1.5-Base构建，上下文长度扩展至高达32Ktoken。
Hugging Face：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
GitHub：https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main
同时，技术报告也放出了。
论文链接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
昨天，DeepSeek突然在Hugging Face上开源了671B模型，果然很快就有后续了。
数学证明大提升
此次DeepSeek-Prover-V2的训练核心，就是靠「递归+强化学习」。
首先，DeepSeek-V3会拆解复杂定理，生成一系列子目标和推理思路。随后，GRPO算法就会从多种候选方案中自动学习如何选出最优解。
对于这次放出的技术，网友盛赞说，这将导致超越人类的数字AI，极大地推动AI研究。
方法可以总结如下：
· 优化算法，以实现更快、更智能的模型
· 揭示AI「黑盒」行为的洞见
· 设计更好的架构，无需无尽的试错
· 加速数据分析，以实现更快的突破
因此，这就导致我们通向AGI，产生超级智能。几年内，AI就将产生人类无法理解的高级数学。
具体来说，DeepSeek-Prover-V2专门用于Lean 4中的形式化定理证明。
其中，初始化数据是通过DeepSeek-V3驱动的递归定理证明流程来收集的。
冷启动训练过程中，会首先提示DeepSeek-V3将复杂问题分解为一系列子目标，然后将已解决子目标的证明合成为思维链过程，并结合DeepSeek-V3的逐步推理，为强化学习提供了一个初始冷启动。
通过这个过程，非正式和正式的数学推理就能集成到一个统一的模型中。
总结来说，亮点如下。
· 生成冷启动推理数据：递归证明搜索方法
为构建冷启动数据集，团队开发了一个简单而有效的递归定理证明流程，利用 DeepSeek-V3作为统一工具，进行子目标分解和形式化。
DeepSeek-V3会被提示，将定理分解为高层次的证明草图。同时，在Lean 4中形式化这些证明步骤，从而产生一系列子目标。
首先使用一个较小的 7B 模型来处理每个子目标的证明搜索，以此降低计算负担。
一旦具有挑战性的问题的分解步骤得到解决，就将完整的逐步形式化证明与DeepSeek-V3产生的相应思维链过程相结合，从而生成冷启动推理数据。
· 基于合成冷启动数据的强化学习
团队精心挑选了一个具有挑战性的问题子集——它们无法通过7B prover以端到端的方式解决，但分解后的所有子目标都已成功解决。
通过整合所有子目标的证明，团队为原始问题构建了一个完整的形式化证明。
然后，将此证明附加到DeepSeek-V3的思维链中，该思维链概述了相应的引理分解，从而将非正式推理与后续形式化过程有机结合。
在合成冷启动数据上微调prover模型后，团队执行了强化学习阶段，以进一步增强其连接非正式推理与形式化证明构建的能力。
根据推理模型的标准训练目标，采用二元正确/不正确反馈作为主要的奖励监督形式。
最终，模型DeepSeek-Prover-V2-671B在神经定理证明方面实现了当前最优的性能，在MiniF2F-test上达到了88.9%的通过率，并解决了PutnamBench中658个问题中的49个。
DeepSeek-Prover-V2为miniF2F数据集生成的证明：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip
· 针对AIME与教科书题目的形式化数据集ProverBench
ProverBench是一个包含325道题目的基准数据集。
其中，15道题目源自最近AIME竞赛（AIME 24&25）中的数论和代数题目，提供了极具挑战性的高中竞赛级别题目。
剩余的310道题目则来自精选的教科书例题和教学教程，构建了一个多样化的、具有教学意义的形式化数学题目集合。
因此，这项基准更全面地评估高中竞赛和本科阶段的数学水平。
DeepSeek-Prover-V2
在论文中，团队构建了用于子目标分解的推理模型，利用合成的冷启动数据和大规模强化学习技术来提升其性能。
通过子目标分解实现递归式证明搜索
将复杂定理的证明过程拆解为一系列较小的引理，作为中间步骤，是人类数学家普遍采用的一种高效策略。
近年来，分层式方法在神经定理证明领域得到了广泛应用。它的核心思路是借助现代大型语言模型（LLM）擅长的非形式化推理能力，来提升定理证明搜索的效率。
这部分包括3阶段：从自然语言推理到形式化证明草图、子目标的递归求解、基于子目标的定理证明中的课程学习。
首先提示DeepSeek-V3，同时生成自然语言形式的证明草图，并将其形式化为Lean语言中的定理陈述，其中对于尚未证明的部分使用sorry占位。
接着，7B证明模型用于递归地求解被分解出的各个子目标。通过组合这些子目标的证明内容，团队可以构建出原始复杂问题的完整形式化证明。
冷启动数据收集流程概览
DeepSeek利用子目标来扩展可用于模型训练的形式化定理范围。
他们生成了两种类型的子目标定理：一种包含前序子目标作为前提条件（对应图 3(b)），另一种则不包含前提条件（对应图 3(a)）。
这两种类型的子目标都被纳入到专家迭代阶段，形成一个渐进式的课程体系，引导证明模型逐步掌握解决精选难题的方法。
这一流程的核心思想与AlphaProof 在测试阶段采用的强化学习策略类似：生成目标问题的多种变体，提升模型解决高难度的IMO级别问题的能力。
将分解后的子目标转化为一系列引理（lemma）陈述
首先执行步骤 (a)：将原始目标状态替换为当前子目标。
接着进行步骤 (b)：将之前的子目标作为前提条件纳入当前引理中。
类型 (b) 的陈述用于递归求解复杂问题，而类型 (a) 和 (b) 的陈述都被纳入课程学习流程中，用于训练模型逐步掌握推理能力。
最后，将这个组合后的正式证明附加到 DeepSeek-V3最初生成的「思维链」之上，形成高质量的冷启动训练数据，用于支持形式化数学推理的学习。
统一非形式化推理与形式化证明
算法框架包括两个阶段，分别依赖两个互补模型：用于引理分解的 DeepSeek-V3，以及用于补全具体形式化证明细节的7B证明模型。
这种方法巧妙地融合了高层次的自然语言推理和低层次的精确证明过程，为构建可用于训练的形式化推理数据提供了重要基础。
· 用合成数据实现冷启动
在研究过程中，DeepSeek挑选出一些特别难解决的问题。
这些问题很棘手，即便用7B证明模型，也没办法从头到尾直接解决。
不过有意思的是，把这些问题拆解成一个个小目标后，每个小目标都能被成功证明。就像拼拼图一样，把这些小目标的证明过程按顺序组合起来，就能得到原始难题的完整证明，而且这个证明是非常严谨、规范的形式化证明。
接着，DeepSeek把这个完整的证明，添加到 DeepSeek-V3 生成的 「思维链」 里。
这里的 「思维链」 就像是解题的思路草稿，详细记录了把难题分解成小目标的过程。
这样一来，DeepSeek就得到了一份特殊的证明样本，它既有像日常思考那样的非形式化推理过程，又有严谨的形式化证明步骤，两者完美结合。
通过这种方式，团队成功收集到了几百条高质量的数据。
它们非常重要，是训练 DeepSeek-Prover-V2模型的基础。
这里方法的核心是把日常语言描述的证明过程，直接转化成有逻辑结构的形式化框架。
· 用强化学习提升推理能力
用冷启动合成数据对证明模型进行初步优化后，就进入了强化学习阶段。
强化学习阶段目的是让模型更好地把日常语言的推理过程，转化成严谨的形式化证明。
在这个过程中，按照标准的推理模型训练要求，用 「正确」 或 「错误」 这两种简单的反馈，作为主要的奖励监督信号。也就是说，如果模型给出的证明是对的，就奖励它；如果错了，就不给奖励。
但训练有个问题：模型生成的证明结构，经常和 「思维链」 里分解问题的思路对不上。
为了解决这个问题，在训练刚开始的时候，团队就加入了一种新的奖励机制，专门用来惩罚那些和分解结构不一致的输出结果。
在实际训练中，这个保证结构一致的方法效果非常好，大大提高了证明的准确率。尤其是在证明那些需要很多步骤、特别复杂的定理时，优势更加明显。
训练细节
DeepSeek-Prover-V2的训练采用了两阶段策略，建立了两种互补的证明生成模式：
这两个生成模式的设计延续了DeepSeek-Prover-V1.5的思路，区别在于不同的提示模板。
在第一阶段中，团队结合课程学习框架和专家迭代机制，训练non-CoT证明模型，并通过子目标分解递归地合成复杂问题的证明。
由于non-CoT模式推理速度快、验证成本低，因此非常适合快速迭代与数据采集。
在此基础上，第二阶段引入了冷启动的思维链数据，这些数据整合了DeepSeek-V3的高级数学推理能力与合成的形式化证明。
CoT模式随后进入强化学习阶段，以进一步提升模型在推理和形式化构造之间的衔接能力。
专家迭代（Expert Iteration）
DeepSeek-Prover-V2的non-CoT模型训练采用了「专家迭代」方法，这是目前形式化定理证明系统中广泛使用的训练范式。
论文链接：https://arxiv.org/abs/2009.03393
每轮训练中，当前性能最好的模型会尝试解决前几轮未成功证明的难题。
成功的证明结果经Lean系统验证后被加入监督微调（SFT）数据集中，用于训练下一代更强的模型。
这个过程不仅让模型持续从初始演示数据中学习，还能提炼自身的成功推理路径，不断优化解决难题的能力。
DeepSeek-Prover-V2整体训练流程与V1和V1.5保持一致，只在训练问题的分布上做了两处改进：
监督微调（Supervised Fine-tuning）
团队在DeepSeek-V3-Base-671B的基础上进行微调，学习率设置为常数5e-6，最大上下文长度为16,384 token。
训练数据来自两个来源：
non-CoT数据强化模型在Lean生态中的形式验证能力，而CoT数据则更强调将数学直觉转化为结构化形式证明的过程。
强化学习（Reinforcement Learning）
DeepSeek采用了Group Relative Policy Optimization（GRPO）作为强化学习算法。
GRPO不需要单独的价值评估模型，而是通过对每道题采样多个候选证明，并基于相对奖励进行策略优化。
训练时，我们使用二元奖励机制Lean验证成功则得分1，失败则为0。
为了确保训练有效性，团队精心挑选了具有挑战性但又可解的题目作为训练提示。
在每轮训练中，随机选取256道不同题目，每道题生成32个候选证明，最大序列长度为32,768 token。
蒸馏与小模型训练（Distillation）
团队将DeepSeek-Prover-V1.5-Base-7B的最大上下文长度从4,096扩展到32,768 token，并利用在671B模型强化学习阶段采集的rollout数据对模型进行微调。
在CoT模式之外，团队还加入了专家迭代期间采集的non-CoT数据，旨在让小模型具备成本更低的证明能力，能够快速输出精炼的形式化结果。
此外，团队也在7B小模型上执行与671B模型相同的强化学习流程。
实验结果
MiniF2F基准测试结果
MiniF2F包含488个形式化的题目，来源包括AIME、AMC和IMO等竞赛，以及MATH数据集，涵盖了初等数学的核心领域，如代数、数论和归纳法。
这些题目被分为两个大小相等的子集，即miniF2F-valid和miniF2F-test，每个子集包含244道题目，并且在各个学科领域具有相同的分布。
如表1所示，实验结果表明，DeepSeek-Prover-V2-671B在miniF2F-test基准上取得了SOTA性能，当采用CoT生成策略时，仅用32个样本便达到了前所未有的82.4%的准确率。
值得注意的是，参数效率更高的DeepSeek-Prover-V2-7B也展现出了很强的竞争力，超越了现有文献中的所有开源定理证明器。
他们还发现了一个明显的规律：随着样本预算从1增加到8192，7B和671B模型之间的性能差距显著扩大，更大规模的模型展现出更高的样本效率和更快的性能提升。
· 子目标引导的课程学习在难题证明中的应用
表2详细展示了DeepSeek-Prover-V2在miniF2F基准测试中的解题情况，其在验证集和测试集上分别取得了91.0%和88.9%的高通过率。
值得注意的是，团队提出了子目标引导的课程学习框架，将通用模型DeepSeek-V3与轻量级专用7B prover相结合，在miniF2F-valid上实现了90.2%的成功率，与DeepSeekProver-V2-671B的性能几乎持平。
这些发现表明，SOTA的通用LLM不仅能进行自然语言理解，还能有效支持复杂的形式推理任务。
通过巧妙的子目标分解，模型便可将难题分解为一系列可处理的步骤，从而有效连接非正式推理与形式化证明构建。
· CoT vs. non-CoT
表1的实验结果表明，在形式化数学推理中，CoT推理模式相比non-CoT模式具有显著的性能优势。
这进一步验证了CoT提示的有效性，它鼓励将复杂问题分解为中间步骤，并证实了推理时扩展在形式化定理证明领域依然适用。
作为补充，表3提供了DeepSeek-Prover-V2在不同推理模式下生成的token数量的统计信息。
正如预期的那样，CoT模式会生成明显更长的输出，反映了其复杂的推理过程。
有趣的是，在non-CoT设置下，671B模型生成的平均输出长度比7B模型更长。
更仔细的分析表明，尽管non-CoT模式下没有显式推理提示，但较大规模的模型通常会在证明代码中插入简短的自然语言注释，这些注释类似于隐式推理步骤。
这表明，即使没有显式的CoT提示，高容量模型也可能在内部和外部隐式地执行中间推理。
本科水平基准测试结果
· ProofNet
ProofNet包含371道使用Lean 3编写的题目，这些题目选自一系列流行的本科纯数学教材，涵盖了实分析、复分析、线性代数、抽象代数和拓扑等主题。
表4的结果显示，相比于non-CoT设置，采用CoT推理时DeepSeek-Prover-V2的通过率得到了显著提升。
尽管训练数据主要源自高中数学，但该模型在更高级的大学数学问题上展现出了强大的泛化能力，代表着强大的形式推理能力。
· PutnamBench
PutnamBench基准测试集包含了1962年至2023年普特南数学竞赛中的数学题。
它是美国和加拿大极负盛名的年度本科生数学竞赛，涵盖分析、线性代数、抽象代数、组合数学、概率论和集合论等多个大学领域的知识。
如表4所示，DeepSeek-Prover-V2-671B在PutnamBench中展现了增强的推理能力，解决了49道题目，并显著优于其non-CoT版本。
这说明，CoT推理方法已经可以有效处理极有挑战性的大学数学问题。
·RL实现的技能发现：7B胜过671B！
此外，团队意外地发现：DeepSeek-Prover-V2-7B在PutnamBench数据集上采用non-CoT生成模式时，也表现出了卓越的性能。
更令人称奇的是，这个较小的7B模型成功解决了DeepSeek-Prover-V2-671B仍未能解决的13道题！
这是为什么？
仔细分析模型的输出后，团队从中发现了一种独特的推理模式——
7B模型经常使用Cardinal.toNat和Cardinal.natCast_inj来处理涉及有限基数的问题，而671B模型生成的输出中明显缺少这种处理方式。
似乎就是这种技术，让7B能有效解决需要精细操作基数值的问题。
组合问题测试结果
CombiBench是一个综合性的基准测试集，其中包含了100道用Lean 4形式化表示的组合竞赛题，配有自然语言描述。
团队采用with-solution设置，此时正确的答案已嵌入在Lean代码中，因此评估可以完全集中在证明过程的生成上。
对其中77道题进行评估后，模型成功解决了12道。
结果表明，尽管该Prover模型主要在数论和代数领域进行训练，但在组合问题上也展现出了良好的泛化潜力，即使这些问题相当难。
ProverBench数据集
为了增强现有基准，团队构建了一个包含325道题目的基准数据集。
其中，15道题目来自AIME 24和25中的数论和代数题目，属于极难的高中竞赛级别题目。剩余的310道题目则来自精选的教科书例题和教学教程。
这就能更全面评估高中竞赛和本科阶段的数学水平。
· AIME题目形式化
美国数学邀请赛AIME 24&25中的题目，已成为评估LLM推理能力的常用基准。
为了弥合模型在形式化和非形式化数学推理能力评估上的差异，我们整理并形式化了AIME 24&25中的部分题目，并排除了几何、组合和计数问题，因为它们在Lean中的表示较复杂。
最终，团队选择了15道题目，涵盖了初等数论和代数中竞赛级别的知识点。
结果显示，DeepSeek-V3-0324成功解决了15道题中的8道题。
而DeepSeek-Prover-V2-671B在已知正确答案的前提下，能够为15道题目中的6道构建出有效的形式化证明。
这种表明，非形式化数学推理与形式化定理证明的性能差距正在显著缩小，高级语言模型在语言理解和形式逻辑的严谨性上正日益接近。
· 教科书题目形式化
除了AIME 24&25之外，团队还从高中竞赛和本科课程教材中挑出题目来扩充基准测试集。
最终，他们形式化了310道题，难度范围很广，覆盖了竞赛级别的初等数学到本科常见的高级主题。
如表6所示，结果表明，采用CoT推理的DeepSeek-Prover-V2-671B始终优于所有基线模型，与在其他基准测试中的表现一致。
在论文最后，团队表示，未来的工作将着重于将范例扩展到类似AlphaProof的系统。
最终目标，就是解决代表自动定理证明领域前沿的IMO级数学难题！
快速开始
我们可以直接使用Hugging Face的Transformers库进行模型推理。
以下是如何生成miniF2F数据集中问题证明的一个简单示例：
参考资料：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main
