02 · DeepSeek-Prover: 用 Lean 核验器当过滤器, 合成 800 万条形式证明

来源: DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data (arXiv: 2405.14333v1, 2024-05-23).

DeepSeekMath 在结论里承认几何和定理证明是短板, 三个月后的 DeepSeek-Prover 就对准了其中一块: 用 Lean 4 写出能被机器核验的证明. 模型和底座都没变, 仍是 DeepSeekMath-Base 7B, 训练方法也只是普通的监督微调. 这篇报告的全部分量都在数据上: 把网上爬来的约 87 万道竞赛题自动翻成 Lean 语句, 过滤, 证明, 用 Lean 核验器判对错, 通过的样本回流训练, 滚四轮得到约 800 万条带证明的形式语句. 读它要换一个视角: 这里的「数据流水」本身就是算法, Lean 核验器同时扮演标注员和质检员.

1. 数据合成流水

1.1. 问题: 形式证明缺的是平行语料

Lean, Isabelle, Coq 这类证明助手把命题和证明都写成代码, 内核按形式规则逐步检查, 通过才算证完. 可靠性远高于自然语言证明, 代价是写起来慢, 资深数学家也要花大量时间. 神经定理证明此前有两条路. 一条是模型引导的树搜索: 模型逐步给出 tactic, 和证明器交互, 按搜索算法扩展, 代表是 GPT-f, ReProver, Hypertree Proof Search, 搜索空间大, 算力贵. 另一条是整证生成: 模型一次写完整个证明脚本, 交给证明器判对错, 代表是 Baldur, Draft-Sketch-Prove, 省掉交互, 但一次写对很难.

更早的一阶定理证明器, 比如 E 和 Vampire, 在简单逻辑框架里很高效, 但处理不了证明助手里常见的高阶, 带大量库定义的命题. 神经方法把这个领域重新激活, 不过树搜索那条线多用 RL 提升准度, 搜索本身耗时耗算力; 整证生成那条线跳过了逐步交互, 效率更高, 却更依赖模型一次写对的能力, 也就更依赖训练数据.

两条路都卡在同一个地方: 形式语料太少. Python 这种语言在 GitHub 上有海量代码可学, Lean 的 mathlib 虽然是最大的形式数学库, 规模和自然语言数学相比仍然小几个数量级. 自动形式化(把自然语言题目翻成形式语句)能补一些, 但此前的工作规模都不大. 报告的判断是: 模型架构和搜索算法不是主要瓶颈, 训练数据是. 所以他们不改模型, 不改搜索, 只造数据. 此前造形式数据的办法有两类: 一类对已有定理做基于规则的变换, 能批量生成, 但受限于预先写好的规则, 变不出新的题型; 另一类用大模型把自然语言题翻成形式语句, 灵活, 但已有数据集规模小, 只覆盖几个小基准, 训练收益有限. DeepSeek-Prover 选的是第二类, 目标是把规模做大两个数量级以上. 表 2 的对照直接说明了语料的差距: 同样用 expert iteration, 只用 mathlib 的人写定理, 训练 token 只有 0.238B; 用自动形式化的语句, 训练 token 到 3.108B, 多了一个数量级.

1.2. 起点: 冷启动一个会翻译的模型

整个流水需要一个会「把题目翻成 Lean」的模型, 但 DeepSeekMath-Base 一开始几乎不会. 冷启动用 MMA 数据集: 它把 mathlib 里的 Lean 4 语句用 GPT-4 反向翻成自然语言题目, 于是得到「自然语言到 Lean」的平行样本, 在上面微调一下, 模型就能按固定模板把题目翻成 Lean 4 声明. 模板要求只输出核心声明, 包在代码块里, mathlib 固定到某个 commit, Lean 固定在 v4.7.0-rc2. 版本固定这件事看似琐碎, 实际很关键: mathlib 引理的名字和签名会随版本变, 同一段证明在新版本上可能就过不了.

题源的选择也有讲究. 报告观察到, 条件明确, 目标清楚的竞赛题比需要复杂定义和构造的高等数学容易形式化, 所以主攻高中和本科竞赛题, 以代数和数论为主, 组合, 几何, 统计为辅. 这类题陈述简单, 解法可能不浅, 适合做证明训练数据. 自然语言题目从网上的习题, 考试, 竞赛资源爬取清洗, 得到 869,659 道. 爬了哪些网站, 怎么清洗, 报告没有细节. 这也埋下一个问题: 竞赛题来源和 miniF2F 的题源(AMC, AIME, IMO, MATH)高度重合, 报告通篇没有提到去污染, 后面读 miniF2F 分数时要把这一点记在心里.

1.3. 质量过滤: 打分和假设否决

自动形式化的产物有两类典型问题. 一类是太简单, 翻出来的语句平凡到没有训练价值. 处理办法是让模型自己打分: 标准包括与当前研究的相关性, 复杂度与深度, 跨学科潜力, 社区缺口, 创新性; 用 miniF2F-valid 的例子做 few-shot, 让模型用 CoT 把语句评成 excellent, good, above average, fair, poor 五档, fair 和 poor 丢弃. 人工抽查认为打分接近人的直觉. 表 3 用等量的高分档和低分档数据分别微调底座, pass@128 下 miniF2F-test 从 38.1% 到 42.6%, valid 从 41.4% 到 48.8%, 差约 4.5 个点. 这个设计有一个副作用: miniF2F-valid 进了打分提示, 它作为评测集的干净程度就打了折扣, 读 valid 分数时比 test 更要谨慎.

打分提示的输出格式在附录 A.1: 模型先把 Lean 代码翻回自然语言, 写出背景, 假设和定义, 再逐条给五个维度写理由, 最终给出总评. 先回译再打分, 相当于顺带做了一次语义检查, 翻不回通顺题意的语句多半会被打低分.

「与当前研究的相关性」「社区缺口」「创新性」更接近论文评审维度, 对一道练习题未必容易稳定判断; 「复杂度与深度」则能直接排除 1 + 1 = 2 一类平凡语句. 报告只说人工抽查结果符合直觉, 没有给出抽查规模、一致率、五档比例以及 fair、poor 的淘汰占比. 表 3 说明整套过滤有效, 但没有比较五维标准与单独使用难度评分的差异.

另一类问题更隐蔽: 语句可以被证明, 但前提自相矛盾, 结论是空虚真. 报告的例子是假设「对所有复数 $z$, $z^2=-1$ 且 $z^3=-1$ 且 $z^6=1$」, 前提本身就假, 推出什么都没有意义. 处理办法是假设否决: 把结论换成 False, 让模型试证, 证出来就说明前提矛盾, 整条丢弃. §5.2 的行列式案例把这种错误的样子展示得很清楚: 模型把「存在 a, b, c 使行列式为 D」写成「对所有非零 a, b, c, 行列式都等于同一个 D」, 然后代入两组具体值算出不同的行列式, 用 linarith 推出矛盾. 这类量词错误在人眼里很像一个正常定理, 靠核验器反证才能稳定抓出来. 两道过滤之后, 87 万道题剩 712,073 条语句.

假设否决有一个结构上的盲区: 它只把冒号后面的结论换成 False, 检查的是冒号前面那些假设. 如果矛盾藏在结论内部的蕴含前件里, 或者藏在量词结构里, 这一步就看不见. 附录 A.2 被当作成功样例的两条语句正好说明了这一点. 例 a 要证「若对所有 $x$, $f(x)\le0$ 蕴含 $x<-1$ 或 $x>1$, 则 $a=3$」, 其中 $f(x)=x^3-ax-1$. 但 $f(0)=-1\le0$ 而 $0$ 不在那两个区间里, 所以这个前件对任何 $a$ 都不成立, 整条命题是空虚真. 模型给的证明正是把 $x=0,1,-1$ 代进前件, 再用 linarith 收尾. 前件写在冒号之后, 假设否决根本不会去检查它. 例 b 的形式是 ∃ k, f k = … → (∃ m, F m = … → m = k), 取 $m=k$ 内层就直接成立, 同样平凡, 证明也只是一行 simp 加 aesop. 报告对这两例的分析只评价了算子翻译得对不对(区间并, Nat.choose), 没有指出语义上已经空了(以上为读附录代码的判断). 这说明 20% 错误率只是下限, 通过核验的语句里仍有一部分在教模型「找平凡出口」.

自动形式化的提示也影响语句形态. 模板里的输入是 informal_statement_with_answers, 即题目连同答案一起给模型. 求值题因此被改写成「证明答案是某个数」的形式, 这是把计算题变成可证命题的关键一步; 代价是答案若本身有误, 翻出来的语句就是假命题, 要靠后面的否定并行兜底.

1.4. 扩大证明池: 同时证原命题和它的否定

过了过滤, 语句仍然不保证为真. 报告估计即使过滤后, 也至少有 20% 的自动形式化语句是错的. 这在大规模合成里是算力黑洞: 人写的定理基本都成立, 可以放心一直搜; 机器翻出来的假命题, 模型会一直试到超时. 对策利用命题和否定的对称性: 对 $\Gamma\vdash P$ 和 $\Gamma\vdash\neg P$ 并行搜索, 各试最多 $k$ 次, 任何一边先找到能通过核验的证明就停. 按尝试次数算一下代价. 只搜 $P$ 时, 真命题在第 $j$ 次证出花 $j$ 次, 假命题一定烧满 $k$ 次. 双路并行时, 真命题在第 $j$ 次证出花 $2j$ 次, 多付一倍; 假命题若否定在第 $j'$ 次证出, 只花 $2j'$ 次, 只要 $j'<k/2$ 就比单路省; 两边都证不出的语句, 代价从 $k$ 变成 $2k$. 所以这套做法划不划算, 取决于假命题占比和否定证明来得多快. 报告没给 $k$ 的取值, 也没给这几类语句各占多少.

这一步同时解决了两件事. 算力上, 假命题通过证出否定被提前判死, 不再烧满超时预算. 数据上, 两边的证明都能进训练池: 证出原命题得到正样本, 证出否定也是一条合法的 Lean 证明, 形式化写错的语句反而变成了训练数据. 和 expert iteration 的原始做法相比, 这是最关键的改动. Expert iteration 默认待证命题都是真的, 只需要不断采样直到证出来; 自动形式化打破了这个前提, 必须给不可证的命题一个出口. 从社区对这篇的讨论看, 「否定并行」也是被引用最多的工程细节, 因为它几乎不增加复杂度, 却把合成流水的效率提高了一截.

否定并行和假设否决分工不同. 假设否决在证明之前把结论换成 False, 检查前提是否自洽; 否定并行在证明阶段检查结论本身是否成立. 一条语句可能前提自洽但结论错误, 比如题目要求证明某个方程的解是 3, 模型翻译时把答案写成了 4, 这种错误只能由否定并行发现. 两道关口分别覆盖前提错误和结论错误. 报告没有给出否定一侧的证明比例以及训练池中的否定证明占比. 错误语句超过 20% 也不代表否定证明达到同一比例, 因为不少错误语句可能两侧都搜索失败. 这部分样本训练模型反驳错误命题, 它对只含真命题的 miniF2F 是否有帮助, 报告没有单独消融.

1.5. 迭代: 弱模型滚成强模型

四个环节串成闭环: 形式化, 过滤, 证明, 用核验通过的样本微调, 更强的模型再回去做下一轮形式化和证明, 直到收益变薄. 每一轮的变化是双向的: 模型证得更多, 能进训练池的样本就更多, 而且更难的语句也开始有证明; 模型翻译得更准, 下一轮语句的质量也更高. 表 4 给出 pass@128 的台阶: iteration 0 到 4, miniF2F-test 从 34.0% 升到 39.3%, 41.4%, 45.1%, 46.3%, valid 从 38.1% 升到 59.4%. 涨幅逐轮收窄, test 在第 3 到第 4 轮只涨 1.2 个点.

这个闭环本质上是一种没有梯度信号的 RL. 核验器给出 0/1 奖励, 只保留奖励为 1 的样本做监督学习, 相当于 rejection sampling 加迭代. V1.5 的报告后来明确把这层关系说破: expert iteration 和合成数据对应 RL 的试错循环, 编译器是提供环境反馈的世界模型. 和 DeepSeekMath 的 GRPO 相比, 这里没有负样本的梯度, 也没有组内相对优势, 失败的证明被直接丢弃. 这种做法的好处是稳定, 坏处是浪费了失败样本里的信息, V1.5 用 RLPAF 补的就是这一块.

训练设定只给出底座 DeepSeekMath-Base 7B、全局 batch 512、恒定学习率 $1\times10^{-4}$ 和 6000 步 warmup. 每轮训练步数、新增样本数及轮次间的数据混合比例均未公开. 因此表 4 的逐轮提升无法分解为数据规模增加和数据难度提高各自的贡献.

几个数字放在一起能粗看训练量级. 光 warmup 就是 6000 步 × 512 条, 约 307 万条样本, 相当于 800 万条数据的四成, 说明每轮微调不是轻量的几百步. 表 2 里自动形式化那一行写的训练量是 3.108B token, 如果它对应的是全部证明样本, 平均每条约 390 token, 这和附录里那些十行以内的短证明在量级上吻合. 和 DeepSeekMath 500B token 的续训相比, 形式证明这一步的训练量小了两个数量级, 模型能力的底子仍在数学预训练里.

过滤后的语句是 712,073 条, 最终数据集却有 8,066,621 条, 贡献列表还写着「800 万条形式语句, 每条都带一个形式证明」. 两个数相差十多倍, 报告没有分解其来源. 可能因素包括跨轮累积、同题多种形式化、同一语句的多个证明以及否定侧证明. 即使按 5 轮、每轮 71 万条粗算, 总量也只有约 350 万, 因而数据集中必然还存在一题多译或一句多证. 这里的「800 万」更适合按证明样本数理解, 不能直接当作 800 万道不同题目.

2. 实验与评测

2.1. 数据规模和数据来源各自贡献多少

表 2 比较数据来源, 设定都是 pass@128. 底座不做任何形式证明训练时, miniF2F-test 27.5%; 用 mathlib 定理做 expert iteration, 31.2%; 用自动形式化语句, 42.6%. 人写的形式库只能带来不到 4 个点, 自动形式化带来 15 个点. 结论很明确: mathlib 喂不饱一个 7B 证明器, 大规模自动形式化才是主要增益. 顺带一提, 表 3 的高分档和表 2 的自动形式化行数字完全相同(48.8%, 42.6%), 大概率是同一次训练.

表 5 比较数据规模: 从 800 万条里取 1,000, 10,000, 100,000, 1,000,000 和全部 8,066,621 条, test 分别是 24.18%, 31.97%, 37.7%, 38.11%, 40.16%. 规模每涨一个数量级, 分数都涨, 但 10 万到 100 万只涨 0.4 个点, 到 800 万又涨 2 个点, 曲线不是平滑的. 这张表还有两处和别的表对不上. 一是只用 1000 条时 test 24.18%, 比完全不训的底座 27.5% 还低, 小数据微调反而伤了多样本采样. 二是全量 800 万条只有 40.16%, 低于表 4 第 4 轮的 46.3%. 报告没解释, 合理的猜测是表 5 是一次性微调的对照, 表 4 是逐轮迭代的模型, 训练过程不同. 这说明「数据量」和「迭代过程」是两个独立的变量, 800 万条数据一次喂进去, 抵不上边造边训.

2.2. 主结果: miniF2F 与 FIMO

miniF2F 有验证集和测试集各 244 题, 覆盖基础算术到 AMC, AIME, IMO 级竞赛题, 用 LeanDojo 发布的 Lean 4 版. 表 1 是报告最常被引用的一张表. DeepSeek-Prover 整证生成: 贪心约 30.0%, 64 次 46.3%, 128 次 46.3%, 8192 次 48.8%, 65536 次 50.0%. 累计(把所有实验中找到的证明合起来算)valid 60.2%, test 52.0%. 对照组: GPT-4-turbo 0409 在 64 次采样下 valid 25.4%, test 23.0%; 树搜索里最强的 Hypertree Proof Search(600M)累计 valid 58.6%, test 41.0%. 采样从 64 次加到 65536 次, 算力多了 1000 倍, test 只涨 3.7 个点, 说明整证生成在难题上很快碰到上限. pass@k 的定义是「模型生成的前 $k$ 次尝试里至少有一次通过核验」, 按一次实际采样的前 $k$ 条直接计数, 不是 Codex 那种从 $n>k$ 个样本里算 $1-\binom{n-c}{k}/\binom{n}{k}$ 的无偏估计. 如果 64 次和 128 次取自同一串采样, 两者同为 46.3% 就意味着第 65 到 128 条没有为任何新题找到证明; 报告也没给多次运行的方差.

表 1 的上下两部分采用不同预算. 上半部分的树搜索方法以「交互步数乘分支」计量, 下半部分的整证生成方法记录独立采样次数, 两者无法直接换算成同一种算力. 「累计」也不是固定预算下的结果, 它取所有实验找到的证明并集, 与 pass@k 的含义不同. 报告给出的结论限于整证设定: 7B 模型经过合成数据训练后, 64 次采样的分数达到 GPT-4 的两倍, 累计指标超过当时最强树搜索方法的 test 分数. 这组数字没有比较两类方法的等算力表现.

GPT-4 这条基线的设定也要看清. 报告说 GPT-4-turbo 0409 和 DeepSeekMath 都「用和本文类似的方法」生成完整证明, 但没有给 few-shot 示例数量, 导入前缀和温度. GPT-4 没有在 Lean 4 数据上微调, 而当时 Lean 4 和 mathlib 4 的写法相对 Lean 3 变化很大, 通用模型很容易写出旧语法或已改名的引理. 所以 23.0% 对 46.3% 的差距里, 有一部分是「见没见过当前版本的 Lean 4」, 不全是推理能力. 这不影响结论的方向, 但「两倍于 GPT-4」这个说法应当放在这个前提下理解.

FIMO 把 IMO shortlist 翻成 Lean 4, 正文写 149 题, 摘要写 148, 两处不一致. 每题 100 次尝试证出 4 题, GPT-4 为 0; 加到每题 4096 次再多证出 1 题, 共 5 题. 附录里的 FIMO 证例能看到模型会组合 induction, linarith, nlinarith, field_simp, aesop 等 tactic. 从 100 次加到 4096 次只多一题, 说明 IMO 级题目基本在这条路径的能力之外; 能证出的几题, 更像是训练分布边缘恰好覆盖到的题型. miniF2F 上的成功集中在训练数据最密的代数和数论中等难度题, 与 FIMO 的稀疏成功形成对照.

2.3. 评测缺口

评测还留下三处缺口. 训练题面爬自竞赛资源, miniF2F 同样来自 AMC、AIME、IMO, 报告没有检查二者重合度, 也没有给出合成语句与评测语句的相似度. miniF2F-valid 既出现在打分提示的 few-shot 示例中, 又被用来报告 60.2% 的验证分数. 主结果的采样预算从贪心横跨到 65,536 次, 累计指标还是多次实验的并集, 各行消耗的算力差异很大. 表 2 到表 5 的内部对照仍能支持过滤与迭代的收益, 但这些缺口会降低它与外部方法直接比较时的可信度.

附录 A.3.1 列出的 miniF2F-test 证例可以把这个担心说得更具体. 其中一题是 amc12b_2021_p4, 也就是 2021 年 AMC 12B 第 4 题, 另一题 induction_1pxpownlt1pnx 是伯努利不等式的一个归纳证明. AMC 真题及其解答在网上随处可见, 正是「高中与本科习题, 考试, 竞赛资源」会收录的内容. 这不证明它进了训练集, 但说明报告至少应当做一次题面级的重合检查. DeepSeekMath 在自然语言数学上做了 10-gram 去污染, 到了 Prover 这一步反而没有提, 算是这篇报告评测部分最明显的缺口. V1.5 的 SFT 数据甚至直接收入了 miniF2F 的验证集, 只保留测试集做评测, 口径比 V1 清楚.

模型大小也值得一提. 表 1 的树搜索对照里, Hypertree 是 600M, ReProver 是 229M, Proof Artifact Co-Training 是 837M, 多数比 7B 小一个数量级; Llemma 7B 和 34B 是同量级, test 分别 26.2% 和 25.8% 到 29.6%. 所以 DeepSeek-Prover 相对小模型搜索方法的优势, 有一部分来自参数量和数学预训练底座. 表 1 里 DeepSeekMath-Base 在 128 次采样下已有 27.5%, 高于 ReProver 的 25.0%, 就是底座本身的贡献. 在同一个底座上, 合成数据把 27.5…297 tokens truncated… tactic, 评测和合成时前缀不一致, 通过率就会漂移. 复现这篇报告需要同时拿到权重, 导入前缀, Lean 和 mathlib 的确切版本, 缺一样都可能对不上表 1.

附录 A.3.1 的成功证明也有一个共同风格: 很短, 主要靠 Lean 自带的自动化 tactic 收尾. 伯努利不等式那题只有一行 induction', 接一串 simp_all 化简规则, 再用 nlinarith 喂一个平方非负的提示就结束了. 这说明整证明生成学到的更多是「选对 tactic 组合, 给对提示项」, 而不是一步步写出人类式推导. 这种风格和 miniF2F 里大量短代数题正好匹配, 碰到需要多层引理拼接的 IMO 级题目就吃力, FIMO 上 100 次采样只证出 4 题, 和这个观察一致. V1.5 后来引入自然语言 CoT 注释和 RMaxTS 搜索, 目标之一就是补这块长证明的短板.

3. 局限与谱系位置

结论写明的边界: 主战场是高中到本科的代数和数论, 几何, 高等定义, 更广的题型是下一步. 整证生成依赖 Lean 工具链和固定导入, 换证明助手或大改 mathlib 版本都要重建核验流水. 合成数据和模型的开源写在贡献和 Broader Impact 里. FIMO 的 5 题也标出了能力上限: 在极难基准上破零, 离系统性解决竞赛级形式证明还远.

谱系上, Prover 是 DeepSeekMath 的直接延伸. 底座是 DeepSeekMath-Base 7B, 继承了 120B 数学 token 的先验; 训练方法从 SFT 加 GRPO 退回到纯 SFT 加 expert iteration, 因为形式证明有了一个比奖励模型可靠得多的裁判, 也就是 Lean 核验器. 这里第一次出现了家族后来反复使用的一个结构: 能被程序自动判对错的任务, 就用判定器生成和过滤训练数据, 让模型自己滚大数据集. V1.5 在这个基础上补了三样东西: 用 Lean 反馈做真正的 RL(RLPAF), 在证明中写自然语言推理, 以及 MCTS 搜索. 再往后, R1 在数学和代码上只用规则奖励, 思路和这里用 Lean 判对错一脉相承. 形式证明的 SFT 数据选取可对照 4.2.2-SFT数据质量筛选与训练技巧, 这篇的打分过滤就是其中「模型打分筛数据」的一个具体实例.

4. 奖励、搜索与证明生成的关系

截断续写(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$ 全部来自下一节的内在奖励. 这里的「动作」包括虚拟节点代表的「就地扩展」, 所以一个节点被反复选中扩展, 统计也会累积在它的虚拟子节点上.

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

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

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

$\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 时.

截断点怎样决定可复用前缀： 生成结果交给 Lean 后, 系统定位第一条失败 tactic. 失败前所有 tactic 已被验证, 可以作为树中的合法路径; 失败行及其后续全部丢弃. 若一条复合 tactic 内部部分成功后失败, 对外仍通常表现为该命令失败, 复用粒度受语法命令边界限制. 粒度太粗会丢掉复合 tactic 内部进展, 太细会增加状态数与验证交互. V1.5 以 tactic 位置切分, 借 LeanDojo 获取前后状态, 是源码结构与搜索成本之间的折中. 宏、all_goals 和组合符可能让一行改变多个目标, 文本行数也不等于一步逻辑推理. 前缀复用需要保证环境确定. 同一文件头、Lean 版本、Mathlib commit 和 options 下, 重放前缀应得到相同状态. 若 tactic 依赖超时、外部 oracle 或不同库版本, 缓存状态可能失效. 论文固定 Lean 4.9.0 与导入, 使 benchmark 内重放可控.

截断也能把超长失败证明压回最近合法点. 但 prompt 会包含前缀代码、注释和状态, 多次续写后仍可能接近上下文上限. 搜索器没有压缩形式证明语义的独立模块, 长文件需要更长上下文或结构化状态存储.

4.2. virtual node 为何允许反复扩展同一状态

开放文本动作空间不能预先枚举. 第一次从状态 $s$ 采样得到 nlinarith, 没有理由认为其他可行 tactic 已经穷尽. virtual node 相当于保留一个永远存在的「再问模型一次」动作, 被选择时生成新的候选. 真实子节点代表已发现状态转移, virtual child 代表尚未采样的潜在转移. UCB 统计决定是沿已有分支深入, 还是从某个旧状态再开新分支. 如果没有 virtual child, 一个节点首次展开后就封闭, 语言模型的随机性无法被持续利用. virtual loss 用于并行. 某线程选择节点后先临时降低其吸引力, 其他线程倾向别处, 等验证返回再用真实奖励覆盖. 它提高树的并行多样性, 也可能让本应集中探索的强分支暂时被冷落. 论文给出 32 线程设置, 没有并发数消融.

状态合并与路径依赖的张力： 从 Lean 看, 两条代码前缀到达同一 proof state 后, 未来合法 tactic 集大体相同. 从语言模型看, prompt 中前缀文字、CoT 和命名不同, 后续分布可能不同. RMaxTS 将等价代码存到同一节点, 续写时随机选择一条前缀, 在状态合并与文本多样性之间折中. 如果只保留一条最短前缀, prompt 更省 token, 可能丢掉有用的自然语言计划. 如果所有前缀都建独立节点, 树会被同状态重复占满, 新奇奖励失真. 多前缀单状态让 Lean 语义去重, 同时保留若干模型上下文. 这种设计也说明搜索不是纯 MDP. 理论状态 $s$ 若只取 Lean goal, policy 还依赖达到它的文本历史 $h$. 更完整状态应是 $(s,h)$, 合并时忽略了部分 $h$. 实验显示这种近似有效, 没有证明对长证明同样成立.

DUCB 的有效记忆长度： $\gamma=0.99$ 时, 距当前 $k$ 轮的权重为 $0.99^k$. 约 69 轮后降到一半, 229 轮后约 0.1. 有效样本数上限 100, 意味着选择器主要反映最近数百次扩展, 不让早期容易获得的新奇永久支配. 探索项中的折扣计数也有上界, 已访问很多次的分支仍保留非零探索奖励. 对非平稳新奇信号合理, 对稳定外在成功概率则可能过度探索. 任务一旦找到证明立即停止, 没有长期利用已知成功分支的问题. $\gamma$ 控制适应速度. 更小值更快忘记, 对噪声更敏感; 更大值更稳定, 节点挖空后转移慢. 论文固定 0.99, 没有 sensitivity study. 完整 RMaxTS 的优势可能依赖 benchmark 证明树尺度与这个有效窗口匹配.

新状态奖励可能出现哪些反例： 第一类是循环改写. tactic 在两个等价表达式间来回转换, 若状态正规化不足, 每次都可能被当新节点. 第二类是无关 have, 不推进主目标却扩充上下文. 第三类是目标爆炸, 一个 tactic 把一个目标拆成很多更难子目标, 仍因新状态得分. Lean 会阻止非法动作, 不能判断数学进展. 计数新奇类似探索未知房间, 房间多不代表接近出口. miniF2F 中高层自动化常能从一个有用中间状态直接收尾, 新奇是尚可接受的代理; 大型库证明可能需要长时间沿一条看似不新奇的路径积累引理. 引入 learned critic 可估计从状态完成的概率, 但训练标签昂贵且可能偏差. 可用搜索回报训练 value, 又形成自举误差. V1.5 选择零 critic 的 RMax, 保持验证信号纯净, 用更大搜索宽度换方向性.

为什么小预算看不到树搜索收益： 建树初期要重复发现合法前缀、抽取状态并估计分支新奇. 独立整证 sample 则从第一份预算起就有机会直接命中. 若题目短、模型单遍成功概率不低, 初期树管理成本难以回收. 只有当多次 sample 反复共享某些正确前缀, 且失败点之后存在多种续写, 前缀复用才优于重开. 大预算提高遇到这类题的机会. 表中 3200 次差不到一题, 4×6400 与 16×6400 才逐渐拉开, 与这个门槛一致. 这也限制个人复现. 单题数千 sample 时, 使用 RL checkpoint 做 independent sampling更简单; 若 CPU 验证远慢于 GPU 生成, 树搜索的反复前缀验证还会受瓶颈. 论文的异步数千核环境把这些延迟隐藏在并行中.

异步执行会怎样改变树： 32 个线程从同一棵树并发选择节点, GPU 批量生成, CPU Lean worker 的完成顺序取决于证明长度与 tactic 耗时. 快速失败可能先回传, 慢而正确的证明稍后到达. 树在等待期间已经被其他结果更新, 选择策略是异步近似. virtual loss 防止重复选择, 其数值会临时影响其他线程. 并发越高, 临时统计越多, 树与串行 UCB 的路径差异越大. 高并发换吞吐, 同时增加调度随机性. 论文报告系统设置, 没有串行/并行质量对照. 批量生成要求把来自不同 theorem 和状态的 prompt 拼 batch. 长度差导致 padding, CoT prompt 更长. GPU 利用率与生成延迟受 batch composition 影响. 数千 CPU 核负责验证, 整体吞吐取决于 GPU proposal 与 Lean 消费是否平衡. 若 Lean 成为瓶颈, 新候选在队列等待, 搜索统计滞后; 若 GPU 慢, CPU 闲置. 论文没有队列、吞吐和利用率, 所以算法预算无法直接转换为墙钟.

4.3. 搜索树中的证明多样性

同一 theorem 可以有代数、几何或自动化等不同 proof. 独立采样通过随机 token 获得多样性, 树搜索还通过状态选择分散分支. 新奇奖励倾向覆盖更多 state, 理论上能提高结构多样性. 状态多样不等于 proof 多样. 两个不同中间状态可能最终都调用同一自动化 tactic, 两段不同代码也可能 kernel term 接近. 论文只统计是否至少一证, 没报告 unique proof、state coverage 或 tactic entropy. 多样性对 pass@k 有直接价值. 如果 sample 完全重复, 增加 $k$ 没有收益; 如果不同 proof 失败独立, 覆盖更快上涨. RL 的 KL 与 CoT/non-CoT 混合可能保持多样性, RMaxTS 新奇则显式扩展状态. 大预算曲线继续上涨说明系统没有完全塌缩.

搜索终止与证明发布： 任何 rollout 得到 Lean 通过后, 当前 theorem 搜索可以立即结束. 最终 proof 是从根到成功节点的某条前缀加新生成后缀. 搜索中的其他分支和错误注释不会进入发布证明. 若多个线程同时成功, 可以选择先返回者、最短 proof 或验证成本更低者. 论文以 solved/unsolved 计分, 没说明多个成功 proof 的选择标准. 这不影响 pass, 会影响可读性与复现输出. 验证通过还应在干净进程重放, 防止 REPL 状态泄漏. 沙箱进程与固定导入有助于隔离. 官方系统以 Lean 为最终裁判, 具体发布 pipeline 在论文中不详细.

没有 critic 时的理论直觉： 标准 UCT 用平均终局回报估计动作价值. 在稀疏证明任务中, 找到第一条 proof 前所有外在回报为零, exploitation 无信息. RMaxTS 把「发现未见状态」当乐观回报, 类似 RMax 对未知状态赋最大值, 使搜索优先完成状态空间覆盖. 一旦某区域被反复扩展, 新状态率下降, DUCB 利用项随近期零奖励降低, 搜索便转向别处. 这个分数表达未知性耗尽前的乐观程度, 不估计当前状态离完成证明还有多远. 对有限浅树有合理效果. 开放动作与无限状态意味着无法真正覆盖完. 状态字符串细微变化也会持续产生新奇, 所以方法依赖模型 proposal 集中在有意义 tactic 和状态合并去重. 理论 RMax 的有限 MDP 保证不能直接搬到这里.

奖励、搜索与证明生成的关系： RLPAF 优化的是生成分布： 对定理 $x$, 模型生成证明 $y$, Lean 奖励 $r(y)\in{0,1}$. GRPO 每组采 32 条, 用组内均值与标准差构造相对优势. 忽略裁剪细节, 优势可写成:

正确证明的 token 概率被提高, 错误证明被降低, KL 项约束模型不要离 SFT 参考过远. 奖励在序列末端给出, 每个 token 共享整条证明优势. 算法不知道哪一条 tactic 起了决定作用, 信用通过策略梯度粗粒度传播. RL 改变的是采样分布, 不直接修改 Lean 搜索器. 若正确证明已经在 SFT 分布尾部, RL 可把它移到更高概率区域; 若定理所需思路从未出现在模型支持集, 0/1 奖励难以创造新动作. 中等难度筛选保证每组有机会出现正负样本, 也让训练集中在现有能力边界附近. 4.5k 提示很少, 每题 32 sample 仍能产生大量在线序列. 题目来自 SFT 数据并按成功率筛选, 分布偏向模型偶尔可解的竞赛式 Lean 题. ProofNet 回退说明这种局部优化没有自动迁移到所有本科数学领域.

树搜索优化的是测试时资源分配： 给定固定 checkpoint, RMaxTS 决定下一次 sample 从哪个已验证状态开始. 它不更新模型参数, 而是在一题内部把更多预算分给能产生新状态的分支. RL 与 MCTS 的作用层不同: RL 跨题改变策略先验, MCTS 在单题中利用 Lean 反馈重排探索. 可以把模型看成 proposal policy $\pi_\theta(a\mid s)$, 搜索器根据统计选择状态 $s$, 再让模型生成动作或整段 rollout. 若模型 proposal 很差, 搜索反复得到非法 tactic; 若模型已经很强, 单遍大量采样也能覆盖正确证明, 搜索边际收益小. 表中低预算几乎无增益, 正是后一种与启动成本共同作用的结果. 截断续写使一次 rollout 的有效前缀能进入树. 普通 best-of-$k$ 每个 sample 独立, 失败证明中的正确前缀全部丢弃. 树搜索复用前缀, 但也要支付状态抽取、去重和反复验证. 收益只有在正确证明需要跨多个尝试组合前缀时超过开销.