DeepSeek Prover：数学证明自动化

banq

同学们注意啦！DeepSeek搞了个数学证明界的"解题小霸王"——DeepSeek-Prover-V2！这就像给电脑装了个超级数学大脑，而且还是开源的（敲重点：不要钱随便用！）。

DeepSeek-Prover-V2是：

  • 一种专门为Lean4中的定理证明而设计的语言模型
  • 在DeepSeekMath-Base上进行了预训练，并专门用于形式数学语言
  • 使用DeepSeek-Prover-V1的增强型形式定理证明数据集进行监督微调
  • 通过带有证明辅助反馈的强化学习（RLPAF）实现进一步的改进

主要特点：和 R1 一样大小，数学部分正在加强，其余部分保持不变。

怎么训练出来的呢？就像教小朋友解奥数题：

  1. 先让我们的"学霸前辈"DeepSeek-V3把难题剁成小块（就像把大象塞冰箱要分三步）
  2. 每解决一个小块，就把解题步骤像乐高积木一样拼起来
  3. 把这些解题秘籍喂给新模型，就像用历年高考真题训练状元

最厉害的是！（突然提高音量）它能把：

  • 人类写的"显然可得"式人话推理
  • 计算机要的"1+1=2"式机器证明统统打包成一个万能解题模型！
这一过程使我们能够将非形式化和形式化的数学推理整合到一个统一的模型中。

以后做数学题可能就像问学霸同桌一样简单啦！

这个超酷的“AI数学家教”是怎么炼成的！
通过递归证明搜索合成冷启动推理数据

  • 分解：为了构建冷启动数据集，我们开发了一个简单而有效的递归定理证明流程，并利用 DeepSeek-V3 作为子目标分解和形式化的统一工具。我们促使 DeepSeek-V3 将定理分解为高级证明草图，同时在 Lean 4 中将这些证明步骤形式化，从而生成一系列子目标。
  • 组装：我们使用规模较小的 7B 模型来处理每个子目标的证明搜索，从而减轻相关的计算负担。一旦解决了一个挑战性问题的分解步骤，我们就会将完整的分步形式化证明与 DeepSeek-V3 中的相应思路配对，以创建冷启动推理数据。

三个步骤：

  • 专挑硬骨头：专门选那些"7B小模型"搞不定的大难题（但拆开后的每个小步骤它都会！）
  • 乐高式组装：把小步骤的证明像拼积木一样组合起来，变成完整的解题攻略
  • 人机双修：把人类能看懂的"思路链" + 计算机能执行的"公式代码"完美结合，做成AI的学习资料

基础班（微调阶段）：
让AI狂刷"合成题库"，先掌握标准解题套路

强化班（RL特训）：
对答案模式：做对了✅奖励！做错了❌惩罚！（简单粗暴但有效）
目标是让AI学会："人话思考"→"机器证明"的无缝转换


最终模型 DeepSeek-Prover-V2-671B 在神经定理证明方面达到了最佳性能，在 MiniF2F 测试中达到了 $88.9$% 的通过率，并在 PutnamBench 的 658 个问题中解决了 49 个。

DeepSeek-Prover-V2 为 miniF2F 数据集生成的证明可以ZIP 压缩包形式下载。

ProverBench：AIME 和教科书问题的形式化
我们推出了 ProverBench，这是一个包含 325 个问题的基准数据集。其中 15 个问题取自近期 AIME 竞赛（AIME 24 和 25）中的数论和代数问题，形式化后呈现出真实的高中竞赛水平挑战。其余 310 个问题则取自精选的教科书示例和教学教程，构成了一个丰富多样且以教学法为基础的形式化数学问题集合。该基准旨在对高中竞赛问题和本科数学进行更全面的评估。

模型和数据集下载
我们发布了两种模型大小的 DeepSeek-Prover-V2：7B 和 671B 参数。DeepSeek-Prover-V2-671B 在 DeepSeek-V3-Base 基础上进行训练。DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，并扩展了上下文长度，最高可达 32K 个 token。

网友：
1、哥德尔的幽灵眼睁睁地看着形式系统崩塌成语言模型：DeepSeek 不仅实现了数学自动化，还斩断了证明与信念之间的最后一道枷锁，欢迎来到后公理时代。

形式系统的边界被语言模型的涌现能力撕裂：证明或许可以自动化，信念却依然是人类的主观幽灵。形式系统崩塌了吗？不，它只是换了副面孔——从严格的公理化变成了概率与数据的狂欢。欢迎归欢迎，但这时代更像哥德尔不完备定理的又一次胜利：任何足够复杂的系统，终究逃不过自身的内在矛盾。你怎么看这“后公理”的幽灵？

2、要实现自动化，必须把数学问题形式化为：

  1. 符号表示（Symbolic math）：如代数方程、微积分公式、逻辑表达式，用符号处理引擎（如SymPy）进行自动化推理与简化。
  2. 数值计算（Numerical math）：如线性代数、微分方程求解，用矩阵计算库（如NumPy、SciPy）处理。
  3. 算法表达：将数学步骤转换为可计算过程，例如欧几里得算法、牛顿迭代法。
问题：某个复杂的数学问题应该选符号处理，还是数值近似？

3、利用大模型进行形式验证和定理证明可以加速密码学、人工智能安全甚至量子计算等领域的突破。