欢迎关注、星标
太卷了，就知道deepseek会在假期搞事情..
没想到4月30号直接发了个新模型，
想了想，还是简单给大家唠两句..
DeepSeek 这家公司又悄悄放了个“大招”——发布了全新的 DeepSeek-Prover-V2 模型，其中一个版本参数量高达 671B ！
huggingface上的Prover-V2模型
消息一出，各种讨论瞬间炸开了锅！
“这是 DeepSeek V3 的升级版吗？”
“传说中的 R2 终于来了？”
“671B 参数，这是要干啥？”
各种猜测满天飞。
打住！打住！先别激动，也别焦虑。
甲木今天就带大家来扒一扒，这个 DeepSeek-Prover-V2 到底是个啥玩意儿，它跟我们普通用户关系大不大，
以及 DeepSeek 这家公司到底在下一盘什么大棋。
省流版先来一个：
DeepSeek-Prover-V2 不是通用的聊天/推理模型（像 V3 或大家期待的 R2）
，它是专门为
形式化定理证明 (formal theorem proving)
设计的，特别是在
Lean 4
这个语言环境下。
它的目标是
自动化数学证明
，推动 AI 在严谨数学推理领域的发展。简单说，就是教 AI 怎么像数学家一样，一步一步、逻辑严密地证明数学定理。
它可能是 DeepSeek
研发更强通用模型（如 V4/R2）过程中的一个重要环节
，用来生成高质量的数学推理数据。
所以，对绝大多数普通用户来说，这个模型目前影响不大
，你期待的那个能说会道、超级聪明的通用大模型（V4/R2）还不是它。大家可以稍微放宽心，但对技术进展保持关注总是没错的！
一图总结
好了，背景交代完毕，咱们现在就深入细节，看看这份来自 DeepSeek 的“硬核”新成果。
什么是DeepSeek-Prover-V2？
首先，咱们得搞清楚 Prover-V2 的“主战场”——形式化定理证明 (Formal Theorem Proving) 和 Lean 4 。
什么是 Lean 4？它和我们平时用的 AI 有啥不同？
想象一下，我们平时和 ChatGPT、Claude这些大模型聊天，用的是自然语言，对吧？自然语言灵活、方便，但也有个“缺点”——不够精确，容易有歧义 。同样一句话，不同人可能有不同理解。
但在数学证明这个领域，最容不得的就是歧义和模糊。每一步推理都必须绝对严谨，逻辑链条不能有任何瑕疵。这时候，就需要一种超级精确、语法极其严格 的计算机语言，这就是形式化数学语言 ，而 Lean 4 就是其中的佼佼者。
甲木大白话:
自然语言 (中文、英文):
就像我们日常做饭用的
食谱
，描述可能比较随意，“少许盐”、“翻炒片刻”。老师傅能懂，但新手或者机器人可能就懵了。
Lean 4:
就像一份
化学实验步骤
，精确到毫克、秒，规定了严格的操作顺序和条件。只要严格按照步骤做，结果就能保证精确无误，而且计算机可以自动检查每一步是否合规。
Lean 4 能干啥？
主要就是用来写数学定义 、定理陈述 ，以及最关键的——能够被计算机自动检查和验证的证明过程 。它的核心价值就在于“自动验证 ”，确保你写的每一步推理都 100% 符合逻辑规则，杜绝任何“想当然”和逻辑谬误。
举个栗子：用 Lean 4 证明 1 + 1 = 2
（下面这个例子来自知乎 @happylittle 的精彩解释，甲木帮你简化转述一下）
用 Lean 4 证明 1+1=2，可不像我们直接写出来那么简单。它得从最基本的“什么是自然数”、“什么是加法”开始定义（基于皮亚诺公理 Peano Axioms）：
-- 1. 定义自然数 MyNat (我们自己定义一个，不用现成的)
inductive MyNat where
| zero : MyNat -- 有个东西叫 zero，它是 MyNat
| succ : MyNat → MyNat -- 如果 n 是 MyNat，那 n 的后继 (succ n) 也是 MyNat
-- 2. 定义 1 和 2
def one : MyNat := MyNat.succ MyNat.zero -- 1 是 0 的后继
def two : MyNat := MyNat.succ one -- 2 是 1 的后继 (也就是 0 的后继的后继)
-- 3. 定义加法 myadd
def myadd (n m : MyNat) : MyNat :=
match n with
| MyNat.zero => m -- 0 + m = m
| MyNat.succ n' => MyNat.succ (myadd n' m) -- (n'+1) + m = (n' + m) + 1
-- 4. 证明 1 + 1 = 2
theorem one\_plus\_one\_eq\_two : myadd one one = two :=
rfl -- rfl 是 Lean 的一个策略，意思是“这等式两边根据定义算出来是一样的”
你看，为了证明一个看似简单的 1+1=2，都需要如此严谨的定义和推理过程。Lean 4 会自动检查 rfl 这个证明策略是否真的能让等式两边完全一致。
知乎网友@happylittle的事例
谁在用 Lean 4？
这玩意儿确实不简单，学习曲线陡峭。目前主要是：
前沿数学家:
用来验证极其复杂的证明，或将经典数学理论形式化。
计算机科学家:
研究形式化方法、程序验证等。
少数爱好者:
对数学基础和严格证明感兴趣。
为啥 DeepSeek 要用 Lean 4 训练模型？
放着海量的网页文本、书籍不用，去啃 Lean 4 这块硬骨头，DeepSeek 图啥？
甲木觉得可能有几个原因：
追求推理的极致严谨:
DeepSeek 可能认为，掌握严谨的数学逻辑推理能力，是通往更强通用人工智能 (AGI) 的关键路径。用 Lean 4 训练，是希望 AI 不仅能模仿文本（像鹦鹉学舌），更能
真正理解和运用逻辑规则
。
高质量、结构化的数据:
Lean 4 代码本身就包含了精确定义和完整逻辑链，数据质量极高，没有歧义。而且证明过程是结构化的，AI 能学习“如何证明”的策略。Mathlib（Lean 的数学库）更是一个现成的、持续增长的优质数据集。
数据荒的可能性:
通用文本数据可能快被“榨干”了，需要寻找新的、高质量的数据来源来进一步提升模型能力。
生成合成数据:
通过 Prover 模型，可以生成大量高质量的数学证明数据，反哺给未来更强的通用模型（如 V4/R2）进行训练。
甲木再打个比方:
用普通文本训练 AI:
像教学生读很多很多范文，希望他能模仿着写出好文章。他可能文笔华丽，但逻辑不一定严谨。
用 Lean 4 训练 AI:
像教学生做严格的逻辑题，并要求他写出详细、可验证的解题步骤。他可能表达朴素，但思路清晰，逻辑严密。
DeepSeek 可能认为，后者对于培养真正的“智能”更重要。
DeepSeek-Prover-V2 如何炼成？
那么，DeepSeek 是如何打造出 Prover-V2 这个“数学证明高手”的呢？
根据论文摘要和官方介绍，他们采用了一套相当巧妙的流程，核心思想是结合非形式化推理 (informal reasoning) 和形式化证明构建 (formal proof construction) 。
这个过程可以分为两大阶段：
阶段一：通过“递归证明”生成高质量的“冷启动”训练数据
这一步的目标是创建一批既包含人类思考过程、又包含严格 Lean 4 证明的数据，作为 Prover 模型的基础训练教材。他们用了一个“递归定理证明流程 (recursive theorem proving pipeline) ”，听起来复杂，其实思路很清晰：
请“通才大师”出马 (DeepSeek-V3):
写“证明草图” (Proof Sketch):
用自然语言写出证明这个定理的
主要思路和步骤
（就像数学家打草稿），形成一个
Chain-of-Thought (思维链)
。
分解子目标 (Subgoal Decomposition):
同时，把这个证明过程分解成一系列更小的、更容易证明的
子目标 (subgoals)
或
引理 (lemmas)
，并把这些子目标写成 Lean 4 的
have
语句，但证明细节先空着，用
sorry
占位。（就像把一个大项目分解成若干个小任务）。
拿一个复杂的数学定理（用 Lean 4 陈述）。
先让
DeepSeek-V3
这个强大的
通用大模型
（就像一个知识渊博的数学家）来分析。
要求 V3 做两件事：
技术报告中的示意图
请“专才小助手”接力 (7B Prover Model):
因为让 V3 这样的大模型直接生成完整且正确的 Lean 4 证明细节很难，成本也高。
所以，DeepSeek 用了一个
更小的、专门训练用于 Lean 4 证明的 7B Prover 模型
（比如基于 Prover V1.5 扩展的，可以理解为一个更专注、更轻量级的证明助手）。
让这个 7B 模型
递归地 (recursively)
去解决 V3 分解出来的那些带有
sorry
的
子目标
。一次解决一个，后面的子目标可以利用前面已证明的结果作为前提（这叫
前提合并，incorporating preceding subgoals as premises
）。
将子目标转化为带前提的 lemma 语句
甲木大白话 - 盖大楼 🏗️:
总建筑师 (DeepSeek-V3):
负责设计整个大楼的蓝图（自然语言证明草图），并将工程分解为各个楼层、各个功能区的建造任务（带 sorry 的 Lean 4 子目标）。
施工小分队 (7B Prover Model):
每个小分队负责一个具体的建造任务（证明一个子目标），他们更专业、成本更低。后面的小分队可以基于前面完成的部分继续施工。
合成最终“竣工图纸” (Synthesize Complete Proof & Data):
甲木再强调一下这个数据的价值 ✨:
这就像一本超级棒的教材，不仅告诉你定理是怎么证明的（最终代码），还告诉你当初是怎么一步步想到这个证明思路的（自然语言草稿）。这对于训练 AI 学会“思考+证明”非常有价值！
当 7B 模型把所有子目标的
sorry
都成功填上（证明完成）后，把这些证明片段
组合起来
，就得到了原始复杂定理的一个
完整的、形式化的 Lean 4 证明
。
关键一步：
把这个
完整的 Lean 4 证明
，
附加
到
DeepSeek-V3 最初生成的那个自然语言证明草图 (Chain-of-Thought)
后面。
这样就得到了一条
高质量的训练数据
：它既展示了“如何像人一样思考”（V3 的 CoT），又展示了“如何将思考转化为严格的机器可验证代码”（完整的 Lean 4 证明）。这种数据就是所谓的
“冷启动”推理数据
。
阶段二：训练 DeepSeek-Prover-V2 模型
有了这些宝贵的冷启动数据，就可以开始正式训练 Prover-V2 了（比如 671B 版本就是基于 DeepSeek-V3-Base 进行训练）：
监督微调 (SFT):
先用这些包含 CoT 和完整 Lean 4 证明的
冷启动数据
，以及其他一些数据（比如没有 CoT 的、更简洁的证明数据，用于训练 non-CoT 模式），对基础模型进行微调。让模型学习这种从“思考”到“形式化证明”的映射关系。
强化学习 (RL):
甲木的比喻 - 训练围棋 AI 🤖:
SFT:
像让 AI 学习高手棋谱（冷启动数据）。
RL:
像让 AI 自己下棋（生成证明），赢了（通过验证）就奖励，输了就惩罚。GRPO 像一种更聪明的训练方法，让 AI 同时尝试多种下法（候选证明），然后比较哪种更好。一致性奖励就像早期训练时，教练要求 AI 必须先按照某种开局定式来下，打好基础。
SFT 之后，再通过强化学习进一步提升模型性能。
奖励机制 (Reward):
很直接，模型生成的 Lean 4 证明如果能被 Lean 编译器
验证通过
，就给
+1
的奖励，否则就是
0
。简单粗暴但有效！
优化算法:
使用
GRPO
，这是 DeepSeek 自己研发的一种高效 RL 算法，之前在 DeepSeek Math 和 R1 模型中都用过。它不需要额外的 Critic 模型，通过采样一组候选证明，根据它们的相对好坏（是否能通过验证）来优化策略。
一致性奖励 (Consistency Reward - 一个细节):
在 RL 训练早期，为了防止模型“放飞自我”，生成的证明结构和 V3 最初给出的 CoT 思路差太远，DeepSeek 还加入了一个“
一致性奖励
”，鼓励模型生成的最终证明包含所有分解出来的
have
结构引理。这有助于更好地连接非形式化思考和形式化结构，尤其是在处理需要多步推理的复杂定理时。
通过这样一套“生成高质量数据 + SFT + RL ”的组合拳，DeepSeek-Prover-V2 就被炼成了！它既能理解高层次的数学思想（继承自 V3 的 CoT 能力），又能生成精确无误的形式化证明代码（通过 Lean 4 训练和验证）。
实战成绩如何？(实验结果展示)
光说不练假把式，Prover-V2 的实战能力到底怎么样？DeepSeek 在论文和介绍中给出了几个关键 Benchmark 上的测试结果。
Benchmark 性能图
主要测试平台：
MiniF2F-test:
包含 488 个来自 AIME, AMC, IMO 等
高中数学竞赛
的形式化题目。DeepSeek 使用了更新后的版本，并保留了 test 部分（244题）严格用于评估。
PutnamBench:
包含 658 个来自
美国大学生普特南数学竞赛
的形式化题目，难度更高，覆盖大学数学领域。
ProverBench (DeepSeek 自建):
包含 325 个形式化问题，其中 15 个来自最新的
AIME 竞赛 (24 & 25 年)，其余 310 个来自精心挑选的** 教科书例题和教程**
，覆盖从初等数学到大学高等数学的广泛领域（数论、代数、微积分、分析学等）。
核心战绩：
MiniF2F-test (高中竞赛级):
DeepSeek-Prover-V2-671B (CoT 模式)
取得了
88.9% 的 Pass Rate
，这个成绩是目前的
State-of-the-Art (SOTA)
，超越了所有已知的开源和闭源模型！即使只用 32 个样本（Pass@32），也达到了惊人的 82.4%。
即使是 7B 版本，在 CoT 模式下也达到了 82.0% (Pass@8192)，同样非常有竞争力。
PutnamBench (大学竞赛级):
DeepSeek-Prover-V2-671B (CoT 模式)
成功解决了
49 个
问题 (样本量 1024)，显著优于其 non-CoT 版本（16个）和其他模型。这表明 CoT 推理方式对于处理更复杂的大学级别问题非常有效。
有趣发现 (7B 模型的“技能点”):
7B 的 non-CoT 模型在 PutnamBench 上竟然解决了 13 个 671B 模型没解决的问题（总解决数达到 62 个）！DeepSeek 分析发现，7B 模型更倾向于使用一种处理
有限基数 (finite cardinalities)
的特定技巧（涉及
Cardinal.toNat
等），这在 671B 的输出中很少见。这表明小模型有时也能在特定问题上“另辟蹊径”。
ProverBench (自建，含 AIME):
DeepSeek-Prover-V2-671B (CoT 模式)
在包含 325 个问题的完整集上，Pass@512 达到了 59.1%。
在备受关注的
15 个 AIME 24&25 难题
子集上，671B (CoT) 成功证明了
6 个
！
非常有意思的对比：
DeepSeek 还用
通用的 DeepSeek-V3 模型
（非 Prover）去做这 15 道 AIME 题的
非形式化解答
（就是用自然语言给出答案，类似我们做数学题），在使用多数投票（Maj@16）的情况下，V3
答对了 8 道
！
这意味着什么？
对于这些难题，当前最强的通用大模型在“理解和思考”层面（非形式化）的能力（8/15），已经非常接近甚至略微超过了专门训练的形式化证明模型在“严格证明”层面（6/15）的能力。
非形式化数学推理和形式化定理证明之间的差距正在显著缩小！
CoT vs non-CoT 模式对比:
无论是 MiniF2F 还是 PutnamBench，
CoT 模式的性能都显著优于 non-CoT 模式
。这再次证明了 CoT（让模型输出推理步骤）对于提升复杂数学推理任务准确性的有效性。
代价是什么？
CoT 模式生成的 Token 数量远超 non-CoT 模式
（见 PDF Table 3，平均长度可能是 non-CoT 的 10 倍左右）。这意味着 CoT 模式虽然更准，但也更慢、更贵。
另一个有趣发现：
即使在 non-CoT 模式下（没有明确要求输出思考步骤），671B 模型生成的 Lean 4 代码中也常常会
自发地插入一些类似注释的自然语言评论
，这暗示了即使没有明确提示，高容量模型也可能
内化并外化
中间推理步骤。
模型和数据集都开源了！
DeepSeek 这次非常慷慨，将 DeepSeek-Prover-V2 的两个尺寸模型（7B 和 671B）以及 ProverBench 数据集都开源 了！
模型下载:
DeepSeek-Prover-V2-7B: 🤗
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
DeepSeek-Prover-V2-671B: 🤗
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
注意：7B 模型基于 Prover V1.5 Base，上下文长度扩展到 32K；671B 模型基于 DeepSeek-V3-Base。
数据集下载:
DeepSeek-ProverBench: 🤗
https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
这意味着研究人员、数学家和开发者都可以下载模型和数据，进行自己的实验、评估和二次开发。这种开放共享的精神值得点赞！👍
结语：Prover-V2 对我们意味着什么？
好了，关于 DeepSeek-Prover-V2 的硬核内容咱们就啃到这里。最后，甲木再帮大家总结一下，并聊聊它对未来的意义。
总结一下 Prover-V2 的关键点：
定位:
专为 Lean 4 形式化数学定理证明设计的开源大模型。
核心技术:
结合 DeepSeek-V3 的非形式化推理（CoT+子目标分解）和专门 Prover 模型（7B）的递归形式化证明，生成高质量冷启动数据，再通过 SFT 和 RL（GRPO+一致性奖励）进行训练。
亮点:
实现了 SOTA 性能，显著缩小了非形式化推理与形式化证明之间的差距，开源模型和数据集。
局限:
非通用模型，对普通用户日常应用场景影响不大；CoT 模式效果好但成本高。
它对未来可能意味着什么？
AI 数学推理能力的新里程碑:
Prover-V2 展示了当前大模型在处理高度抽象、逻辑严谨的数学证明任务上能达到的惊人水平。这不仅仅是“解题”，更是对机器智能“深度理解”和“严谨推理”能力的一次重要验证。
数理推算就是最好训练推理模型的场景..
连接人类直觉与机器严谨的桥梁:
Prover-V2 的训练方法，特别是结合 V3 的 CoT 和最终的 Lean 4 证明，探索了一条将人类的非形式化思考过程与机器可验证的形式化逻辑联系起来的有效路径。这对于未来构建既能理解人类意图、又能进行可靠推理的 AI 系统至关重要。
高质量合成数据的“生产引擎”:
Prover-V2 可以被看作是一个强大的“数学知识引擎”，它能够生成大量高质量、带有推理过程和形式化验证的合成数据。这些数据对于训练下一代更强大的通用大模型（或许就是 DeepSeek V4/R2？）可能具有极高的价值。
推动形式化方法在更广泛领域的应用:
虽然目前主要用于数学，但形式化方法在软件工程、芯片设计、安全协议验证等领域也有广泛应用。Prover-V2 的成功可能会启发更多利用大模型来辅助进行形式化验证的研究。
AGI 探索的一条可能路径:
DeepSeek 将数学和代码视为 AGI 的“天然试验场”。通过在这些封闭、可验证的系统里不断提升 AI 的推理和自我学习能力，或许真的能一步步逼近通用人工智能。Prover 系列模型就是这条路径上的重要探索。
所以，虽然我们普通用户暂时还不能直接用 Prover-V2 来聊天、写文案，但它代表的技术突破和探索方向，预示着未来 AI 可能拥有的更深层次的理解和推理能力。
让我们一起期待 DeepSeek Prover V2 详细论文的发布，
看看里面还藏着哪些技术细节，
也期待这些技术能早日应用到我们能直接体验的通用大模型上！
未来已来，它或许复杂，或许充满挑战，
但更蕴藏着前所未有的机遇。
而我们，既是见证者，更是参与者，
与 AI 一同，去探索、去创造、去定义下一个智能时代！
过五一去了，happy！
我是甲木，一个强实践导向的 AI 应用布道者，致力于帮助普通人拥抱 AI，提升效率。关注我，我们一起在 AI 的星辰大海里打怪升级！
今天的硬核分享就到这里啦！有没有感觉对 AI 的能力又有了新的认识？
觉得甲木讲得还算清楚明白的话，请给个【点赞👍】+【在看👀】+【转发↗️】三连支持一下吧！
用你的“三连”告诉我，你收到了这份来自 AI 前线的最新情报！
与我联系
欢迎三连（点赞+评论+转发 ）！！