ListenHub

4-30

晓曼: 哎，老王，最近看到深寻科技搞了个大新闻，说是出了个什么 DeepSeek-Prover-V2，开源的，专门证明数学定理的。听着挺唬人的，这玩意儿到底是个啥？我数学不好，你给咱通俗易懂地解释解释呗？

原野: 哈哈，这东西你可以理解成一个 AI 数学天才。它能像人一样一步一步地推理，证明那些复杂的数学定理。而且开源了，大家都能用。

晓曼: 像人一样推理？怎么个像法？难道它还会像我一样，对着数学题挠头？

原野: 那倒不至于挠头。它的核心思路是把一个大的证明题拆成一堆小的子问题，然后一个一个地解决，最后再把这些小证明拼起来，就成了完整的证明。

晓曼: 拆解？有点像咱们以前做数学题，先分析思路，一步一步地往下做？那它怎么拆？是自己看着题目就能分解出子任务？这也太厉害了吧！

原野: 嗯，这里面有个关键的工具，叫 DeepSeek-V3。你可以把它想象成一个经验丰富的数学老师，它先给出一个解题思路的草图，比如说，它会说：“这道题啊，咱们先证明A，再证明B，最后证明C。”

晓曼: 哎呦，听着有点意思了，这V3 这么厉害？能自己给出草图？

原野: 对，V3 给出草图之后，还会用一种叫Lean 4 的语言，把每一步都写得特别清楚，就像给机器下指令一样，生成子目标。之后呢，还会用一个小一点的模型去试着证明这些子目标。

晓曼: 等等，小一点的模型？不是应该直接用最厉害的模型吗？这是为了省钱？

原野: 哈哈，你真相了！要是每个小任务都用超大模型，那算力成本就太高了。所以先用小模型试试水，找到一些成功的证明，然后再用这些数据去训练大模型。这就像先让新手练练手，再让高手出马。

晓曼: 明白了！那接下来是不是就用强化学习了？就像训练狗狗一样，做对了给奖励，做错了给惩罚，让它慢慢学会怎么把那些“数学灵感”变成严谨的证明？

原野: 你理解得太到位了！而且啊，它还会特别关注那些小模型搞不定，但是拆解后每个小目标都能解决的难题。把这些难题的完整证明拿来训练大模型，让它知道怎么搭起从“日常数学思路”到“严谨形式化证明”的桥梁。

晓曼: 听着就觉得特别牛。那这模型到底有多厉害？能解决多难的题？

原野: 目前来看，DeepSeek-Prover-V2-671B 在神经定理证明领域绝对算得上是顶尖水平。它在一些标准测试集上表现非常出色。

晓曼: 哇，这么厉害！听得我都想试试了。能自己玩吗？

原野: 当然能！模型和数据集都放在 Hugging Face 上了，你可以自己下载来玩。他们还提供了详细的文档和示例，教你怎么用它来证明数学题。

晓曼: 哎，总结一下，这DeepSeek-Prover-V2 核心就是用 V3 拆题，小模型冷启动，强化学习来打磨。最后搞出一个能在各种测试里拿高分的开源定理证明模型。

原野: 没错！欢迎大家去试玩，自己给AI 出题，看看它能不能给你回手一篇严谨的证明。

晓曼: 好嘞！感觉数学大佬和机器学习爱好者都能用这个玩出新花样。那我们下次再聊别的酷玩意儿！

大纲

DeepSeek-Prover-V2 发布： 深寻科技发布了 DeepSeek-Prover-V2，一款用于形式化数学定理证明的开源大型语言模型。
核心能力： 通过强化学习进行子目标分解，从而推进形式化数学推理。
训练方式：
- 利用 DeepSeek-V3 将复杂问题分解为子目标。
- 将已解决子目标的证明合成为连贯的思维链，结合 DeepSeek-V3 的逐步推理，为强化学习提供初始数据。
- 整合非形式化和形式化数学推理到一个统一的模型中。
冷启动数据集构建：
- 使用 DeepSeek-V3 作为统一工具，进行子目标分解和形式化。
- DeepSeek-V3 将定理分解为高级证明草图，并同步用 Lean 4 形式化这些步骤，生成一系列子目标。
- 使用较小的 7B 模型处理每个子目标的证明搜索，降低计算负担。
- 将完整的形式化证明与 DeepSeek-V3 的思维链配对，创建冷启动推理数据。
强化学习阶段：
- 选择 7B 证明模型无法端到端解决，但所有分解的子目标已成功解决的难题。
- 组合所有子目标的证明，构建原始问题的完整形式化证明。
- 将此证明添加到 DeepSeek-V3 的思维链中，综合非形式化推理和后续形式化。
- 使用二元正确/错误反馈作为主要奖励监督，进行强化学习，提高模型连接非形式化推理和形式化证明构建的能力。
模型性能：
- DeepSeek-Prover-V2-671B 在神经定理证明方面达到最先进的性能。
- 在 MiniF2F-test 上达到 88.9% 的通过率。
- 解决了 PutnamBench 中的 658 个问题中的 49 个。
ProverBench 基准数据集：
- 包含 325 个问题。
- 15 个来自 AIME 竞赛中的数论和代数问题（AIME 24 和 25）。
- 310 个来自教科书示例和教育教程。
- 旨在更全面地评估高中竞赛问题和本科水平的数学问题。
模型和数据集下载：
- 提供 7B 和 671B 两种模型尺寸。
- DeepSeek-Prover-V2-671B 基于 DeepSeek-V3-Base 训练。
- DeepSeek-Prover-V2-7B 基于 DeepSeek-Prover-V1.5-Base 构建，具有高达 32K tokens 的扩展上下文长度。
- Hugging Face 上提供模型和数据集下载。
快速开始：
- 使用 Hugging Face 的 Transformers 进行模型推理。
- DeepSeek-Prover-V2-671B 与 DeepSeek-V3 共享相同的架构。
- 提供使用示例，展示如何为 miniF2F 数据集中的问题生成证明。

脚本