7.2 DeepSeek-R1：从“纯强化学习自进化”到“多阶段可用推理模型”，以及 DeepSeek-Prover-V2 的形式化证明管线

关键词：Pure RL、GRPO、规则奖励（Accuracy / Format）、Aha Moment、冷启动（cold-start）、拒绝采样 + SFT、全场景强化学习（Helpfulness / Harmlessness）、蒸馏；以及形式化定理证明的“子目标分解 → 递归求解 → 课程学习 + 一致性奖励 → 两阶段 no-CoT/CoT”。

---

1. 背景：为什么 post-training 成为推理能力的主战场？

大模型的推理能力提升，越来越依赖 post-training（预训练之后的训练阶段）。相较于继续扩大预训练规模，post-training 常见优势是：

• 更直接地提升推理任务准确率（数学、代码、逻辑）
• 更容易对齐用户偏好与社会价值（helpfulness / harmlessness）
• 相比预训练成本更低、迭代更快

在推理领域，另一条重要线索是 inference-time scaling：通过让模型在测试时“想得更久 / 搜得更多”，提升最终答案质量。早期的代表性思路是通过增加 CoT（Chain-of-Thought）长度提升推理；后续扩展到：

• PRM（过程奖励模型）：对中间步骤打分，引导更好的推理轨迹
• Search：MCTS、Beam Search 等在推理空间中搜索更优轨迹

但一个核心现实是：想要达到顶尖推理系统那种“强而稳”的效果，仅靠 test-time scaling 并不总能充分解决问题。DeepSeek-R1 的关键主张之一，是把重点放回到 训练阶段：用“纯强化学习”让模型在训练中自进化出更强推理行为。

---

2. 研究问题与总体路线：从 R1-Zero 到 R1

DeepSeek-R1 的故事可以视为两步：

1. DeepSeek-R1-Zero：
   在 base model 上直接做大规模强化学习（不先 SFT），观察推理行为能否“自发出现并增强”。

2. DeepSeek-R1：
   R1-Zero 虽然推理能力很强，但存在明显可用性问题（可读性差、语言混合等）。因此引入 少量冷启动数据 + 多阶段训练，在保留推理增益的同时，变得更“用户友好”、更通用。

此外还有第三条线：蒸馏。把 R1 的推理模式迁移到更小模型上，让小模型也能获得强推理能力。

---

3. DeepSeek-R1-Zero：纯强化学习如何让推理“自进化”？

3.1 为什么强调“纯强化学习（Pure RL）”？

以往许多推理强化学习工作高度依赖监督数据（例如大量标注的推理轨迹、步骤级标注、或者大规模 SFT 先把模型拉到一个很强的初始化）。DeepSeek-R1-Zero 的核心实验更激进：
不做 SFT 冷启动，直接从 base model 开始 RL。

其动机是验证：当奖励信号足够正确、训练规模足够大时，模型能否通过 RL 交互过程自动形成：

• self-verification（自我验证）
• reflection（反思与重审）
• 更长、更复杂的 CoT（思考时间增长）

---

3.2 强化学习算法：GRPO 视角理解

R1-Zero 采用的是 GRPO（Group Relative Policy Optimization）范式。直观上，GRPO 的核心是：

• 对同一个问题采样一组回答
• 用这组回答的相对比较（比如组内均值、方差）来构造优势函数
• 从而减少对显式 Value Model（Critic）的依赖，使训练更简洁

可以用如下形式表达（符号按常见写法给出）：

• 对问题 $q$，从旧策略采样 $G$ 个输出：
  {o1,o2,…,oG}∼πθold(O∣q) \{o_1, o_2, \ldots, o_G\} \sim \pi_{\theta_{\text{old}}}(O|q) {o1​,o2​,…,oG​}∼πθold​​(O∣q)

• 每个输出由奖励函数给出标量奖励 $r_i$，并构造组内标准化优势：
  Ai=ri−mean({r1,r2,⋯ ,rG})std({r1,r2,⋯ ,rG}) A_i = \frac{r_i - \text{mean}(\{r_1, r_2, \cdots, r_G\})}{\text{std}(\{r_1, r_2, \cdots, r_G\})} Ai​=std({r1​,r2​,⋯,rG​})ri​−mean({r1​,r2​,⋯,rG​})​

• 目标函数沿用 PPO 风格的 clipped ratio，并加 KL 约束（对齐参考策略）：
  $${\mathcal{J}}_{\text{GRPO}}(\theta )=\mathbb{E}\left[\frac{1}{G}\sum _{i=1}^G\left(\min \left(\frac{{\pi }_{\theta }(o_i|q)}{{\pi }_{{\theta }_{\text{old}}}(o_i|q)}{A}_i,\text{clip}\left(\frac{{\pi }_{\theta }(o_i|q)}{{\pi }_{{\theta }_{\text{old}}}(o_i|q)},1-\epsilon ,1+\epsilon \right)A_i\right)-\beta {\mathbb{D}}_{\text{KL}}({\pi }_{\theta }||{\pi }_{\text{ref}})\right)\right]$$

怎么理解这套公式“在推理里为什么有效”？

• 组内标准化 $A_i$ 的意义：同一问题的多个候选回答往往质量差异很大。用组内相对优势，等价于让模型学习“同题里更好的回答应该更可能出现”，而不是依赖一个绝对尺度的 value 估计。
• ratio + clip：避免策略更新过猛导致崩坏。
• KL：把策略限制在参考策略附近，减少分布漂移的风险。

---

3.3 奖励建模：规则奖励（Accuracy + Format）

R1-Zero 的奖励设计非常关键：它没有依赖 ORM/PRM 之类的学习型奖励模型，而是采用 规则（rule-based）奖励，主要包含两类：

1. 正确率奖励（Accuracy Reward）
   目标是奖励最终答案正确。典型做法是让模型输出一个易解析的最终答案（固定格式），然后用规则验证：

• 数学：提取最终答案，与标准答案或可验证结果对比
• 编程：编译器 + 测试用例评测

2. 格式奖励（Format Reward）
   强制模型把推理过程放在特定标签中（例如 <think>...</think>），让“思考”和“最终答复”结构化。

一个简化的奖励组合可以概括为（形式表达，具体权重依实现而定）：
$$r=r_{\text{acc}}+{\lambda }_{\text{fmt}}{r}_{\text{fmt}}$$

其中 $r_{\text{acc}}$ 反映正确性，$r_{\text{fmt}}$ 反映格式遵循。

为什么不直接用 PRM/ORM？
一个主要担忧是 reward hacking：当奖励模型复杂且可被利用时，策略可能学会“骗过奖励”，而不是提升真实推理质量。规则奖励在可验证任务中更稳健、也更可控。

---

3.4 训练模板：让约束只管“结构”，不管“内容偏好”

为了避免对推理风格施加过强先验（例如强制反思、强制某种解题策略），R1-Zero 的模板目标是：

• 只规定输出结构：先推理，再给答案
• 不规定推理内容必须怎么写

这样做的意义是：把自由度留给 RL 自进化，让模型自行发现更有效的策略（例如自检、回退、尝试替代路径）。

---

3.5 训练现象：性能增长、思考时间增长，以及 Majority Vote 的进一步加成

R1-Zero 的重要观测包括：

• 随 RL 训练推进，某些推理基准的性能呈现稳定一致的提升趋势
• 推理链长度（或回答长度）随训练步数增长，甚至接近线性增长：
  这可以理解为模型在训练中学到“多想一会儿更可能拿到正确奖励”，从而自发延长思考过程

此外，推理任务中常见的推理增强技巧是 多数投票（consensus / majority vote）：

• 同一题采样多次（例如 $N=64$）
• 取出现频率最高的答案作为最终答案

这相当于把 test-time compute 再拉满一次，经常能显著抬高最终准确率。

---

3.6 Aha Moment：从“直接往下算”到“主动回头审视”

所谓 “Aha Moment”，可以理解为：模型在训练到某一阶段后，开始学会一种更高阶的策略——重新评估自己早先的步骤，并在发现潜在错误时主动回退、换路。

可以用一个非常直观的案例来说明这种行为为什么重要。

案例：一个容易走偏的多步推理题

假设问题需要连续推导 6 步。早期模型可能：

• 第 2 步做了一个隐含假设
• 后面所有推导都建立在这个假设上
• 最终答案错误

如果模型只会“往前推”，它很难纠正第 2 步的错误。

而出现反思行为后，模型可能在第 5 步发现矛盾，于是：

• 回到第 2 步检查假设
• 改用另一条推导路径
• 最终得到正确答案并拿到奖励

这种“自发的回头检查”并不是人工硬编码的，而是在奖励驱动下，策略空间里自然出现的有效行为模式。

---

3.7 R1-Zero 的缺点：强推理不等于好用

尽管 R1-Zero 展示了纯 RL 的推理潜力，但它也暴露出明显问题：

• 可读性低：输出不够清晰、结构不稳定
• 语言混合：推理链可能混入多种语言，影响使用体验

这就引出了 R1 的核心目标：在保留推理提升的同时，让模型更“用户友好”、更通用。

---

4. DeepSeek-R1：冷启动 + 多阶段训练，把“强推理”变成“可用模型”

R1 的两个研究问题可以概括为：

1. 加少量高质量冷启动数据，能否进一步提高推理性能或加速收敛？
2. 如何训练一个用户友好模型：CoT 清晰连贯，同时具备强通用能力？

---

4.1 冷启动（Cold-start）：用少量长 CoT 稳住 RL 起跑线

从 base model 直接 RL，早期往往不稳定，输出也可能非常“野”。冷启动的做法是：

• 收集少量高质量长 CoT 数据
• 用这些数据先做一次微调，让 actor 有一个相对稳定、可读的初始策略
• 再进入大规模 RL

冷启动数据来源包括：

• few-shot prompt 诱导长 CoT
• prompt 加 reflection / verification 诱导更高质量轨迹
• 对 R1-Zero 输出做人类后处理与筛选

冷启动的一个关键目标是：把输出规范化为更易读模式。例如在回答末尾加入总结区块，使用户能快速看到答案要点。

---

4.2 面向推理的强化学习：继续用规则奖励，但加入“语言一致性奖励”

在冷启动后，R1 进入第一阶段大规模 RL，目标仍然以推理能力为主。

这里出现的新问题是：CoT 可能出现语言混合。为此引入 语言一致性奖励，与正确性奖励叠加。一个直觉形式是：

• 设目标语言为 L
• 统计思维链中属于 L 的 token 或单词比例，作为 $r_{\text{lang}}$
• 总奖励为：
  $$r=r_{\text{acc}}+{\lambda }_{\text{lang}}{r}_{\text{lang}}$$

这样可以在不破坏推理优化方向的前提下，约束输出语言更一致、更可读。

---

4.3 拒绝采样 + SFT：用 RL 收敛后的模型“反哺”下一阶段训练数据

当第一阶段 RL 得到一个较强推理模型后，R1 进入 “拒绝采样与 SFT” 阶段，其核心是：

• 用当前模型对一批 prompt 采样多个 response
• 只保留“更优 / 更正确 / 更符合规则”的样本
• 把筛选后的数据作为 SFT 数据，进一步提升稳定性与泛化

数据通常分两类：

1. 推理数据：
   通过推理 prompt 采样多条轨迹，只保留正确轨迹，形成大规模推理数据集（例如数十万级别）。

2. 非推理通用数据：
   写作、事实问答、翻译、角色扮演、自我认知等，混入通用领域数据以提升全面能力。

SFT 的意义可以理解为：把 RL 得到的行为模式“固化”为更稳定的生成分布，同时补齐通用能力短板。

---

4.4 全场景强化学习：同时优化推理、Helpfulness 与 Harmlessness

最后进入第二阶段 RL（全场景强化学习），目标更全面：

• 推理数据：继续采用 rule-based reward（如正确性 + 格式）
• 通用数据：使用 Reward Model 捕捉更细腻的人类偏好

同时对齐两个方向：

1. Helpfulness（有用性）
   重点关注最终总结部分，确保回答实用、相关，同时尽量减少对推理过程的干扰。

2. Harmlessness（无害性）
   评估整个 response（包括推理过程与总结），识别并减轻潜在风险、偏见或有害内容。

这一阶段的直觉是：
推理能力只是强模型的一部分；真实可用模型必须在“推理强 + 输出友好 + 安全对齐”之间达到平衡。

---

5. 蒸馏：把 R1 的推理模式迁移到更小模型

蒸馏部分的关键结论是：
推理能力不一定需要大模型才能表现出来；大模型学到的推理模式可以用 SFT 形式迁移给小模型。

做法是：

• 用 DeepSeek-R1 生成（或筛选得到）大规模样本
• 对下游小模型做监督微调（SFT）

蒸馏对象覆盖多种规模与家族（例如 Qwen、Llama 的不同参数量），体现出推理模式的可迁移性。

---

6. DeepSeek-Prover-V2：形式化定理证明的“子目标分解 → 递归求解 → RL”管线

形式化定理证明（如 Lean 4）与自然语言推理非常不同，它的难点在于：

• 需要严格、可验证的证明（proof checker 一步都不让错）
• 证明步骤的搜索空间极大（每一步都可能分叉）
• 任何一个小错误都可能导致整个证明无效

因此它不仅要求“答案正确”，还要求“步骤可验证且结构严谨”。

---

6.1 核心管线概览：先搭骨架，再逐个填空，最后用 RL 再打磨

DeepSeek-Prover-V2 的核心思路可以拆成三段：

1. 子目标分解与冷启动数据生成：
   用大模型生成证明草图，把复杂定理拆成多个子目标（类似人类先写证明框架）。

2. 递归求解子目标：
   用专门证明器模型逐个解决子目标，把 sorry 占位符补齐。

3. 课程学习 + 一致性奖励的强化训练：
   从简单到困难训练，并用一致性约束防止最终证明偏离原先分解结构。

---

6.2 子目标分解：把一个大目标拆成多个可控子问题

在 Lean 里，一个常见的“证明草图”会包含占位符：

• have ... := by sorry 表示：先声明一个中间引理，但暂时不证明（留坑）
• 这些坑就是子目标（subgoals）

这种结构模拟了人类证明习惯：
先决定整体证明路线与关键引理，再逐个完成引理证明，最终合并。

案例：为什么分解能显著缩小搜索空间？

设原始目标是证明命题 $T$。直接搜索证明相当于在巨大空间里找一条完整路径，难度非常高。

如果能分解为：
$$T\Leftarrow (L_1\wedge L_2\wedge \cdots \wedge L_k)$$

即只要证明 $k$ 个子引理 $L_1,\dots ,L_k$，并把它们组合起来即可完成 $T$。
那么搜索就从“找一条长路径”变成“找多条短路径 + 拼装”。这在形式化证明里往往更可行。

---

6.3 递归求解：用证明器模型逐个填坑，并把解当作前提继续证明

拿到含 sorry 的草图后，证明器模型会：

• 先把第一个子目标当作当前目标去证明
• 证明成功后，把它作为已知前提加入上下文
• 再证明下一个子目标
• 循环直到所有子目标完成
• 最后把子证明按逻辑顺序合成为完整证明

这个过程之所以称为“递归”，是因为每个子目标本身也可能需要进一步分解或多步推导。
最终得到一条完全可验证的 Lean 证明序列。

---

6.4 课程学习：从简单到复杂地喂数据，让模型逐级变强

形式化证明任务跨度巨大：
从简单代数引理到复杂竞赛级定理，难度差异非常大。

课程学习（curriculum learning）的做法是：

• 先训练容易的定理/引理
• 再逐步加入更困难的样本
• 让模型能力沿着难度曲线逐渐提升

这通常能带来更稳定的训练与更高的最终上限。

---

6.5 一致性奖励：让最终证明尽量遵循“原先分解的结构”

一个实际现象是：模型在最终生成证明时，可能会偏离最初的子目标结构，例如：

• 草图里引入了 $k$ 个关键引理
• 最终证明漏用了其中某些引理，或跳过了某些结构步骤
• 导致证明风格混乱，甚至更容易失败

因此在训练初期加入额外约束：
如果最终证明与草图结构不一致（例如漏掉了某些 have 引入的引理），就施加惩罚。可以抽象写为：

• 设草图引入的引理集合为 $\mathcal{H}$
• 最终证明实际使用的集合为 $\hat{\mathcal{H}}$
• 一致性惩罚可以与差集大小相关：
  $$r_{\text{cons}}=-|\mathcal{H}\setminus \hat{\mathcal{H}}|$$

总奖励（示意）：
$$r=r_{\text{prove}}+{\lambda }_{\text{cons}}{r}_{\text{cons}}$$

其中 $r_{\text{prove}}$ 是“证明通过验证器”的主奖励，$r_{\text{cons}}$ 用于约束结构一致性。

---

6.6 no-CoT 与 CoT 的两阶段：效率与精度的折中

DeepSeek-Prover-V2 还引入两种输出模式的配合：

1. no-CoT（非思维链）模式
   强调直接产出简洁的 Lean 证明代码，不显式展开中间推理。优点是速度快、成本低，适合更简单或更熟练的题型。

2. CoT（思维链）模式
   强调在形成最终形式化证明前，显式阐述中间推理步骤，以提高透明性与逻辑连贯性。对于困难定理更有利，能提高成功概率，也更利于调试与分析。

两阶段训练的直觉是：
先让模型学会“快速给出可验证证明”的能力，再让模型学会“在复杂问题上更稳、更可控地推导”。

---

6.7 关键启发：为什么这套形式化证明范式值得关注？

启发 1：子目标分解是对抗巨大搜索空间的通用武器

把复杂任务拆成更小子问题，本质上是在降低决策深度与分支因子。
这不仅适用于形式化证明，也适用于代码生成、复杂规划、多步推理等场景。

启发 2：弥合非形式化推理与形式化推理的鸿沟

人类数学家常用直觉与非形式化推理引导证明方向，然后再写出严谨形式化证明。
“先生成推理草图 → 再把草图翻译/补全为形式化代码 → 再验证”的流程，正是在模拟这条路径。它为训练模型获得某种“数学直觉”提供了可操作的范式。

启发 3：更强的自动化定理证明器可能会成为数学研究的基础设施

当模型能稳定生成可验证证明时，它就不仅是“会做题”，更可能成为：

• 证明验证助手
• 复杂推导的加速器
• 甚至在一定条件下帮助发现新定理的工具链组件

---

7. 小结：DeepSeek-R1 与 Prover-V2 的共同主题

尽管一个面向通用推理，一个面向形式化证明，但两者共享一条清晰主线：

• 用 可验证信号（规则奖励/验证器）作为训练的硬约束
• 让模型通过 强化学习 自进化出更强的推理行为
• 在工程上通过 冷启动、阶段化训练、数据筛选与结构约束 把“强推理”转化为“稳定可用的系统”
• 并通过 蒸馏 把能力下放到更小模型，实现更广泛部署

这类方法的核心魅力在于：只要奖励与验证足够可靠，模型往往能自己学会更高级的策略，而不需要把解题过程逐步教给它。