DeepSeekMath-V2自我验证：搞数据的风吹到了奖励模型

在开放性问题上，仅靠生成答案很容易出错。如何让模型不仅能写出证明，还能识别自身错误，从而形成闭环优化？答案是——自我验证。来看一下 DeepSeek 最新的论文：DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning[1]，看自我验证如何让 LLM 生成与评估协同来提升数学定理证明能力。

TL; DR

  • 训练验证器：验证器不仅打分，还识别证明中的问题。
  • 引入元验证：通过二次评分机制防止验证器虚构问题，使验证分析更可靠。
  • 训练生成器：生成器在生成证明后进行自我分析，并根据验证器和元验证器的反馈优化输出。
  • 验证生成协同：生成器与验证器形成闭环，生成新的证明挑战验证器能力，同时扩大自动标注数据，提高整体系统可靠性。

核心启示是：奖励模型不仅要给分数，更要建模评估分析过程，让生成与验证形成协同闭环，显著提升开放性问题的推理能力。

背景

Self-verification is particularly important for scaling testtime compute, especially for open problems without known solutions.

自我验证在扩展推理阶段（测试时）计算量时尤为重要，特别是在那些没有已知解的开放性问题上。这其实说白了就是怎么奖励的问题。出发点也很直观，RLVR 的两个问题：

  • 不可靠，模型可能通过有缺陷的逻辑或侥幸的错误得到正确答案。
  • 不适用于定理证明类任务，因为这些问题可能并不需要给出数值形式的最终答案，而是以严谨的推导过程为主要目标。当然，对于其他开放问题也不适用。

所以，自然导向“生成验证”。方法基于下面几个观察：

  • 即使没有参考解，人类也能识别证明中的问题，这在处理开放性问题时是一项关键能力。
  • 当经过大规模的验证仍无法发现问题时，一个证明更可能是有效的。
  • 识别有效问题所需的努力可以作为证明质量的代理指标，并可被用于优化证明生成过程。

作者相信 LLM 可以被训练识别证明问题，而无需参考解决方案。这样的验证器需要下面的流程：

  • 利用验证反馈来优化证明生成。
  • 扩大验证计算规模，以自动标注那些难以验证的新证明，从而生成用于提升验证器本身的训练数据。
  • 使用增强后的验证器进一步优化证明生成。

方法

证明验证

训练一个验证器来识别问题并对证明进行评分

给定证明评估准则 Iv、问题 X 和证明 Y，验证器 πφ(·|X, Y , Iv) 被设计为生成对证明的分析：

  • 首先总结所识别的问题（如果有的话）。
  • 然后根据三个等级为证明打分：1=完美证明，0.5=有小瑕疵，0=错误。

RL 训练数据 Dv = {(Xi Yi si)}：

  • 爬取 17,503 道竞赛证明题 Dp。
  • 使用 DeepSeek-V3.2-Exp-Thinking 生成候选证明，由于模型并未针对定理证明进行优化，且容易生成简洁但易出错的回答，于是通过提示让它进行多轮迭代式的证明改写，提升证明的全面性与严谨性。
  • 从不同类型的题目中（如代数、数论）随机抽取证明，并由数学专家根据评分标准对每份证明打分。

RL 训练目标：

  • Base：在数学和代码数据上 SFT 过的 DeepSeek-V3.2-Exp-SFT。
  • Score：格式+得分。打分=1-|s-s'|，s 是标注的分数，s’ 是预测的分数。

这一步得到一个验证器，可以识别问题，并给出最终得分。

引入元验证审查证明分析

前面得到的验证器使预测的证明评分与专家标注保持一致，但对所识别的问题本身并没有直接监督。这就可能带来一个关键漏洞：在训练过程中评估有缺陷的证明（即 si < 1）时，验证器可以通过直接预测正确分数，同时虚构不存在的问题来获得满分奖励，削弱其可靠性。

于是引入元验证：一种二次评估过程，用于判断验证器识别的问题是否真实存在，以及这些问题是否根据评分标准 Iv 合理地支持预测的证明分数。

使用 RL 训练元验证器，过程如下：

  • 得到上一步的初步验证器。
  • 数学专家根据准则 Imv 对验证器的响应质量进行评分，得到数据集 Dmv = {(Xi, Yi, Vi, msi)}，Vi 是对证明 Yi 的分析，msi ∈ {0, 0.5, 1} 是专家标注的质量评分。
  • 训练了一元验证器 πη(· | X, Y, V, Imv) 来分析验证器的证明分析 V，它首先生成对分析中发现问题的总结，然后给出一个质量评分，用以衡量验证器分析的准确性和合理性。其实就是人工再对分析继续打分。
  • 奖励同前面的验证器：格式+得分。

拿到这个元验证器后，可以用来增强前面的验证器，也就是把元验证器的奖励反馈加上重训一下。奖励就变成了：格式+得分+元验证器得分。元验证器得分用来堵“识别的问题没有监督”这个漏洞。

训练数据包含了 Dv 和 Dmv，对 Dmv 使用了与元验证器相同的奖励机制。得到的模型能够同时执行证明验证和元验证任务。

在 Dv 的验证集上，验证器的证明分析的平均质量分数——由元验证器评估——从 0.85 提升至 0.96，同时保持了证明分数预测的相同准确率。

小结

总的来说，这一大步就是想要训练一个能够精确识别问题并给出得分的验证器。也就是说，保证验证器的所有输出都是高质量的、“有监督”的。

证明生成

训练一个定理证明的生成器

其目标就是最大化上一步验证器的奖励，

max⁡πθEXi∼Dp,Yi∼πθ(⋅∣Xi)[RY]\max _{\pi_\theta} \mathbb{E}_{X_i \sim \mathcal{D}_p, Y_i \sim \pi_\theta\left(\cdot \mid X_i\right)}\left[R_Y\right]

自然，也是强化训练。

使用自我验证增强推理

当证明生成器无法一次性生成完全正确的证明时，迭代验证与改进可以提升结果。这一过程包括使用外部验证器分析证明，并提示生成器修正所识别的问题。

不过作者观察到这里有个关键限制：当生成器被要求一次性生成并分析自己的证明时，即便外部验证器轻易识别出错误，生成器也倾向于宣称证明是正确的。也就是说，生成器无法像专门的验证器那样以同样的严谨性评估自己的工作（即便告诉它也不行）。

因此，必须赋予证明生成器真正的验证能力：在训练过程中，提示生成器 πθ 先生成一个证明 Y，然后进行自我分析 Z，其格式和评分标准 Iv 与验证器一致。将自我分析中预测的证明分数记为 s′。

然后，使用验证器 πφ 对两个部分进行评估：证明 Y 获得分数 RY = s，自我分析 Z 获得元验证分数 Rmeta(Z) = ms。奖励如下：

R=Rformat(Y,Z)⋅(αRY+βRZ)RZ=Rscore(s′,s)⋅Rmeta(Z)\begin{aligned} R &= R_{format} (Y,Z) \cdot (\alpha R_Y + \beta R_Z) \\ R_Z &= R_{score}(s^{\prime}, s) \cdot R_{meta}(Z) \end{aligned}

R_format 用于验证证明和自我分析是否符合指定格式，R_score(s′, s) 用于奖励准确的自我评估，打分方法应该和前面《证明验证》环节一样。α = 0.76，β = 0.24。

这个奖励的激励包括：

  • 对错误的忠实承认会比错误地声称正确获得更多奖励。R_score为主。
  • 最高奖励来自生成正确证明并准确识别其严谨性。R_Y和R_meta为主。
  • 对证明生成器而言，获得高奖励的良好策略是在最终提交答案前尽可能多地识别并解决问题。所有R。

小结

让证明器自己也生成自我验证，然后评价自我验证得分、自我验证结果和验证器结果对比得分、证明器结果得分。我突然想到了在《Reward建模新范式：无验证器RL与Reference的妙用 | 长琴[2]》中介绍过的逆向奖励，不过这里更进一步，还需对生成的自我评估再次打分评估。

验证生成协同

于是，协同效应出现：验证器提升生成器的能力，而生成器能力提升后，会产生新的证明来挑战验证器当前的能力。GAN 起来了……为了方便人工标注，为每个证明生成了多个验证器分析，以便呈现潜在问题供人工审核。然后人工标注完再训练，这个闭环就转起来了。

同时，作者认识到两个使进一步提升自动化水平成为可能的事实：

  • 扩大验证器样本数量可以提高在有缺陷证明中捕捉真实问题的概率。
  • 审核验证器识别出的问题本身就是元验证，这比从零识别问题更容易。

基于此，开发了如下自动标注流程：

  • 对于每个证明，生成 n 个独立的验证分析。这里应该是生成器的自我分析。
  • 对于报告存在问题（得分为 0 或 0.5）的分析，生成 m 个元验证评估以验证所识别的问题。若大多数元验证确认分析结果，该分析即被视为有效。这里应该是用验证器分析。
  • 对于每个证明，检查打出最低分的分析。如果至少有 k 个此类分析被认为有效，则该证明被标注为该最低分。若所有验证尝试均未识别出合法问题，则证明标注为 1。否则，该证明将被丢弃或交由人工专家进行标注。这一步是关注得分了，如果最低分的有至少 k 个，标注为最低分，同时如果所有验证都无法识别问题，那肯定是 OOD badCase 了，直接标注；否则就是不确定了，需要人工参与或者直接丢掉。

总的来看，启示是：无论是奖励模型还是策略模型，最好不要只有分数，还要有过程，这样也便于人工参与。

小结

核心是验证器，其实可以理解成一个复杂的 Reward 模型——既能输出对结果的打分，还能输出评估过程，还能输出对评估的分析，以及对分析的打分。就是一个评估+评估再评估的综合验证器。这看起来是建模，其实是数据。包括后面的验证生成协同，其实也是怎么更好地搞数据。好吧，搞数据终于从生成器转到验证器了。

References

[1] DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning: https://github.com/deepseek-ai/DeepSeek-Math-V2
[2] Reward建模新范式：无验证器RL与Reference的妙用 | 长琴: https://yam.gift/2025/11/11/NLP/LLM-Training/2025-11-11-RM-New-Paradigm-Verifier-Free-RL/