note_sync/大模型/deepseek/06-形式化证明/02-DeepSeek-Prover-V1.5-2408.08152_abstract.md

DeepSeek-Prover-V1.5：借助证明助手反馈的强化学习与蒙特卡洛树搜索

原文标题：DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search arXiv：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

一、摘要（全文翻译）

我们提出了 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 次尝试通过率