02 · DeepSeekMath-V2: 用元验证训练可自检的自然语言证明模型

论文 DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning 于 2025 年 11 月公开, 模型基于 DeepSeek-V3.2-Exp-Base, 代码与模型见 deepseek-ai/DeepSeek-Math-V2. 工作对象从有标准数值答案的竞赛题转向自然语言定理证明. 核心变化是训练一个能够指出证明缺陷的 verifier, 再让 generator 同时生成证明与自我分析, 最终用扩大验证计算得到的新标签继续训练 verifier.

1. 最终答案奖励为什么不足以训练证明

最终答案奖励只检查结果, 不检查证明过程是否成立.

1.1. 答案正确与推导正确是两个事件

AIME 与 HMMT 一类定量题可以把模型答案同 ground-truth 比较, 奖励几乎不需要理解推导过程. 模型可能通过错误抵消, 猜测或不成立的中间步骤得到正确数值. 最终答案奖励只观察末端结果, 因而会把这些轨迹与严格证明同样标成成功. 当任务要求证明命题而没有数值答案时, 该奖励甚至没有可比较对象.

自然语言证明要求每个关键结论都有前提支持, 边界条件完整, 量词与分类讨论没有遗漏. 形式证明可以交给 Lean 或 Isabelle 内核检查, 自然语言证明缺少同等可靠的编译器. DeepSeekMath-V2 因此训练 LLM verifier 来近似数学专家评阅: 输入问题 $X$ 与候选证明 $Y$, 定位具体缺陷并给出等级, 而非重新生成一份参考解答.

1.2. 三档分数把证明质量变成训练信号

验证 rubric 使用三个分数: 1 表示完整严谨, 所有逻辑步骤均有说明; 0.5 表示总体思路成立, 只有小错误或细节遗漏; 0 表示存在致命逻辑错误或关键缺口. verifier $\pi_\phi(\cdot|X,Y,I_v)$ 先输出发现的问题, 再给出分数. 分档降低专家标注与模型学习的难度, 同时保留完全错误, 可修补与完整证明之间的差异.

冷启动问题集从 AoPS 竞赛集合抓取, 优先数学奥林匹克, 国家队选拔与 2010 年以后明确要求证明的题目, 共 17,503 道, 记为 $D_p$. DeepSeek-V3.2-Exp-Thinking 的变体生成候选证明并多轮改进, 数学专家再按 rubric 标成 0, 0.5 或 1, 形成 $D_v={(X_i,Y_i,s_i)}$. 候选模型尚未专门优化定理证明, 会产生简短且易错的样本, 正好为 verifier 提供缺陷类型.

1.3. 只学分数会产生虚假的缺陷分析

初始 verifier 的奖励包含格式项与分数项. 格式项检查输出是否含规定的分析与 boxed 分数. 分数奖励为 $R_{score}(s'_i,s_i)=1-|s'_i-s_i|$, 预测越接近专家分数越高. 两项相乘后, 格式错误直接使奖励失效, 分数差异则连续影响奖励.

这套目标只监督最终分数, 没有直接判断模型指出的问题是否存在. 对一个专家标为 0 的证明, verifier 即使虚构完全无关的缺陷, 只要也给 0 分就能获得满分. 评分准确率与分析忠实度因此可以分离. 一个高分辨率 verifier 若频繁编造缺陷, 不能作为 generator 的可靠奖励模型, 也不能用于开放问题的自检.

2. 元验证怎样约束 verifier 的忠实度

2.1. meta-verifier 检查的是评语而非证明

元验证把 verifier 的输出 $V$ 当成待检查对象. 数学专家依据 $I_{mv}$ 评价 $V$ 是否准确指出了 $Y$ 中真实存在的问题, 这些问题是否足以支持最终分数, 并给出 $ms_i\in{0,0.5,1}$. 数据集写为 $D_{mv}={(X_i,Y_i,V_i,ms_i)}$. meta-verifier $\pi_\eta$ 接收问题, 证明, 验证分析与 rubric, 输出对分析本身的缺陷总结和质量分.

meta-verifier 不负责重新写一份完整证明. 它需要核实一个已经提出的具体批评, 搜索空间通常小于从头发现所有证明错误. 这也是后续自动标注能够扩大计算的基础: verifier 负责提出候选缺陷, meta-verifier 负责筛除幻觉和不成立的批评.

2.2. 三项乘积让虚构问题失去奖励

增强后的 verifier 奖励为 $R_V=R_{format}\cdot R_{score}\cdot R_{meta}$. 格式与总分正确还不够, 元验证质量低也会压低整体奖励. 训练同时使用 $D_v$ 与 $D_{mv}$, 得到的同一个模型能够执行证明验证和元验证两类任务.

在 $D_v$ 验证集上, meta-verifier 给证明分析的平均质量分从 0.85 提升到 0.96, 同时证明分数预测准确度保持不变. 这个结果隔离了元验证的主要收益: 它没有靠牺牲分数判断换取更好评语, 而是减少评语中不准确或缺乏依据的问题. 0.96 仍是由训练出的 meta-verifier 评价, 不是形式系统给出的绝对正确率.

2.3. 自动标注靠扩大验证样本而非一次判断

generator 变强后, 新证明的错误更隐蔽, 单次 verifier 可能漏检. 自动标注流程先为每份证明采样 $n$ 份独立验证分析. 对给出 0 或 0.5 的分析, 再采样 $m$ 份元验证, 多数元验证确认后才把该问题视为有效. 然后查看给出最低分的分析: 若至少有 $k$ 份最低分分析通过元验证, 证明得到该最低分; 若所有尝试都没有发现合法问题, 证明标为 1; 其余不确定样本丢弃或交给专家.

最低分规则偏向发现错误, 多数元验证则限制误报. 随 $n$ 增加, 至少一次找到真实缺陷的概率上升; 随 $m$ 增加, 单条批评被错误接受的概率下降. $n,m,k$ 的具体取值没有在正文公开, 因而方法可以复述, 完整自动标注成本无法复算. 最终两轮训练完全以该管线替代人工标注, 质量抽查显示自动标签与专家判断较一致.

3. generator 如何把自检纳入强化学习

3.1. verifier 先作为生成证明的奖励模型

proof generator $\pi_\theta(\cdot|X)$ 从 $D_p$ 采题并生成 $Y$, verifier 给出证明分数 $R_Y$. 初始目标就是最大化该分数. 与答案匹配奖励相比, verifier 可以处理没有数值答案的题, 也能区分致命错误和局部缺口. 代价是奖励本身来自模型, verifier 的漏检与偏差可能被 generator 利用.

训练采用 GRPO. 每轮先优化验证能力, 再从 verifier checkpoint 初始化 generator 并优化证明生成. 从第二轮起, verifier 由上一轮通过 rejection fine-tuning 合并验证和生成能力的 checkpoint 初始化. 生成得到更困难的新证明, 新证明经扩大验证自动标注后又进入 verifier 训练, 两个能力沿迭代共同提高.

3.2. 自我分析需要单独奖励忠实度

只要求 generator 在一次输出里生成证明并自评时, 模型常会声称自己的证明正确, 即使独立 verifier 很容易发现缺陷. 能依据外部反馈修改证明, 不代表能对自己的输出执行同样严格的检查. 论文因此要求 generator 先生成证明 $Y$, 再按 verifier rubric 输出自我分析 $Z$ 与自评分 $s'$.

外部 verifier 分别评价两部分. 证明得到 $R_Y=s$, 自我分析得到 $R_Z=R_{score}(s',s)\cdot R_{meta}(Z)$. 总奖励为:

$R_{format}$ 要求证明和自评格式同时成立. $R_{score}$ 奖励自评分与外部 verifier 分数一致, $R_{meta}$ 检查自评指出的问题是否真实. generator 若诚实承认错误可以获得自评奖励, 但最高奖励仍来自写出正确证明并准确判断其严谨性. 0.76 与 0.24 让证明质量占主导, 防止模型只写出优秀批评却不解决题目.

3.3. 顺序改进把超出单次窗口的修正拆开

对 IMO, CMO 等难题, 单次 128K token 内可能无法同时生成完整证明, 发现全部问题并修正. 顺序改进先输出证明与自评, 再把上一轮结果放进 refinement prompt, 要求下一轮解决已发现的问题. 当模型自评为满分或达到最大轮数时停止.

IMO Shortlist 2024 实验为每题启动 32 条独立线程. 每份最终证明由 32 份 verifier 分析多数投票评价. Pass@1 是各线程最终证明的平均分, Best@32 按线程自评分选出每题最佳证明. 最大迭代从 1 增至 8 时, Pass@1 由图中的约 0.15 上升到约 0.29, Best@32 在多处约为 0.40. 自选最佳显著高于线程平均, 支持 generator 能够区分自己的较好与较差证明. 图中数值由绘图读取, 不应当作带置信区间的精确估计.

4. 高计算搜索的成绩与边界

这里的高分来自搜索预算与验证预算共同扩大, 不是 one-shot 能力.

4.1. 64 路生成和验证组成候选池搜索

高计算设置为每题生成 64 份初始证明, 每份配 64 份验证分析. 每轮按平均验证分选出 64 份最高分证明, 再为每份证明随机选择 8 份分析, 优先选择指出问题的 0 分或 0.5 分分析. 每个证明与分析对生成一份改进证明并更新候选池. 搜索最多进行 16 轮, 或某份证明通过全部 64 次验证后提前停止.

生成和验证都由最终 proof generator 执行, 没有使用不同的闭源裁判. 多样化生成负责探索证明路线, 多次验证负责暴露缺陷, refinement 负责局部修正. 计算量远高于一次回答, 并且候选选择仍依赖同族模型的评分偏好. 专家最终复核最高分证明, 因而竞赛成绩不是只由模型自评分宣布.

4.2. IMO, CMO 与 Putnam 成绩使用专家评分

IMO 2025 中模型完全解出 5 道题, 得分比例 83.3%, 达到金牌档. CMO 2024 完全解出 4 道, 另一道获部分分, 得分比例 73.8%, 同样达到金牌档. Putnam 2024 完全解出 11 道, 剩余一道有小错误, 最终 118/120; 当年人类最高分为 90. 这些数字来自高计算候选池和专家评阅, 不是一次采样的 Pass@1.

IMO-ProofBench 分 basic 与 advanced 各 30 题. Heavy 设置在 basic 上为 99.0%, advanced 为 59.0%. basic 高于图中 DeepThink IMO Gold 的 89.0%, advanced 仍低于该系统的 65.7%. hardest IMO-level 问题仍然困难. 论文也报告未完全解出的题中, generator 通常能够指出自己证明的真实问题, 表明自检能力可能早于完整求解能力成熟.

4.3. 自验证仍然不是形式保证

所有 verifier, meta-verifier 与 generator 都来自相近模型谱系. 扩大独立采样能降低偶然漏检, 不能排除共享盲点. 一份错误证明若系统性欺骗 verifier 与 meta-verifier, 可能通过多次检查. 论文通过专家终审竞赛证明缓解这一风险, 对开放数学问题则仍缺少 ground-truth.

形式证明助手要求机器可检查的语法, 一旦内核接受即可提供远强于 LLM 评分的保证. 自然语言证明更灵活, 能表达探索思路并利用大规模语料, 但 verifier 分数只是经验性可信度. DeepSeekMath-V2 的贡献是让自然语言验证成为可训练, 可扩展的反馈通道, 不是用概率验证取代形式内核.

训练闭环还有分布风险. 自动标签来自当前 verifier 能发现的错误, generator 会逐渐避开这些已知模式, 未被 verifier 表达的缺陷可能保留下来. 继续改进需要外部专家抽查, 新型对抗证明, 形式工具反馈或不同模型交叉验证. 论文最终两轮无需人工逐条标注, 不表示后续系统可以永久取消人类和形式验证.

自动标注规则本身还包含选择偏差. 只有 verifier 主动指出的问题才会进入 meta-verification, verifier 从未想到的缺陷没有候选分析可供复核. 当多个分析都给 1 分时, 管线倾向把证明标成正确; 该结论依赖多次采样覆盖缺陷空间. $n$, $m$, $k$ 越大, 计算越高, 但共享盲点不会仅靠重复采样消失.

0, 0.5, 1 三档分数也会压缩错误严重程度. 两份都得 0.5 的证明可能分别缺一个简单边界条件与一个需要新引理的关键步骤, 修改成本差异很大. rubric 的优势是标签稳定且便于 RL, 代价是奖励分辨率有限. generator 后续看到具体问题分析, 而不只看到分数, 才能获得更有方向的改进信息.

Figure 2 的 Best@32 由 generator 的自评分挑选, 再由同族 final verifier 评价. 自评与外部评分相关支持自验证能力, 但两者共享训练方法和 rubric, 相关性可能部分来自共同偏好. 若要衡量跨裁判泛化, 还需要独立专家或不同模型 verifier 对全部候选盲评, 论文只对最终高计算竞赛证明安排专家终审.

顺序改进增加最大轮数后, Pass@1 并非每一步都单调增加. Figure 2 中曲线存在局部波动, 说明 refinement 可能修好一个问题又引入另一个问题. 停止条件依赖模型自评为满分, 假阳性会过早停止, 假阴性则浪费后续计算. 多线程与 Best@32 用并行多样性缓解单条路径退化, 没有消除该风险.

高计算搜索的规模远高于表面上的 64 个候选. 初始阶段每份证明配 64 份分析, 已产生 4096 次验证. 每轮选出的 64 份证明各配 8 份分析生成新证明, 最多再运行 16 轮. 实际请求数还取决于提前停止和候选池更新. 论文没有报告总 token, GPU 时和每题成本, 所以竞赛分数不能直接代表日常推理预算下的能力.

全部 64 次验证通过被当作高置信正确的停止信号. 如果每次验证错误相互独立, 重复通过会显著降低错误概率; 同一模型的采样并不满足严格独立假设. 提示格式, 训练数据和推理模式造成的系统偏差会让多次结果相关. 因此 64 次通过是经验性置信规则, 不是统计校准后的正确性证明.

Putnam 118/120 与人类最高分 90 的比较还要保留计算条件. 人类参赛者受 6 小时赛制限制, 模型使用大规模并行生成, 验证与最多 16 轮修改. 该结果证明搜索系统能够产出高质量最终证明, 不表示单个模型在同等时间和工具约束下超过最强人类. 论文也明确把这组结果归于 scaled TestingTime compute.

内部 CNML 集合由团队自行构造, 题目数量为 91, 各类别规模不等. Figure 1 的平均证明分来自 final verifier, 不是全部专家评分. 它适合比较相同裁判下的三个模型, 不能独立校准 verifier 是否对某个模型风格更宽松. IMO, CMO, Putnam 和 ProofBench 的外部题目及专家检查提供了更强补充证据.

自然语言 verifier 与形式系统可以组成分层管线. verifier 先在庞大的非形式证明空间中寻找路线, 提出缺陷并筛选候选; proof assistant 再检查可以形式化的最终论证. 前者提供搜索效率与可读思路, 后者提供内核级保证. DeepSeekMath-V2 没有把最终证明自动翻译并编译到 Lean, 所以论文成绩仍属于自然语言证明评价.

元验证还可以用于人机协作. verifier 给出具体缺陷, meta-verifier 先筛除不成立的批评, 专家再集中查看通过筛选的少量争议点. 与要求专家从头阅读每份长证明相比, 这种流程可能降低标注成本. 论文最终两轮完全自动化说明模型已能承担大量筛选工作, 但没有公开专家抽查样本数和一致率, 无法量化节省幅度.

generator 明确知道奖励规则可能带来 reward hacking. 元验证通过检查缺陷真实性限制简单的分数欺骗, 格式奖励则只约束输出结构. 更隐蔽的策略仍可能生成迎合 verifier 表达偏好的证明, 而不是最清楚或最简洁的数学论证. 引入独立裁判, 隐藏 rubric 变体和形式检查有助于测试这种过拟合.

模型对未解决证明能够指出真实问题是一项独立能力. 在开放问题中, 立即找到完整解答通常困难, 可靠识别当前路线的缺口仍能帮助研究者避免无效方向. 但如果 verifier 只指出局部表达缺陷而遗漏核心反例, 自检会制造虚假信心. 使用时应保留具体问题与证据, 不只展示最终 0, 0.5, 1 分数.

从训练设计看, verifier, meta-verifier 与 generator 的职责形成三层约束. verifier 判断证明, meta-verifier 判断 verifier 的批评, generator 同时优化证明和自评. 自动标注再把多次判断聚合成新标签. 每增加一层都会提高计算量, 也把单次评分错误转化为可以交叉检查的对象. 方法的价值来自这种显式分工, 不是任何单个评分模型绝对可靠.

这条路线能否推进到研究级数学, 取决于难题分布外泛化, 长证明一致性, 外部知识使用与可靠校准. 竞赛题有明确题面, 通常预期存在短期可检查的解答; 研究问题可能缺少已知结论, 定义持续变化, 证明依赖大量文献. DeepSeekMath-V2 提供了可扩展的验证训练框架, 当前结果尚不能证明模型能够独立解决开放数学问题.

训练资料主要来自竞赛证明题, 这会塑造 verifier 对严谨性的判断方式. 奥赛证明强调有限篇幅内的构造, 分类与不等式推导, 研究论文还包含引用前置定理, 数值实验, 计算机辅助证明和领域约定. rubric 能否跨到这些文体需要新的专家数据. 直接把竞赛 verifier 用作研究结论裁判, 可能把省略的公认背景误判为缺陷, 或漏掉专业领域中的隐含条件.

三档评分在 refinement 中承担两种作用. 分数用于候选排序和停止判断, 具体分析用于告诉 generator 修改什么. 如果只有分数, generator 只能重新采样; 如果分析准确, 修改可以集中在缺失引理, 未覆盖情形或错误推导. meta-verification 提高的正是第二类信号质量, 所以 0.85 到 0.96 的变化即使不改变分数准确率, 仍可能明显改善后续生成.

$\alpha=0.76$ 与 $\beta=0.24$ 体现证明质量优先于自评质量. 若 $\beta$ 太高, 模型可能投入大量 token 描述自己的错误, 却不愿承担修复证明的风险; 若 $\beta$ 太低, 诚实发现错误几乎得不到回报, 模型又会恢复到一律宣称正确. 论文只公开最终权重, 没有给权重消融, 因而可以解释激励方向, 不能断言该比例是普遍最优.

rejection fine-tuning 用上一轮模型生成并筛选的样本合并验证与生成能力, 再初始化下一轮 verifier. 这使一个 checkpoint 同时理解证明内容和评审格式, 降低两类任务之间的迁移成本. 代价是模型角色进一步同源, generator 与 verifier 可能共享错误模式. 自动化训练循环需要持续加入外部题型和独立评价, 才能避免能力在当前 rubric 内部循环强化.

论文的结果应按三档计算预算理解. one-shot 衡量一次生成; sequential refinement 允许最多 8 次串行修改并运行 32 条线程; Heavy 搜索使用 64 份证明, 大量验证和最多 16 轮候选更新. 三档成绩回答不同问题. 只有明确预算, 才能比较模型基础能力, 自我改进效率和大规模搜索上限, 也才能评估方法是否适合交互式使用.

5. 自验证闭环中的概率、搜索与校准

三档标签对应的是证明可接受性, 不是命题真假. 证明问题包含命题 $X$ 与候选论证 $Y$. 命题可能为真, $Y$ 仍然错误;命题也可能在题目约定下成立,但 $Y$ 省略了关键情形. verifier 学习的条件分布是

其中 $V$ 是问题分析,$s$ 是对当前论证的质量分. 它没有独立预测命题的真值. 这一区分很重要:一个 verifier 给 0 分,表示这份证明未达到 rubric,不能单凭该分数推出命题为假. 三档标签将连续的证明质量压缩成序数. 0 与 0.5 的边界通常在于缺陷是否破坏主路线;0.5 与 1 的边界在于遗漏是否仍需实质数学工作. 标签间距写成数值以后,$R_{score}=1-|s'-s|$ 默认 0 到 0.5 与 0.5 到 1 的距离相同. 这是一种训练约定,并非证明修复成本真的线性.

假设专家标签为 1,模型预测 0.5,分数奖励为 0.5;预测 0 则为 0. 对专家标签 0.5,模型预测 0 或 1 都得到 0.5. 因而中间档在数值上对两侧对称,但真实错误可能不对称:把完整证明误判成 0 会浪费搜索,把致命错误误判成 1 会产生错误接受. 自动标注阶段的最低分聚合选择了更偏向后者风险的策略. 分数准确与缺陷忠实是两条轴. 把证明是否存在致命缺陷记为 $E$,verifier 是否指出一个真实缺陷记为 $F$,最终分数正确记为 $C$. $C=1$ 不推出 $F=1$. 对明显错误的证明,模型可以凭风格或长度猜到低分,再编造一个听起来合理的理由. 反过来,模型可能准确发现局部缺口,却把严重程度从 0.5 误判成 0. 初始分数奖励主要优化 $P(C=1)$. 元验证奖励把 $P(F=1\mid V)$ 纳入目标. 乘积形式

具有门控效果:分析不忠实会削弱分数正确带来的收益. 若改成加法,模型仍可能用高分数项补偿虚构分析;乘积更强调两项同时成立. 代价是任何一项接近零都会让整条样本梯度弱化,训练方差可能更大. $R_{meta}$ 仍由模型近似,不是数学真值. meta-verifier 读取具体批评后核查,搜索任务比从头审阅证明更窄,却可能与 verifier 共享盲点. 如果两者都误解某个定理条件,虚构批评仍可能获高分. 元验证降低的是经验误报,没有构成无限递归后终将正确的保证. 多次验证提高召回率的条件. 设一份错误证明含某个缺陷,单次 verifier 发现它的概率为 $p$. 若 $n$ 次采样在给定证明后条件独立,至少一次发现的概率为

当 $p=0.2,n=8$ 时,$P_{hit}\approx0.832$;增至 32 次后约为 0.999. 这解释了扩大验证计算的基本收益. 真实采样不独立,同一模型与同一 prompt 会让错误高度相关. 可以用有效相关系数理解:相关越高,新增样本提供的新缺陷视角越少,实际曲线低于独立公式. 多样化验证 prompt,温度或模型家族可降低相关性. 论文主要依靠同一模型独立采样,获得的是路线内部的搜索扩展. 它能覆盖模型偶尔会想到但一次没有想到的缺陷,难以覆盖模型表示中根本不存在的反例. 元验证多数票怎样压低误报. 对一条候选批评,设单个 meta-verifier 错误接受虚假问题的概率为 $q<1/2$. 采样 $m$ 次并用严格多数接受时,误接受概率为

在独立假设下,该概率随 $m$ 指数下降. 如果 $q=0.2,m=5$,至少 3 票错误接受的概率约为 0.058. 共享偏差同样会破坏独立性. 某个看似缺条件、实际可由题目约定推出的步骤可能让所有采样一致误判. 自动标签还要求至少 $k$ 份最低分分析通过元验证. $k$ 越大,错误证明被判低分需要更多一致证据,精度上升但召回下降; $k$ 越小,更容易捕获隐蔽缺陷,误报风险也增加. 论文没有公开 $n,m,k$,因此无法计算其标签接受率与单位样本成本. 最低分聚合是一种风险厌恶决策. 候选分析给出一组分数 $s_1,\ldots,s_n$. 取通过元验证的最低分,相当于关注存在一个有效致命反例. 证明的逻辑性质正适合这种聚合:只要一个关键步骤不成立,其他评审全部称赞也不能使证明正确.

但最低分对误报极敏感,所以必须先做元验证并要求 $k$ 份支持. 平均分不适合替代. 例如 31 个评审给 1,1 个评审准确指出致命反例给 0,平均 0.969 会掩盖错误;最低分能保留反例. 若那一个 0 来自幻觉,最低分又会错误否决. 整套管线围绕这一对精度—召回矛盾设计. 全部通过仍然只给经验置信度. 若错误证明单次漏检概率为 $u$,且验证独立,64 次全部漏检概率为 $u^{64}$. 即使 $u=0.8$,该值也约为 $6.3\times10^{-7}$. 这个数字看起来极小,前提却很强. 若存在一个共享盲点,相关错误可让条件漏检概率接近 1,重复 64 次也不会改善.

因此“64 次全部通过”更像压力测试:模型用许多推理轨迹尝试寻找问题,没有找到时提高信心. 它不能像 Lean 内核那样把证明还原到可信规则. 专家终审竞赛输出仍是必要环节,尤其当成绩用于高风险声明时. 自评奖励为什么不会鼓励一味认错. generator 奖励为

假设证明分 $R_Y=0$,但自评准确指出致命问题并给 0,则 $R_Z$ 可以接近 1,总奖励约 0.24. 如果证明完整且自评正确,$R_Y=R_Z=1$,总奖励为 1. 诚实认错比错误地自称满分更好,仍显著低于写出正确证明. 若只奖励自评分与外部评分一致,模型可以给正确低分却编造理由. $R_{meta}(Z)$ 要求自评中的批评真实. 若只奖励批评真实,模型可能指出无关小问题却错误判断整体质量. $R_{score}$ 与 $R_{meta}$ 的乘积让严重程度和依据共同进入自评质量.

这套激励并不保证自评是因果忠实的. generator 可能在生成证明时已隐式知道某一步脆弱,事后复述一个奖励偏好的分析;也可能从语言表面识别典型缺陷,未真正重算整条推导. 外部 verifier 判断输出是否有用,无法读取模型内部推理过程. 这里的“忠实”指批评与证明事实一致,不指完整揭示神经网络的内部因果链. 自评与证明共享上下文会产生承诺偏差. 生成证明以后,模型继续在同一上下文中自评. 前文由自身写出,会形成语言连贯性和路线承诺. 独立 verifier 从新的上下文读取证明,更容易采取对抗视角. 论文观察到模型能按外部反馈修正,却常在首次自评中偏向认为自己正确,正符合这种差异.

训练自评奖励相当于要求模型在同一上下文里切换角色:先提出论证,再主动搜索反例. 格式标记把两个阶段分开,但参数和隐藏历史仍共享. 更强的自评协议可以让模型先压缩证明中的关键依赖,逐条检查,或用独立上下文重新审阅. DeepSeekMath-V2 选择单次输出中的 Solution 与 Self Evaluation,优点是可直接用 RL 优化并控制总格式. Refinement 是带噪反馈下的策略更新. 令第 $t$ 轮证明为 $Y_t$,选中的问题分析为 $V_t$,refinement 模型生成

若 $V_t$ 指出真实缺陷且给出足够定位,$Y_{t+1}$ 的成功概率会上升;分析错误时,模型可能破坏原本正确的步骤. Figure 2 随轮数的局部波动正反映这种风险. 每轮 refinement 都是一次带噪随机编辑,不具备单调优化保证. 可以把证明质量写成潜在函数 $Q(Y)$. 理想改进满足 $\mathbb E[Q(Y_{t+1})\mid Y_t]>Q(Y_t)$. 论文的平均曲线支持在实验分布上存在正漂移,没有保证每条线程单调. 候选池保留旧证明可以避免新版本退化后永久丢失最好解,这也是 best-first 搜索比只沿一条链修改更稳的原因. 候选池搜索同时做探索与利用. 64 份初始证明提供路线多样性,验证分数选择较有希望的候选属于利用;为每份候选随机选择多个问题分析并生成改进属于局部探索. 候选池更新后继续循环,结构接近以 learned verifier 为价值函数的 best-first search.

若只保留最高分证明,verifier 的早期误判可能让真正有潜力但暂时不完整的路线被淘汰. 保留 64 个候选缓解这一问题. 仍可能发生模式坍缩:同一 generator 生成的证明共享主思路,表面有 64 条,有效路线远少于 64. 路线多样性需要按关键引理或结构聚类衡量,论文没有给该统计. 搜索预算的量级可以下界估算. 初始 64 份证明各配 64 份验证,仅第一轮筛选就有

次验证. 每轮若 64 份证明各用 8 份分析生成改进,就是 512 次 refinement. 最多 16 轮对应 8192 次改进生成,还未计新候选的再次验证,元验证以及长达 64K 或 128K 的最大输出. 提前停止会降低实际成本,该下界已表明 Heavy 成绩属于大规模推理系统. 官方推理代码公开的默认参数与论文描述并不完全等同于所有评测设置:代码中可见并行生成,每证明验证次数,最大生成长度和是否跳过元验证等开关. 复现实验应以具体配置和输入文件为准,不能把脚本默认值当成论文所有表格的唯一参数. 计算应该优先分给生成还是验证.

设总预算 $B=G+V$,其中 $G$ 用于生成候选,$V$ 用于验证. 候选太少时,verifier 再准确也只能从有限路线中挑选;验证太少时,大量候选无法可靠排序. 最优分配取决于 generator 命中正确路线的概率和 verifier 区分好坏的能力. 一个简化模型中,单候选正确概率为 $p_g$,生成 $g$ 份至少一份正确的概率为 $1-(1-p_g)^g$. verifier 对正确与错误候选的排序准确率随验证样本 $v$ 增长. 当 $p_g$ 很低,先扩生成更有效;当候选中已有好证明但错误证明评分噪声大,扩验证更有效. DeepSeekMath-V2 同时把两侧扩大,没有报告固定总预算下的分配消融. GRPO 奖励面对 verifier 偏差.

对同一道题采样一组证明,GRPO 使用组内相对优势更新 generator. 设奖励模型为 $r_\phi(Y)$,generator 会增加高于组均值的证明概率. 如果 verifier 偏好长证明,特定措辞或常见模板,这些特征即使与严谨性无关也可能获得正优势. 元验证减少虚构批评,却不自动消除风格偏差. 例如简短证明省略公认引理,verifier 可能比数学专家更严格;冗长证明逐句解释,更容易得到高分但也增加隐藏错误机会. 应将长度,风格与最终专家分数分层比较,论文没有公布这类奖励模型校准曲线.

训练 generator 后,输出分布向 verifier 高分区域移动,形成典型分布偏移. 原 verifier 在旧 generator 样本上准确,面对专门优化的新证明可能失效. 论文通过新证明自动标注并迭代训练 verifier,正是在修复这条生成—验证差距. 只训练一次固定 reward model,随后无限优化 generator,更容易产生 reward hacking. 自动标注是一种主动学习循环. 新 generator 产生更难验证的证明,这些样本集中在当前决策边界附近:表面完整,缺陷隐蔽,多次验证有分歧. 扩大验证与元验证给出标签后,它们成为下一轮 verifier 的高价值训练数据. 这比继续从弱模型收集显然错误证明更能提高边界分辨率.

自动管线把不确定样本丢弃或交给专家,会改变训练分布. 只保留高置信标签可降低噪声,也可能移除最难且最有价值的证明. 若困难样本长期被丢弃,verifier 在灰区能力不会提升. 合理系统应记录丢弃率,争议类型与专家回流,论文没有公开完整统计. Rejection fine-tuning 合并两种角色. 每轮结束后,筛选高质量生成与验证轨迹做 fine-tuning,再以该 checkpoint 初始化下一轮 verifier. 证明生成让模型掌握数学构造,验证训练让模型掌握反例与严谨性. 两种能力共享底座,可能互相迁移:会证明有助于判断一步是否可补,会验证有助于生成时避免缺口.