AI Agents DeepSeek Systems and Models Retrieval-Augmented Generation Sparse Attention Long-Horizon Agents Recursive Self-Improvement Continual Learning and TTT

Browse this library

Chinese source article

02 · DeepSeek-Prover-V1.5: 证明助手反馈, 截断续写和好奇心搜索

V1 用 800 万条合成语句把 7B 模型在 Lean 4 miniF2F-test 上推到 50.0%, 靠的是一遍写完整段证明.

View original Markdown ↗

来源: DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search(arXiv: 2408.08152v1, 2024-08-15, 后收入 ICLR 2025). 仓库: https://github.com/deepseek-ai/DeepSeek-Prover-V1.5.

V1 用 800 万条合成语句把 7B 模型在 Lean 4 miniF2F-test 上推到 50.0%, 靠的是一遍写完整段证明. V1.5 没有换骨架, 参数仍是 7B, 改动落在四个地方: 继续预训练时加入形式语言, SFT 数据里插入自然语言 CoT 注释和 tactic 状态注释, 用 Lean 的 0/1 验证结果做 GRPO(报告叫 RLPAF), 推理时把整证生成接进蒙特卡洛树搜索并配上内在奖励(RMaxTS). 这四处互相依赖: 状态注释是树搜索续写的前提, 中等难度的提示筛选是 GRPO 能学到梯度的前提, 大规模 CPU 验证集群是一切大预算数字的前提. miniF2F 上的结果同时依赖这条训练与搜索链, 不能单独归因给其中一个环节.

1. 训练流水: 预训练, SFT 与 RLPAF

1.1. 问题: 整证生成看不见中间状态

形式证明模型大致分两类. 逐步生成每次只写一条 tactic, 交给 Lean 执行, 拿回新的证明状态再写下一条, 通常配树搜索, GPT-f, ReProver, HTPS, InternLM2-StepProver 都属于这一类. 整证生成一次写完整段证明代码再交给 Lean 验证, 失败就重采样, DSP, LEGO-Prover 和 V1 属于这一类. 前者每步都能看到真状态, 但模型和验证器之间来回通信很多; 后者通信少, 却要在看不到中间状态的情况下预测一长串 tactic.

报告把后者的毛病归结为误差累积(compounding errors): Lean 的 tactic 模式是一步步改写证明状态, 模型对某个中间状态「脑补」错了, 后面每一行都建立在错的状态上. V1 的证明普遍很短, 主要靠 nlinarith, simp_all 这类高层 tactic 收尾, 一旦题目需要多层中间结论, 这个毛病就暴露出来. V1.5 想要的是: 保留整证生成的低通信成本, 同时在出错时能拿到真状态, 从出错的地方接着写, 而不是从定理陈述重开.

1.2. 起点: 继续预训练, 骨架不变

V1.5-Base 从 DeepSeekMath-Base 7B 继续预训练, 语料是高质量数学和代码, 重点放在 Lean, Isabelle, Metamath 这些证明助手用的形式语言(源文 §2.1). 报告没有给出这轮预训练的 token 数、学习率、数据配比以及各形式语言的占比. 可见的效果只有一个数: Base 用 3-shot 提示在 miniF2F-test 上 Pass@128 为 29.7%, 6400 次采样到 42.2%. V1 报告表 1 里 DeepSeekMath-Base 同样 128 次采样是 27.5%, 两者预算相同, 续训只带来约 2 个点. 两边的 few-shot 示例来源可能不同, V1.5 用的是 Yang(2023) 的人写证明, 所以这 2 个点也不全是权重的功劳. 相比之下 SFT 一步把 Pass@128 抬到 50% 上下, 形式证明能力主要是 SFT 数据给的, 继续预训练更像是把形式语法的底子打平.

报告也没有通过消融说明 Isabelle 和 Metamath 语料能否改善 Lean 证明. 三种语言的语法和 tactic 体系差别很大, 可能迁移的是「目标-假设-变形」这类证明结构, 具体贡献无法从现有实验中分离.

骨架方面, 这仍是 DeepSeekMath 那套 7B Dense decoder-only 结构, 报告没有提任何架构改动. 这点决定了整条技术路线的形状: 参数不变, 所以增益只能来自数据格式, RL 信号和推理时的搜索. 也因为模型小, 单卡 A100-40G 加 vLLM 就能跑采样, 真正的瓶颈落在 Lean 验证上, 后面树搜索那一节会看到, 验证要数千个 CPU 核.

1.3. 训练数据: CoT 注释和 tactic 状态注释

SFT 数据的定理来自 Mathlib4, V1 和 Lean Workbook 的合成语句, 以及 miniF2F 和 ProofNet 的验证集, 再用 expert iteration 滚出证明: 生成, 验证, 拿通过的回训, 再生成(源文 §2.2). 每轮之间让 DeepSeek-Coder-V2 236B 给证明补自然语言注释, 最终得到 9,645k 条序列. SFT 训 9B token, batch 2,048, 恒定学习率 1e-4, 上下文 4,096. 用 9B 除以 9,645k, 平均每条约 930 token, 这是带注释之后的长度. 数据质量怎么筛, 可以对照 SFT 数据质量筛选; 这里 Lean 编译器本身就是最硬的过滤器, 不需要另训质量模型.

注释分两种. 第一种是 CoT: 在证明块开头插一段完整的自然语言解法, 再在每条 tactic 前插对应步骤的说明, 和 Lean-STaR 每步前单独做 CoT 的思路接近, 区别是 V1.5 把推理直接写进代码注释. 训练时用两套引导提示区分 CoT 模式和 non-CoT 模式, 推理时可以任选. 第二种是 tactic 状态: 作者给 Lean REPL 接上 LeanDojo 的抽取工具, 拿到每条 tactic 的位置和执行前后的状态, 然后在合法证明里插入 tactic state: 注释. 训练时注释之后的 token 算 loss, 之前的当提示, 相当于一个「读懂当前状态再往下写」的辅助目标. 第二种注释是截断续写的地基, 没有它, 后面树搜索喂进去的状态注释模型根本不认识.

两种模式在输入上的区别只在第一行引导语. 附录 A 里 non-CoT 的提示是「Complete the following Lean 4 code」, CoT 的提示是「Complete the following Lean 4 code with explanatory comments preceding each line of code」, 后面跟相同的文件头: import Mathlib, import Aesop, set_option maxHeartbeats 0, 以及一串 open. maxHeartbeats 0 关掉了 Lean 的单步计算上限, 真正的时间约束只剩 300 秒的外部时限. 同一道 aime_1983_p9, non-CoT 输出两行 tactic 就结束; CoT 输出先写一段整体思路, 再在每条 tactic 前写一句说明, 长度是前者的好几倍. 这个长度差直接影响 2,048 token 上限下能写多长的证明, 也影响相同采样数下的推理成本, 报告的预算记号按「生成次数」计, 把这两种长度不同的生成当作等价.

有一点报告没有讨论: CoT 注释是 Coder-V2 写的, Lean 只检查代码, 不检查注释. 附录 B.2 的 amc12_2000_p12 就是例子, 注释里说「用一个引理: 三数之和有界则乘积有界」, 代码里并没有这样的引理, 真正干活的是 interval_cases a <;> interval_cases m <;> interval_cases c 把 13³ 种取值全部枚举一遍. 同一附录里 numbertheory_x5neqy2p4 的模 11 注释和代码是对得上的. 所以 CoT 注释有时是真规划, 有时只是事后的叙述, 报告把 CoT 模式的增益归因于「更系统的数学思维」, 这个归因没有做注释与代码一致性的检查.

1.4. RLPAF: 用 Lean 当奖励的 GRPO

RL 阶段的提示来自 SFT 数据, 只挑 SFT 模型多次尝试后成功率中等的定理, 最终留下约 4.5k 条, 每条同时配 CoT 和 non-CoT 两种引导(源文 §2.3). 奖励就是 Lean 验证的 0/1, 不训练奖励模型. 算法采用 DeepSeekMath 提出的 GRPO: 每题采 32 条候选, 用组内相对得分当优势, 不需要 critic. 参考模型是 SFT 模型, KL 系数 0.02, 学习率 5e-6, 最大长度 2,048, batch 512. 报告未给训练步数和总 GPU 时间, 因而无法计算这一阶段的总训练成本.

中等难度筛选和 GRPO 的组内比较是配套的. 全对或全错的组, 组内优势全为零, 这一步什么也学不到; 只有一组 32 条里有对有错, 梯度才非零. 这比 DeepSeekMath 的处境简单得多: 那边用的是神经网络奖励模型, 要担心奖励被钻空子, 这边 Lean 验证几乎没有假阳性. 不过报告没有说明验证脚本如何拒绝 sorry 或其他绕过检查的写法. 按今天的叫法, 这就是 RLVR(可验证奖励的 RL), 比 R1 用规则奖励做大规模 RL 早了近半年.

奖励粒度覆盖整条证明. 一段证明包含十几条 tactic 时, 末尾一条出错也会使整条序列得到 0 分, 正确前缀无法在训练中获得单独信用. GRPO 没有逐步信用分配; 推理阶段的截断续写保留成功前缀作为搜索节点, 部分弥补了这个缺口. CoT 模式还包含大段注释, 2,048 的最大长度对它更紧. 报告未给出截断比例以及 RL 前后的平均证明长度, 无法量化长度限制的影响.

1.5. RL 到底改变了什么

图 3 在 Pass@128 上比较各阶段: Base 29.7%, SFT non-CoT 49.8%, SFT CoT 50.4%, RL non-CoT 50.5%, RL CoT 51.6%. SFT 这一步涨了约 20 个点, RL 只再涨 1.2 个点(CoT 模式). 报告的论点是: 和 DeepSeekMath 里「RL 只是把 TopK 里的正确答案抬上来」不同, 形式证明上 RL 带来的是基础能力提升, 证据是采样预算加大后差距不消失. 表 3 支持这一点, 单遍 CoT 在 16×6400 预算下 SFT 57.4%, RL 60.2%, 差 2.8 个点, 反而比 128 次时更大.

表 1 把这个趋势摊得更开. 单遍 CoT 下 SFT 和 RL 在各预算的成绩: 32 次 48.2% 对 50.0%, 64 次 49.6% 对 50.7%, 128 次 50.4% 对 51.6%, 3200 次 53.3% 对 54.9%, 4×6400 次 55.8% 对 58.4%, 16×6400 次 57.4% 对 60.2%. 差距从 1 到 2 个点逐步拉到 2.8 个点, 采样越多 RL 领先越多. 这和 DeepSeekMath 的 Figure 7 方向相反, 那边 RL 只抬 Maj@K, Pass@K 不动. 一个可能的解释是奖励的性质不同: DeepSeekMath 用的是有噪声的神经奖励模型, 这里是几乎零噪声的 Lean 验证. Base 的曲线则更平: 128 次 29.7%, 3200 次 39.2%, 6400 次 42.2%, 多采样能涨, 但和 SFT 之间始终隔着十几个点.

这个论点有两处需要打折扣. 第一, 对照对象是 SFT, 不是 Base. 2025 年那篇讨论 RLVR 边界的论文(Yue 等)发现, 在自然语言数学上, 采样数足够大时 Base 的 Pass@k 会反超 RL 模型, V1.5 的 Base 只测到 6400 次, 42.2%, 离 RL 的 60.2% 还很远, 所以这里无法检验同样的现象, 相关讨论见 RLVR 的局限与探索边界. 第二, 「RL 在所有设定下都胜过 SFT」只在 miniF2F 上成立. 表 2 的 ProofNet 里, 单遍 4×6400 时 RL 在验证集 21.6% 低于 SFT 22.2%, 全集 22.6% 低于 SFT 22.9%; RMaxTS 1×3200 时 RL 全集 21.8%, SFT 21.9%. 仓库 README 的汇总表也把 ProofNet 上 SFT 列为 22.9%, RL 列为 22.6%. 4.5k 条 RL 提示来自 SFT 数据, 偏高中竞赛代数, 对本科级的实分析, 抽象代数题帮助有限, 这是一个合理的解释, 报告没有讨论.

后来的开源工作给了一个更直接的对照. 2025 年 2 月的 Goedel-Prover 把 Numina 的自然语言题目形式化成 164 万条 Lean 语句, 用 expert iteration 证出其中 80 万条以上, 然后只在 V1.5-Base 上做 SFT, 不做 RL, miniF2F-test Pass@32 就到 57.6%, 比 V1.5-RL 的 50.0% 高 7.6 个点, 3200 次采样时 62.7% 对 54.9%. 这说明在这个规模上, 语句覆盖面比 RL 那一两个点重要得多, V1.5 的 RL 增益是真的, 但在整条流水线里分量不大.

2. 树搜索: 截断续写与 RMaxTS

2.1. 截断续写: 把整证拆成搜索树

截断续写(truncate-and-resume)的流程是: 模型照常写完整段证明, 交给 Lean; 全对就结束; 有错就在第一条错误处截断, 丢掉后面的代码, 把成功的前缀加上 Lean 返回的最新 tactic 状态注释, 作为下一轮的提示(源文 §1, §3.1). 截断出来的前缀按 tactic 切开, 每条 tactic 连同它前面的 CoT 注释构成搜索树的一条边, 代表一次状态转移. 这样整证生成就有了一个状态-动作接口, 树搜索可以挑任何一个节点续写, 不必只从末尾一条成功的 tactic 往下接.

几个细节是为 Lean 的特点定制的. 不同 tactic 写法可以到达同一个状态, 所以每个节点存一组等价的 tactic 代码, 续写时随机抽一条当前缀. 一次扩展模型会写出多条 tactic, 所以一次扩展可能往树里插入一整条节点路径, 这和 AlphaZero 那类棋类 MCTS 每轮只扩一层不同. 选择阶段用了 virtual node: 每个节点带一个虚拟子节点, 选中它就表示「就在这里扩展」, 于是非叶节点也能被反复扩展. 这对生成模型是必要的, 因为同一个节点能续写出的内容没有上限, 不能像棋盘那样把合法着法列全. 附录 A 的 aime_1983_p9 展示了续写时模型看到的东西: 提示末尾的注释写着当前目标 12 * (x * x.sin) ≤ 9 * (x ^ 2 * x.sin ^ 2) + 4, 模型在 CoT 里把它整理成 $(3x\sin x-2)^2\ge0$ , 末尾一行 nlinarith [sq_nonneg (3 * x * Real.sin x - 2)] 收尾.

和纯逐步搜索相比, 这套接口每次扩展只调一次模型, 一次 Lean 验证, 却可能推进多步, 通信密度低得多. 代价是每次验证都要把整段前缀连同新代码一起交给 Lean 重新检查, 前缀越长, 单次验证越贵, 报告没有给单次验证的平均耗时. 和纯整证重采样相比, 它保住了已经验证过的前缀, 同一道题的第二百次尝试不必再从头写 have h1 : 0 < x * Real.sin x. 同一套训练目标既能单遍采样又能进树搜索, 报告把这当作方法的主要结构贡献(源文 §3.5), 部署时可以按算力在两者之间切换, 不用维护两套模型.

MCTS 的四步里, 模拟被并进了扩展: 整证生成模型从被选节点往下写到底, 本身就是一次 rollout. 回传时沿本轮的选择路径, 对每个 $(s,a)$ 更新两项统计: 经过它的轨迹数 $N(s,a)$ 和这些轨迹的奖励和 $W(s,a)$ , 利用项取 $W/N$ , 探索项是随访问次数衰减的 UCB 奖励. 式 4–6 是 UCB1 的原始写法, 实际采用的是式 7–9 的折扣版, 越早的轨迹权重越低. 外在奖励只有证完时的 1, 所以在找到证明之前, $W$ 全部来自下一节的内在奖励. 这里的「动作」包括虚拟节点代表的「就地扩展」, 所以一个节点被反复选中扩展, 统计也会累积在它的虚拟子节点上.

2.2. RMaxTS: 没有外在奖励时靠新状态指路

树搜索的外在奖励只有一种: 整题证完给 1, 否则 0. 证完之前所有节点的价值估计都是 0, 标准 UCT 此时只按访问次数挑节点, 和盲目展开差不多. RMaxTS 借用 RMax 的想法: 一次扩展只要往树里加了至少一个新节点(也就是看到了新的 tactic 状态), 内在奖励就是 1, 否则是 0(式 3). 证完之前轨迹奖励完全由内在奖励决定, 流程接近 ZeroRMax. 同一状态可以由多种代码到达, 奖励「新状态」而不是「新代码」, 能减少写法不同但状态相同的重复生成.

内在奖励有一个特点: 树越大, 越难碰到新状态, 奖励的期望随搜索进行不断下降, 是非平稳信号. 标准 UCB1 假设奖励分布不变, 靠大量访问逐渐收敛, 有限预算下, 早期积累的高奖励记录会一直压着估计值. 所以报告改用折扣 UCB(DUCB, 式 7–9), 每来一条新反馈, 旧记录按 $\gamma=0.99$ 衰减. 内在奖励和两种 UCB 分别写成:

R_{\mathrm{intrinsic}}(\tau)=\mathbb{I}[\text{本次扩展至少向树中加入一个新节点}],

Q_{\mathrm{UCB1}}(s,a)=\frac{W(s,a)}{N(s,a)}+\sqrt{\frac{2\ln\sum_{a'}N(s,a')}{N(s,a)}},\qquad W=\sum_{\tau\in\Gamma(s,a)}R(\tau),\ N=|\Gamma(s,a)|,

Q_{\mathrm{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)}},\qquad W_\gamma=\sum_{t=1}^{N(s,a)}\gamma^{N(s,a)-t}R(\tau_t),\ N_\gamma=\sum_{t=0}^{N(s,a)-1}\gamma^t.

$\Gamma(s,a)$ 是经过 $(s,a)$ 的所有轨迹. UCB1 的利用项是历史奖励的算术平均, 前一百次扩展都拿到新节点, 后一百次都没拿到, 均值仍是 0.5. DUCB 的 $W_\gamma$ 给第 $t$ 条轨迹乘 $\gamma^{N-t}$ , 最近一条权重 1, 一百条之前约 0.37, 利用项变成近期奖励的加权平均, 上例会掉到约 0.27. $N_\gamma$ 是同一组权重之和, 上界是 $1/(1-\gamma)=100$ , 访问再多也不超过 100, 所以探索项不会像 UCB1 那样随 $N\to\infty$ 趋于 0, 被冷落的分支总保有一份被重新选中的机会. 这两处合起来, 就是「新状态挖空的节点价值很快降下来, 让位给别处」的具体实现. 这里的折扣作用在搜索迭代轮次上, 不是单条轨迹内部的时间步, 和 MDP 里的折扣因子含义不同, 报告专门提醒了这一点.

这套内在奖励属于强化学习里基于计数和新奇度的探索家族, 报告引用了 Bellemare 等的伪计数和 Burda 等的 RND. 这类方法有一个老问题: 新奇不等于进展. 在证明搜索里, 一条 tactic 把目标改写成更复杂的形式, 或者引入一个无关的中间结论, 同样会产生新状态, 同样拿到奖励 1, 搜索会被引向这些方向. RMaxTS 没有任何机制区分「离证完更近的新状态」和「只是不一样的新状态」, 这正是结论节说缺一个 critic 的原因. 在 miniF2F 这种短证明为主的集合上, 这个问题不严重, 因为证明树本来就浅; 证明一旦变长, 无差别的新奇奖励可能会让树横向铺得很宽.

并行化决定了这套方法能不能跑起来(源文 §3.4). 每个计算节点起 256 个 MCTS runner, 每张 GPU 一个模型, 生成 batch 512; Lean 通过 REPL 调用, 跑在数千核的 CPU 集群上, 每次验证一个沙箱进程, 生成和验证都是异步的. 每棵树 32 个线程并发做选择-扩展-验证-回传, 进行中的迭代先回传虚拟奖励 0(virtual loss), 避免多个线程挤到同一节点. 报告没有给出总 CPU 核时和 GPU 时.

3. 实验

3.1. 消融能证明多少

图 5 在 RL 模型 CoT 模式下拆 RMaxTS 的组件. 4×6400 预算时: 单遍 58.4%±0.5%, UCT 无内在奖励 58.2%±0.3%, 内在奖励配 UCB1 58.6%±0.3%, 去掉 tactic 状态 58.4%±0.3%, 完整 RMaxTS 59.6%±0.6%. 16×6400 时依次是 60.2%, 61.1%, 60.7%, 61.1%, 62.7%. 报告据此得出三点: 没有内在奖励, 树搜索退化到接近不搜索; 内在奖励必须配 DUCB; tactic 状态注释是树搜索有效的必要条件.

方向上这三点和数据一致, 但幅度要换算成题数看. miniF2F-test 共 244 题, 1 题约 0.41 个点. 16×6400 下完整 RMaxTS 约证出 153 题, 三个消融版本约 148–149 题, 单遍约 147 题. 也就是说, 在十万级采样上, 内在奖励, DUCB, 状态注释各自的贡献都在 4–5 题左右, 而 16×6400 这一档没有给标准差. 结论可能是对的, 但证据比正文的措辞弱. 表 3 里还有一处值得核对: SFT 模型的 non-CoT & CoT 混合 (2+2)×6400, 单遍和 RMaxTS 两行都是 56.1%±0.8%, 连标准差都相同, 可能是巧合, 也可能是抄录错误, 报告没有说明.

小预算下树搜索几乎不起作用, 这一点正文没有强调. 表 1 里 RL 单遍 3200 次 54.9%, RL + RMaxTS 1×3200 55.0%; SFT 单遍 3200 次 53.3%, SFT + RMaxTS 53.5%. 两处都只差 0.1–0.2 个点, 不到一题. 树搜索的收益主要出现在 4×6400 以上, 这和「内在奖励要积累足够多的新状态才开始有…448 tokens truncated…0 次生成. 但一次整证生成最长 2,048 token, 一次逐步生成只写一条 tactic, 按 token 或按验证调用次数算, 两边的差距会小得多, 报告没有给 token 口径的对比. 另一个量级: 32×6400 即每题 204,800 次整证生成, 244 题合计约 5000 万次, 每次都要 Lean 验证, 这就是 §2.2 那套数千核集群存在的原因.

ProofNet(表 2): RL 单遍 4×6400 全集 22.6%, RL + RMaxTS 全集 25.3%, 测试集 25.3%, 验证集 25.4%, 对照 ReProver 13.8%, InternLM2-StepProver 18.1%. 表注写明 ProofNet 验证集参与了 SFT 的 expert iteration, 所以验证集那一列不能当泛化证据, 只有测试集 186 题是干净的. 测试集上单遍 23.7% 到 RMaxTS 25.3%, 约多证出 3 题. miniF2F 验证集同样进了 SFT 数据, 所以 miniF2F 也只能看测试集. 和 V1 相比, V1.5 把「哪些评测集进了训练」写清楚了, 这是评测口径上的进步.

3.3. CoT 和 non-CoT 各擅长什么

两种模式确实互补. 附录 B.1 里 non-CoT 赢的题, 比如 induction_pord1p1on2powklt5on2 和 imo_1960_p2, 证明是一串 field_simp, nlinarith, norm_num, 靠 Lean 自动化硬算过去; B.2 里 CoT 赢的题, 比如 mathd_algebra_459 先在注释里把四元方程组解出 $d=13/15$ , 再逐个 have 落到代码. 混合策略把预算对半分, RL + RMaxTS 在 (16+16)×6400 时 63.5%, 比纯 CoT 的 16×6400 62.7% 多约 2 题, 而总预算是后者的两倍. 所以混合策略的增益里, 一部分来自多花了一倍的 TestingTime 算力, 一部分来自两种模式覆盖不同题目, 表 3 没有给等预算下纯 CoT 32×6400 的数字, 两者分不开. 推理模式如何影响思考能力, 更一般的讨论见推理与思考能力.

4. 局限与谱系位置

报告的结论节把整条流水线比作 AlphaZero: expert iteration 和合成数据是试错循环, Lean 编译器是世界模型, 树搜索负责探索. 作者自己承认只做了探索这一半, 利用这一半没做: 没有 critic 给不完整的证明打分, 也就没有逐步信用分配和剪枝, 搜索靠的是好奇心和访问统计. 另一个方向是从单个定理走向多定理的 Lean 文件级证明, 报告说模型已有一定文件级上下文理解, 但没有给评测.

谱系上, V1.5 夹在两代之间. 往前看, 它继承了 V1 的合成数据和整证生成范式, 以及 DeepSeekMath 的基座和 GRPO. 往后看, 2025 年 4 月的 Prover-V2 换了思路: 用 DeepSeek-V3 把难题拆成一串 have 子目标, 由一个 7B prover 递归证每个子目标, 拼起来的完整证明加上 V3 的 CoT 做冷启动数据, 再用 GRPO 训 671B 模型, miniF2F-test Pass@32 82.4%, Pass@8192 88.9%. V1.5 的 CoT 注释由外部大模型写, V2 的 CoT 由通用大模型负责拆题, 形式化那一侧交给专用 prover, 分工更明确. RMaxTS 在 V2 的公开材料里没有再作为主推方法出现, 子目标分解接替了「把长证明拆短」这个角色. V1.5 留下来的是两样东西: 用 Lean 0/1 做 GRPO 奖励的做法, 以及截断续写这种让整证模型读到编译器状态的接口.

还有一样常被忽略: V1.5-Base 本身成了开源形式证明的底座. Goedel-Prover 就是在 V1.5-Base 上做的 SFT, 并且用 V1.5-RL 为 expert iteration 的第一轮生成证明. 这说明继续预训练那一步虽然在报告里只占一段, 数字也只涨了约 2 个点, 却是后来者最愿意复用的部分. 对只有单机的读者, 最有参考价值的数字是单遍 128 次的 51.6% 和 3200 次的 54.9%; 树搜索那几档依赖数千核验证集群, 在个人环境里很难复现.

5. 实验与统计口径

消融能证明多少. 图 5 在 RL 模型 CoT 模式下拆 RMaxTS 的组件. 4×6400 预算时: 单遍 58.4%±0.5%, UCT 无内在奖励 58.2%±0.3%, 内在奖励配 UCB1 58.6%±0.3%, 去掉 tactic 状态 58.4%±0.3%, 完整 RMaxTS 59.6%±0.6%. 16×6400 时依次是 60.2%, 61.1%, 60.7%, 61.1%, 62.7%. 报告据此得出三点: 没有内在奖励, 树搜索退化到接近不搜索; 内在奖励必须配 DUCB; tactic 状态注释是树搜索有效的必要条件. 方向上这三点和数据一致, 但幅度要换算成题数看. miniF2F-test 共 244 题, 1 题约 0.41 个点. 16×6400 下完整 RMaxTS 约证出 153 题, 三个消融版本约 148–149 题, 单遍约 147 题. 也就是说, 在十万级采样上, 内在奖励, DUCB, 状态注释各自的贡献都在 4–5 题左右, 而 16×6400 这一档没有给标准差. 结论可能是对的, 但证据比正文的措辞弱. 表 3 里还有一处值得核对: SFT 模型的 non-CoT & CoT 混合 (2+2)×6400, 单遍和 RMaxTS 两行都是 56.1%±0.8%, 连标准差都相同, 可能是巧合, 也可能是抄录错误, 报告没有说明.

小预算下树搜索几乎不起作用, 这一点正文没有强调. 表 1 里 RL 单遍 3200 次 54.9%, RL + RMaxTS 1×3200 55.0%; SFT 单遍 3200 次 53.3%, SFT + RMaxTS 53.5%. 两处都只差 0.1–0.2 个点, 不到一题. 树搜索的收益主要出现在 4×6400 以上, 这和「内在奖励要积累足够多的新状态才开始有区分度」的机制是一致的. 对只能跑几千次采样的使用者, 单遍整证生成基本就是全部收益. 主结果和预算口径. miniF2F-test(表 1): RL 单遍 128 次 51.6%, 3200 次 54.9%, 16×6400 次 60.2%, 比 V1 的 50.0% 高 10.2 个点; RL + RMaxTS 16×6400 62.7%; 用 CoT 和 non-CoT 各一半预算的混合策略, 32×6400 到 63.5%. 对照组里 InternLM2-StepProver 54.5%, Lean-STaR 46.3%, HTPS 41.0%, GPT-f 36.6%, COPRA + GPT-4 26.6%. 摘要里的 63.5% 同时用了 RL, RMaxTS 和混合提示三样东西; 只看模型本身, 应该看单遍的 60.2%. ICLR 2025 版正文把主结果写成 62.7%, 没有把混合策略的数字当标题.

评测协议写在源文 §2.4. 每个模型单卡 A100-40G, 用 vLLM 采样, 温度 1, top-p 0.95, 最多 2,048 token; 验证时导入 Mathlib4 和 Aesop, 单题时限 300 秒. miniF2F 和 ProofNet 原本都是 Lean 3, 作者手工转成 Lean 4.9.0, 比 V1 用的 v4.7.0-rc2 新. 这意味着 V1 的 50.0% 和 V1.5 的数字不是在完全相同的语句文件和工具链上测的, 表 1 里 V1 那一行是在哪个版本上重跑的, 报告没有说明. Base 模型用 3-shot, 示例从验证集随机抽: miniF2F 用 Yang(2023) 的人写证明, ProofNet 则用 V1.5-RL 生成的正确证明当示例. 用最终模型的输出去给 Base 做示例, Base 在 ProofNet 上的 9.7% 就不完全是 Base 自己的水平, 报告没有讨论这一点. SFT 和 RL 模型不用 few-shot, 改用 CoT 或 non-CoT 两种引导提示.

预算怎么比是这一节最容易读错的地方(源文 §4.1). 单遍方法按总生成数记, best-first 按 $N\times S\times T$ 记, 树搜索按 $N\times T$ 记. 报告称 3200 次整证就超过 InternLM2-StepProver 的 64×32×100 次, 后者折合 204,800 次生成. 但一次整证生成最长 2,048 token, 一次逐步生成只写一条 tactic, 按 token 或按验证调用次数算, 两边的差距会小得多, 报告没有给 token 口径的对比. 另一个量级: 32×6400 即每题 204,800 次整证生成, 244 题合计约 5000 万次, 每次都要 Lean 验证, 这就是 §2.2 那套数千核集群存在的原因.

表 3 显示 CoT 相对 non-CoT 的优势随预算放大: 单遍 RL 模型 4×6400 时 CoT 58.4%, non-CoT 56.5%, 16×6400 时 60.2% 对 57.4%. 报告的解释是自然语言注释让规划路径更多样, 大预算时能覆盖更多不同的证明思路. 这个解释和数据方向一致, 但和 §1.3 提到的问题连在一起看: 注释不受 Lean 检查, 多样性可能部分来自注释本身带来的随机扰动, 而不全是「更好的规划」, 报告没有做区分这两者的实验.

1-(1-p)^k.

真实评测通常从 $n$ 个 sample 中估计 pass@ $k$ , 常用无偏估计器根据失败数 $c$ 计算组合比例. 当所有候选同分布且独立时, $k$ 增大单调接近至少一次成功概率. 模型样本高度相关, 有效多样性低于 $k$ . V1.5 的大预算写成多组 $6400$ , 可能通过不同随机运行聚合 theorem 是否至少成功. 表中百分比是 244 个 theorem 的通过比例, 并非单题平均 $p$ . 有些题在前几十次就成功, 有些题十万次仍失败, 总曲线反映难度混合. pass@k 奖励覆盖面, 不关心正确证明概率质量. 一个模型每题只有万分之一概率成功, 给足预算也可能有高 pass; 线上单次使用却很差. Pass@128 更接近有限部署, 16×6400 展示支持集与搜索上限. 两种口径都重要.

树搜索样本不独立, 不能直接套 $1-(1-p)^k$ . 后续扩展依赖先前发现状态, $k$ 代表自适应查询次数. 把 RMaxTS 与独立采样按相同生成数比较有直观意义, 统计模型不同. 题目数如何限制小差值解释. miniF2F-test 有 244 题, 单题约 0.41 个百分点. 0.1 或 0.2 点差小于一题, 来自多次运行平均或四舍五入, 不应写成实质提升. 1 点约 2–3 题, 2.8 点约 7 题. 把百分点换成题数能恢复直觉. 同一模型不同 seed 会改变哪些题被证明. 论文对部分设置报告标准差约 0.3–0.8 点, 与一到两题相当. 完整大预算缺少所有对应方差, 63.5 与 62.7 的 0.8 点差未必稳健, 而且预算不同.

题目不是同质 Bernoulli. 多道题可能共享 nlinarith 模式, 一项能力变化会成组影响, 简单二项置信区间低估相关性. 更有信息的报告应列配对翻转: SFT 未证而 RL 证出的题, RL 退化的题, RMaxTS 独有题及证明长度. ProofNet test 186 题, 单题约 0.54 点. RMaxTS 从 23.7 到 25.3 约多 3 题. 这是正向信号, 规模远小于 miniF2F 的主标题增益, 也说明搜索收益随领域与证明深度变化. miniF2F 与 ProofNet 的分布差异. miniF2F 主要是中学竞赛题, 大量代数、数论与不等式可由 linarith、nlinarith、norm_num、ring 等自动化收尾. 自然语言 CoT 容易提出中间等式, Lean tactic 生态也与数据中常见模式吻合. ProofNet 来自本科数学陈述, 涉及更广定义、分析与抽象结构. 证明需要选择库 lemma、处理类型类和拓扑/代数环境, 单靠算术 tactic 不够. V1.5 的 RL 提示只有 4.5k, 来自 SFT 中等难度题, 领域覆盖可能偏 miniF2F 风格.

这解释 RL 在 miniF2F 稳定优于 SFT、ProofNet 某些预算却持平或回退的可能原因. 它是分布假设, 论文没有按领域列训练题和错误类型. 不能把 miniF2F 上「RL 增强基础能力」直接外推到全部 Lean 数学. ProofNet validation 进入 SFT expert iteration, test 才能用于泛化. Base few-shot 又用了 V1.5-RL 生成的证明当示例, 不同模型行的上下文信息不完全对齐. 这使表格适合比较最终系统, 不适合纯 checkpoint 归因. CoT 模式的成本口径. CoT 在每条 tactic 前写解释, 输出 token 明显多于 non-CoT. 相同 sample 数下, GPU 解码时间、KV cache 和截断概率不同. CoT 分数高不能直接称为免费提升, 应报告每个成功证明的平均 token 与时间. 2048 token 上限对两模式影响不同. non-CoT 能容纳更多 tactic, CoT 可能在代码完成前被解释耗尽. 短 miniF2F 中规划收益超过长度代价; 长证明可能反转. 论文没有按证明长度分桶.

混合模式的互补还可能只是增加多样性. 用两个 prompt 形成两个采样分布, 类似 prompt ensemble. 若换成多种 non-CoT 提示也可能覆盖更多证明. 要隔离自然语言推理, 需要等 token、等 prompt 数与等总预算比较. 消融缺少哪些轴. RMaxTS 消融覆盖内在奖励、UCB/DUCB 与状态注释, 没有扫描 $\gamma$ 、线程数、每次 rollout 长度、状态合并规则和模型温度. 搜索组件相互作用, 固定一个配置的移除实验只能说明该点附近贡献. 训练侧缺少纯 tactic state、纯 CoT、两者同时和无注释的完整矩阵. SFT 数据、预训练与 expert iteration也没有规模曲线. 因而 CoT 与状态监督各自对单遍和搜索的贡献难以拆分. RL 侧缺少提示数量、组大小、KL 与训练步数消融, 也没有训练 reward、entropy 和验证曲线. 1–3 点增益可以确认, 为什么产生以及是否已经饱和仍未知.

最终缺少等成本对照. 增加独立 sample、RMaxTS、best-first 与逐步 prover 应按 GPU token、Lean CPU 与墙钟比较. 论文使用生成次数作为统一轴, 有利于展示算法, 不能回答真实集群的性价比. 从 pass 曲线反推题目分层. 若所有题拥有相同单次成功率, pass 曲线会由一个 $p$ 决定. 实际从 128 到十万 sample 仍增长, 说明题集至少包含三层: 高概率题早早通过, 低概率题需大预算, 零支持题始终失败. 曲线尾部上涨来自第二层. RL 若只重排已有 proof, 可能让高概率题更早通过, 大 $k$ 最终与 SFT 汇合. 表中大预算差距没有消失, 支持 RL 让部分题从近零概率进入可采样尾部, 或扩大了正确证明多样性. 它仍未达到证明「创造全新推理算法」的强度.

RMaxTS 的目标是把第二层题的合法前缀组合起来. 对高概率短题, 独立 sample 足够; 对零支持题, 树也无合法 proposal. 所以搜索增益集中在中间层, 与 RL 的中等难度训练筛选形成相似结构. 若报告按题目单遍成功率分桶展示搜索增益, 可以直接验证这一解释. 论文没有该图, 只能从预算曲线间接判断. 混合策略怎样区分互补与额外预算. 设 CoT 在题集上成功集合为 $A$ , non-CoT 为 $B$ . 混合覆盖率由 $|A\cup B|$ 决定, 互补部分是 $|A\triangle B|$ . 只给两种单独总分与混合总分, 无法求出交集, 因为采样预算和随机性也变化. 等预算实验应把总 sample 固定为 $K$ , 在 CoT/non-CoT 间分配 $\lambda K$ 与 $(1-\lambda)K$ , 扫描 $\lambda$ . 论文的 (16+16)×6400 比纯 CoT 16×6400 多一倍总预算, 混合上涨 0.8 点可能来自额外 sample.

不过附件案例确实显示模式偏好不同. non-CoT 更常简短调用自动化, CoT 更常显式建立中间 have. 这种结构差异给互补提供定性证据. 要量化仍需相同预算和题级翻转表. 标准差与重复运行怎样读. 部分结果写成均值±标准差, 表明多个随机运行或批次. 标准差描述运行间波动, 不等于均值置信区间; 还需要重复次数才能计算标准误. 论文没有在每个大预算格都给完整重复信息. 0.5 点标准差约一题多. 两个设置均值差 0.4 点且区间重叠时, 不应强调排名. 完整 RMaxTS 对某些消融高 1–1.5 点, 方向更可信, 题数仍只有数题. benchmark 题数固定, 重复随机性来自模型采样与搜索调度. 32 线程异步还会因返回顺序改变树, 即使随机 seed 相同也可能不完全确定. 复现应报告多 seed 与调度设置.

与后续强基线比较时的时间顺序. Goedel-Prover 用更大形式化数据在 V1.5-Base 上 SFT, 说明数据覆盖可以超过 V1.5 的 RL 增益. 它发布时间更晚, 使用 V1.5 作为基础, 不能反过来否定 V1.5 当时的方法贡献. Prover-V2 使用更强通用模型分解和 671B RL, 模型规模、数据与任务构造都不同. 它表明路线演进到显式子目标与大模型, 不是 RMaxTS 的受控替代实验. 正确比较方式是把后续结果作为上限与机制启示: V1.5 找到 verifier RL 和状态搜索接口, 后续扩大 theorem 数据与规划能力. 每代主结果的预算也不同, 不能只排一个 pass 百分比排行榜. 用数值理解采样收益递减. 若某题单次成功率 $p=1%$ , 独立采样 128 次的成功率约为 $1-0.99^{128}\approx72.4%$ ; 3200 次几乎必过. 若 $p=0.01%$ , 128 次约 1.27%, 3200 次约 27.4%, 十万次才接近必过. 大预算主要从第二类极低概率题中继续挖答案.

如果 $p=0$ , 任何独立采样都无效. 树搜索可能把多个非零概率正确前缀拼起来, 将整证零支持变成可达; 前提是每个关键局部动作都能由模型提出. 这就是 RMaxTS 相对 best-of- $k$ 的潜在优势. 题集曲线是不同 $p_i$ 的平均. 从表格总 pass 无法反推出单题分布, 同一总分可能由「多数题中等概率」或「一半很易、一半为零」形成. 后者增加 sample 很快饱和, 前者持续上涨. 论文的大预算曲线提供部分形状信息, 没发布题级 $p_i$ . 采样收益递减还决定资源分配. 与其给已高概率题继续上万 sample, 可以根据早期失败动态把预算移给边界题; 但早期没成功也可能是极难零支持题. 一个 value 或难度估计器能改善分配, RMaxTS 用状态新奇作为局部代理. 最低可复现实验应报告什么.

模型侧需要 checkpoint、prompt 模式、temperature、top- $p$ 、最大 token 与 sample 数. Lean 侧需要版本、Mathlib commit、导入、heartbeat、墙钟超时和禁用 escape 规则. 数据侧需要 test 文件摘要以及 validation 是否进训练. 搜索侧还要记录 runner、线程、virtual loss、 $\gamma$ 、状态去重和每次 expansion 的生成数量. 成本侧记录 GPU token、Lean calls、CPU 秒与墙钟. 只报告 N×T 无法让不同硬件与方法公平比较. 结果侧除 pass@k, 还应给题级成功、证明长度、Lean 时间、CoT token、unique states 与多 seed 方差. 这些指标能区分 checkpoint 更强、搜索更广、自动化更重和预算更多. V1.5 已公开论文、模型与仓库, 为复现提供了主体. 未公开预训练数据配比、完整训练日志和集群成本, 所以最容易复现的是 checkpoint 推理与小预算 pass, 最难复现的是从 Base 到 RL 的整条训练和十万级 RMaxTS.