116 lines
14 KiB
Markdown
116 lines
14 KiB
Markdown
# DeepSeek-Prover-V1.5：借助证明助手反馈的强化学习与蒙特卡洛树搜索
|
||
|
||
> **原文标题**：DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
|
||
> **arXiv**：[2408.08152](https://arxiv.org/abs/2408.08152) ｜ **发布**：15 Aug 2024
|
||
> **作者/机构**：Huajian Xin、Z.Z. Ren、Junxiao Song、Zhihong Shao 等（DeepSeek-AI，深度求索）
|
||
> **原文 PDF**：[02-DeepSeek-Prover-V1.5-2408.08152.pdf](./02-DeepSeek-Prover-V1.5-2408.08152.pdf)
|
||
|
||
## 一、摘要（全文翻译）
|
||
|
||
我们提出了 DeepSeek-Prover-V1.5，这是一个面向 Lean 4 定理证明的开源语言模型，它通过同时优化训练过程与推理过程来改进 DeepSeek-Prover-V1。该模型在 DeepSeekMath-Base 上进行了预训练，并在形式化数学语言方面做了专门化；随后，它使用一个源自 DeepSeek-Prover-V1 的、经过增强的形式化定理证明数据集进行监督微调。进一步的提升则通过基于证明助手反馈的强化学习（Reinforcement Learning from Proof Assistant Feedback, RLPAF）来实现。在 DeepSeek-Prover-V1 的单遍完整证明生成方法之外，我们提出了 RMaxTS——一种蒙特卡洛树搜索的变体，它采用由内在奖励驱动的探索策略来生成多样化的证明路径。DeepSeek-Prover-V1.5 相比 DeepSeek-Prover-V1 取得了显著改进，在高中水平的 miniF2F 基准测试集上取得了新的最优结果（63.5%），在本科水平的 ProofNet 基准测试集上也取得了新的最优结果（25.3%）。
|
||
|
||
## 二、核心贡献
|
||
|
||
1. **形式化数学专用预训练**：在 DeepSeekMath-Base 上用数学与代码数据继续预训练，重点覆盖 Lean、Isabelle、Metamath 等形式语言，弥补通用基座对形式系统语法语义掌握不足的问题。
|
||
2. **两类数据增强的监督微调**：用 DeepSeek-Coder V2 236B 为 Lean 4 代码标注自然语言思维链注释，并把验证器返回的中间 tactic state 以注释插入代码，使模型兼顾自然语言推理对齐与编译器反馈利用，最终数据集含 9,645k 条序列。
|
||
3. **基于证明助手反馈的强化学习（RLPAF）**：用 GRPO 以 Lean 验证结果（正确为 1、否则为 0）作为奖励做在线强化学习，避免训练学习式奖励模型带来的失配。
|
||
4. **截断-恢复（truncate-and-resume）机制**：在首个验证错误处截断、把成功片段解析为树节点、再从节点恢复生成，无需改变模型目标即把树搜索嵌入整段生成框架，统一了逐步生成与整段生成两条路线。
|
||
5. **RMaxTS 搜索算法**：以「新增节点即给奖励」的内在奖励驱动探索，并用折扣 UCB（DUCB）应对奖励非平稳性，配合根并行、树并行与虚拟损失实现大规模并行搜索。
|
||
|
||
## 三、方法与技术要点
|
||
|
||
### 3.1 预训练与监督微调（Section 2.1–2.2）
|
||
|
||
在 DeepSeekMath-Base 上继续预训练高质量数学与代码数据得到 DeepSeek-Prover-V1.5-Base，重点覆盖 Lean、Isabelle、Metamath 等形式语言。**痛点**：形式化证明既要掌握 Lean 的语法语义，又要把抽象推理落到精确形式表示，通用数学基座不足。
|
||
|
||
证明代码取自 Mathlib4、DeepSeek-Prover-V1 合成定理、Lean Workbook 与 miniF2F/ProofNet 验证集，并用专家迭代（生成—验证—重训—再生成）扩充。针对「自然语言有细致推导、Lean 里却靠高层 tactic 暴力求解、掩盖内部机理」的问题，作者用 DeepSeek-Coder V2 236B 把自然语言推理**作为注释嵌入代码**：证明块开头插入完整解法，并在每个 tactic 前交替插入对应步骤，用两种引导提示区分 CoT 与非 CoT。为支持截断-恢复，借 LeanDojo 增强 Lean REPL 抽取 tactic 三元组（位置及前后 tactic state），并把状态以 `/- tactic state: … -/` 插入；训练时该注释之后的 token 计入监督损失，之前作为提示不参与。微调共 9B token，批 2,048，常数学习率 1e-4，100 步预热，最大上下文 4,096。
|
||
|
||
### 3.2 基于证明助手反馈的强化学习（Section 2.3）
|
||
|
||
训练提示从 SFT 数据中筛选「多次尝试成功率中等」的定理，兼顾提升空间与正反馈可得性，过滤后保留约 4.5k 条定理陈述，每条同时加 CoT 与非 CoT 提示。奖励无需奖励模型：Lean 验证正确给 1、否则给 0；该信号精确但稀疏，故靠上述筛选缓解。算法采用 GRPO——按组内相对奖励优化、无需 critic 模型，且组内恰好同时含正确与错误证明，与组相对特性契合。训练以 SFT 模型兼作初始模型与 KL 惩罚参考模型，学习率 5e-6，KL 系数 0.02，每定理采样 32 条候选、最长 2,048，批大小 512。
|
||
|
||
### 3.3 评估设置（Section 2.4）
|
||
|
||
基准为 miniF2F（高中数学竞赛，244 验证 + 244 测试）与 ProofNet（本科数学，185 验证 + 186 测试），均由 Lean 3 人工转为 Lean 4.9.0。Base 用 3-shot，SFT/RL 用 CoT 与非 CoT 两种引导提示。度量是 pass@$K$；单张 A100-40G 配 vLLM 采样（temperature 1、top-p 0.95、上限 2,048 token），导入 Mathlib4 与 Aesop 验证，单次限时 300 秒。
|
||
|
||
### 3.4 Tactic 级树抽象：截断与恢复（Section 3.1）
|
||
|
||
证明树建在 tactic 级，每条边代表一次 tactic state 转换。**截断**：把整段证明交 Lean 解析，在最早验证错误处截断，保证之前的 tactic 均可成功推进；代码切成若干片段，每片段含一个合法 tactic 及其思维链注释、对应一条树边，形成根到某节点的路径。**恢复**：Lean 4 中不同 tactic 可到达同一状态，故每个节点存一组等价 tactic；扩展时随机选一个作提示，提示由「以该 tactic 结尾的不完整代码 + 当前 tactic state 注释块」组成，微调模型正是被训练来识别该格式并续写。该抽象把不确定长度的整段生成转为可比较复用的离散动作，使搜索无需改动模型即可复用单遍生成模型。
|
||
|
||
### 3.5 基于 MCTS 的交互式定理证明（Section 3.2）
|
||
|
||
采用标准 MCTS 的选择、扩展、模拟、反向传播四步，但**把模拟并入扩展**，因为整段生成模型在扩展节点时本身就完成了一次 rollout。
|
||
|
||
**选择**：从根向下按树策略挑节点：
|
||
|
||
$$\text{TreePolicy}(s)=\mathop{\arg\max}_{a\in Children(s)\cup\{\oslash\}}Q_{UCB}(s,a)$$
|
||
|
||
动作既可是走向子节点 $a\in Children(s)$，也可是扩展当前节点（记 $a=\oslash$）。这里用**虚拟节点**技术：为每个节点配一个「假想子节点」代表选中自身做扩展，使搜索能持续扩展非叶节点——这对生成模型很关键，其输出范围无法用固定次数的试探界定。价值估计由利用与探索项组成：
|
||
|
||
$$Q_{UCB}(s,a)=\underbrace{Q(s,a)}_{\text{Exploitation}}+\underbrace{UCB(s,a)}_{\text{Exploration}}$$
|
||
|
||
$Q(s,a)$ 是依据历史的采样估计，$UCB(s,a)$ 随 $(s,a)$ 被反复执行而衰减，$Q_{UCB}(s,a)$ 可视为以高概率成立的上界。
|
||
|
||
**扩展**：从节点恢复不完整代码、做一次完整证明生成并交 Lean 验证；通过即终止搜索得新证明，否则在最早错误处截断，把剩余 tactic 转为一条路径并入树。传统竞赛 MCTS 每次只扩一层，这里每次迭代可能**插入整条节点路径**。**反向传播**：对第 $t$ 次迭代轨迹 $\tau=\{(root,s^{(1)}),\dots,(s_t,\oslash)\}$ 上所有 $(s,a)$ 更新价值；外在奖励来自编译器：完成 $R_{\text{extrinsic}}(\tau)=1$，否则为 0。
|
||
|
||
### 3.6 面向搜索的内在奖励：RMaxTS（Section 3.3）
|
||
|
||
证明搜索的外在奖励极度稀疏——只有完全解出才有非零奖励，是典型的「难探索」问题。RMaxTS 借鉴 RMax「到达未见状态即给最大奖励」的思想：完成前既无外在奖励，探索便完全由内在奖励驱动，即 $R(\tau)=R_{\text{intrinsic}}(\tau)$（类似 ZeroRMax）：
|
||
|
||
$$R_{\text{intrinsic}}(\tau)=\mathbb{I}\left[\text{at least one new node is added to the search tree}\right]$$
|
||
|
||
即一次扩展只要新增节点就给奖励，从而优先扩展能生成多样 tactic state 的节点；由于不同代码可能产生相同状态转移，该启发式还减少冗余。
|
||
|
||
**非平稳性**是第二个难点：随搜索树扩张，发现含未见状态的新节点越来越难，内在奖励期望值随探索衰减；标准 UCB1（$Q_{UCB1}(s,a)=\frac{W(s,a)}{N(s,a)}+\sqrt{\frac{2\ln\sum_{a'}N(s,a')}{N(s,a)}}$，$W,N$ 为奖励之和与次数）无法适应，故改用折扣上置信界：
|
||
|
||
$$Q_{DUCB}(s,a)=\frac{W_{\gamma}(s,a)}{N_{\gamma}(s,a)}+\sqrt{\frac{2\ln\sum_{a'}N_{\gamma}(s,a')}{N_{\gamma}(s,a)}},\quad W_{\gamma}=\sum_{t=1}^{N}\gamma^{N-t}R(\tau_{t}),\quad N_{\gamma}=\sum_{t=0}^{N-1}\gamma^{t}$$
|
||
|
||
使新反馈权重更大，实践中取 $\gamma=0.99$。与无限时域 MDP 值迭代不同，此处的折扣施加在**树搜索迭代**上而非单条轨迹的动作步长上。
|
||
|
||
### 3.7 并行化与既有方法对比（Section 3.4–3.5）
|
||
|
||
并行手段有三：根并行（每节点 256 个 runner、每 GPU 一个模型，Lean 在数千核集群上以沙箱进程异步验证）、树并行（每棵树 32 个线程 worker 循环执行选点—生成—验证—回传）、虚拟损失（进行中的迭代暂记奖励 0，促使并发 worker 选不同节点）。以往方法分两路：多遍逐步生成（GPT-f、Thor、ReProver、HTPS 等，适配搜索但通信开销大）与单遍整段生成（DSP、LEGO-Prover、Lyra 等，高效却用不上中间状态、易误差累积）；截断-恢复把二者统一，用近乎相同目标同时支撑两种范式。
|
||
|
||
## 四、主要实验结果
|
||
|
||
| 基准 / 任务 | 本模型 | 对比对象 | 说明 |
|
||
|---|---|---|---|
|
||
| miniF2F-test（单遍 pass@128） | 51.6% ± 0.5%（RL, CoT） | V1 46.1% ± 0.5%；SFT 50.4% ± 0.4%；Base 29.7% ± 0.5% | RL 在全部 $K$ 上均有提升 |
|
||
| miniF2F-test（单遍最大预算） | 60.2%（RL, 16×6400） | V1 50.0%；SFT 57.4% | 提升 10.2 个百分点 |
|
||
| miniF2F-test（树搜索） | 63.5%（RL + RMaxTS, 32×6400†） | InternLM2-StepProver 54.5%；HTPS 41.0%；SFT+RMaxTS 60.2% | 新 SOTA；† 为两种提示混合 |
|
||
| miniF2F-test（等预算） | 54.9% ± 0.7%（RL, 3200 次单遍采样） | InternLM2-StepProver 54.5%（64×3200 树搜索） | 采样预算小一个量级以上 |
|
||
| ProofNet-test（单遍） | 23.7%（SFT/RL, 4×6400） | Base 9.7% | RL 在 128 次预算下 18.2% ± 0.5% |
|
||
| ProofNet（树搜索） | 25.3%（RL + RMaxTS），验证集 25.4% | ReProver 13.8%；InternLM2-StepProver 18.1% | 全量（all）22.6%→25.3% |
|
||
| RMaxTS 消融（16×6400） | RMaxTS 62.7% | 单遍 60.2%；UCT（无内在奖励）61.1%；DUCB→UCB1 60.7%；无 tactic state 61.1% | 两个核心组件都必要 |
|
||
|
||
本模型在 miniF2F-test 上全面领先：单遍 60.2% 较 V1 的 50.0% 提升 10.2 个百分点，结合 RMaxTS 后达 63.5%；ProofNet 上单遍与树搜索分别为 23.7%（test）与 25.3%，超过 ReProver（13.8%）与 InternLM2-StepProver（18.1%）。等预算优势更明显：RL 模型仅 3200 次单遍采样即达 54.9%，后者需 64×3200 次树搜索才达 54.5%。消融显示去掉内在奖励的 UCT 退化为 61.1%、DUCB 换成 UCB1 为 60.7%、去掉 tactic state 提示亦为 61.1%，三者缺一不可；CoT 与非 CoT 互补（16×6400 时 60.2% vs 57.4%），混合策略把 RL 模型推到 63.5%。
|
||
|
||
## 五、结论、局限与影响
|
||
|
||
- **结论**：DeepSeek-Prover-V1.5 是 70 亿参数模型，在 Lean 4 形式化证明上超越所有开源模型：先以形式化数学语料扩展 DeepSeekMath-Base 7B，再经 Lean 4 代码补全数据监督微调与 GRPO 在线强化学习，最后由 RMaxTS 做大规模探索式搜索。该框架意在建立形式化证明的 AlphaZero 式流水线——专家迭代对应试错循环，编译器充当「世界模型」提供监督。
|
||
- **局限性**：作者自述目前只覆盖强化学习的**探索**侧面（RMaxTS 多样化生成），**利用**侧面即搜索本身尚未探索；附录示例显示 CoT 偏系统性数学思考、非 CoT 更擅长用高层 tactic 解决可自动化的计算问题，单一模式各有短板；且 ProofNet 验证集参与了监督微调的专家迭代，其成绩需谨慎解读。
|
||
- **影响**：作者认为有前景的方向是训练 critic 模型评估不完整证明并剪枝搜索分支，这种「部分证明」critic 会隐式实现时序信用分配，把证明级反馈分解为步级价值差；如何为长规划路径构建 critic 并给出引导奖励仍是难题。此外研究已从单定理证明走向复杂多定理 Lean 文件中的真实理论证明，作者观察到当前模型已具备一定文件级上下文理解能力。
|
||
|
||
## 六、关键术语对照表
|
||
|
||
| English | 中文 |
|
||
|---|---|
|
||
| Formal Theorem Proving | 形式化定理证明 |
|
||
| Lean 4 / tactic mode | Lean 4 / tactic 模式 |
|
||
| Whole-Proof Generation | 完整证明生成 |
|
||
| Proof-Step Generation | 逐步证明生成 |
|
||
| Supervised Fine-Tuning (SFT) | 监督微调 |
|
||
| Reinforcement Learning from Proof Assistant Feedback (RLPAF) | 基于证明助手反馈的强化学习 |
|
||
| Group Relative Policy Optimization (GRPO) | 组相对策略优化 |
|
||
| Chain of Thought (CoT) | 思维链 |
|
||
| Expert Iteration | 专家迭代 |
|
||
| Tactic State | tactic 状态 |
|
||
| Truncate-and-Resume | 截断-恢复机制 |
|
||
| Monte-Carlo Tree Search (MCTS) | 蒙特卡洛树搜索 |
|
||
| RMaxTS (RMax applied to Tree Search) | 应用于树搜索的 RMax 算法 |
|
||
| Intrinsic Reward | 内在奖励 |
|
||
| Discounted Upper Confidence Bound (DUCB) | 折扣上置信界 |
|
||
| Virtual Loss | 虚拟损失 |
|
||
| miniF2F / ProofNet | miniF2F / ProofNet 基准 |
|
||
| Pass@K | 前 K 次尝试通过率 |
|