验证前沿：能力之后的证明、监督与信任

上一章追问能力结果究竟测量了什么。本章接着问：我们需要什么证据，才有充分理由根据一项结果采取行动？模型几秒钟就能产出答案、证明思路、程序、设计、生物学假设或市场预测。生产不等于接受。两者之间还有规格、检查、复制实验、判断与问责。

验证前沿是生成主张与有充分理由接受主张之间的差距。主张可能为真、可能有用，也可能两者皆非。这里关心的是，现有证据与审查流程能否支撑一个决定。它的范围小于整个安全问题，也不同于算力前沿。验证前沿只是一项工作假设，不是经过测量的普适定律。在一些领域，检查成本很低；在另一些领域，准备证据和独立审查才是主要工作。真正需要回答的是：候选结果越来越多时，审查能力会在何处成为约束。

本章把此前出现的几条线索连在一起。第 21 章 解释了为什么可检查的结果能成为有力的训练信号；第 27 章 把验证器视为推理组件；第 52 章 要求用环境证据替代智能体的自我报告；第 55 章 则讨论如何监督不能完全信任的系统。中间还缺少一套接受纪律：主张是什么，必须附带哪些证据，各项检查能够证明什么，以及谁有权作出决定？

一个主张需要证据契约

有用的单位是带证据的主张。用 $c$ 表示主张，用 $e$ 表示证据包。证明对象、测试报告、执行轨迹、数据集、实验方案、模型卡和异议记录都可以成为证据，但它们提供的证据并不等价，也没有哪一项能单独接受这个主张。

审查开始前，先把主张归入类别 $j$，例如形式定理、软件变更、经验效应或发布决定。每一种主张类别都有版本化的证据契约。下面是一种策略模板：

$$\begin{aligned} A_j(c,e)=\mathbf{1}\!\Big[ &\,p_j(c,e)=1 \\ &\land \bigwedge_k h_{jk}(c,e)=1 \\ &\land \bigwedge_\ell s_{j\ell}(c,e) \geq \tau_{j\ell} \Big]. \end{aligned}$$

其中，$A_j(c,e)$ 是策略对类别 $j$ 的主张给出的二元接受结果；$p_j(c,e)$ 是来源判定条件；$h_{jk}(c,e)$ 是由 $k$ 索引的必需硬性检查；$s_{j\ell}(c,e)$ 是由 $\ell$ 索引的诊断分数；$\tau_{j\ell}$ 是相应的分数阈值。符号 $\mathbf{1}[\cdot]$ 表示括号内所有条件成立时取 1，否则取 0；$\land$ 表示「并且」，$\bigwedge$ 表示所有带索引的条件都必须成立。

这只是一项版本化策略的模板，不是对真理的普适定义。契约必须写清楚适用哪些硬性检查与分数、缺少证据时如何处理，以及哪个接受决定的责任主体拥有决定权。实验室、维护者、监管机构或事故指挥者完全可能因为公式之外的风险或管辖要求，合理地拒绝一项证据充分的主张。这个公式让策略可以审查，却不会把判断变成真理。

验证能力受制于待审队列

成本比值会掩盖运营问题，一条简单的待审队列能把它显露出来。对同一主张类别和同一风险等级，$B_t$ 表示区间 $t$ 开始时的待审项目数，$G_t$ 表示该区间新进入的主张数量，$R_t$ 表示已经完成的审查决定数量，包括接受、拒绝或暂缓。那么

$$B_{t+1} = \max\{0, B_t + G_t - R_t\}.$$

这些量必须使用可比单位。一次很快完成的代码风格检查，不能与一次临床复制实验放进同一队列。这是计数恒等式，不是排队论定理。它省略了优先级、服务时间差异、返工和审查人员可用性，却仍然揭示了关键事实：新到主张长期多于已完成决定时，待审工作必然累积。

def final_backlog(arrivals, reviews):
    backlog = 0
    for new_claims, completed_reviews in zip(arrivals, reviews):
        backlog = max(0, backlog + new_claims - completed_reviews)
    return backlog

intervals = 12
arrivals = [40] * intervals
fixed_reviews = [20] * intervals
scaled_reviews = [45] * intervals

print("fixed capacity backlog:", final_backlog(arrivals, fixed_reviews))
print("scaled capacity backlog:", final_backlog(arrivals, scaled_reviews))

这个例子刻意保持简单，不预测任何实验室或产品团队。它说明的是，生成器基准若不同时报告主张到达速度、审查能力、决定耗时与积压的年龄分布，就并不完整。

不同检查提供不同保证

「已经验证」只有在同时说明验证对象与保证内容时才有意义。不同检查回答的问题并不相同：

• 证明内核。 它能证明某个证明对象按照已编码的公理与内核规则，确实推出精确的形式化陈述。它不能证明陈述符合原本意图，也不能证明可信计算基毫无缺陷。
• 类型检查器、编译器证明或静态分析。 它能证明产物符合给定的类型、转换规则或程序属性，却不能证明程序具备所有期望行为。
• 测试与执行。 它能证明程序在受测环境中、对已经执行的测试用例表现如何，却不能证明未经测试的输入或环境一定不会失败。
• 模拟器。 它能证明结果在模拟器模型与假设之内如何表现，却不能证明物理世界会出现相同行为。
• 计算可重复性。 它能证明使用相同的数据、代码和方法，可以重新生成结果，却不能证明换用新的数据仍能复制结果，也不能排除共同偏差。
• 实验可复制性。 它能证明针对同一问题收集的新的数据支持相容结果，却不能证明一项永恒的二元真理，也不能证明结论适用于所有人群。
• 模型或人工审查。 它能根据量规和现有证据给出有理由的判断，却不能产生证书，而且相关的审查意见并非独立证据。

美国国家科学院区分了计算可重复性（reproducibility）与实验可复制性（replicability）：前者使用相同数据和方法重复计算，后者使用回答同一科学问题的新数据得到一致结果 (National Academies of Sciences, Engineering, and Medicine 2019)。复制结果本身仍然有程度、效应量、不确定性和适用范围之分，不会自动把主张变成事实。

作为基础设施的形式证明

形式数学最清楚地展示了提议与接受的区别。证明助手需要精确的陈述和证明对象，再由一个小型内核检查这个对象是否遵循形式规则。寻找证明可能非常困难，检查证明却可能很便宜，但保证只到形式边界为止。

CompCert 是一个有代表性的软件案例。它经过验证的后端证明了从 Cminor 到 PowerPC 汇编这一特定转换的语义保持定理，并不意味着任意编译器都能证明任意程序正确 (Leroy 2009)。Flyspeck 使用 HOL Light 和 Isabelle 形式化了开普勒猜想，并为该形式化陈述生成机器检查过的证明 (Hales et al. 2017)。这两个案例的证据链都包括陈述、证明、内核、库和工具链。

神经定理证明改变的是证明搜索，不是这条接受边界。GPT-f 生成 Metamath 证明，并找到被证明库接受的短证明 (Polu and Sutskever 2020)。MiniF2F 提供 488 道奥数级形式化陈述，首次发布时完整覆盖 Metamath 与 Lean 翻译，并部分覆盖 Isabelle 和 HOL Light (Zheng et al. 2022)。FrontierMath 使用专家原创题和自动答案检查来降低污染风险，但答案检查器不等于形式证明，也不能证明每个解答过程 (Glazer et al. 2024)。2026 年 6 月 12 日，Epoch 在修正或移除影响 42% 的题目后发布 FrontierMath v2，剩余 338 题。检查器可以给指定题目的答案评分，却不能保证题面与参考答案本身没有问题 (Epoch AI 2026)。LeanDojo 发布用于 Lean 交互和前提检索的工具、数据与基准 (Yang et al. 2023)。DeepSeek-Prover-V2 把非形式化分解与 Lean 4 证明搜索结合起来 (Ren et al. 2025)，AlphaGeometry2 则把语言模型与符号几何引擎结合起来 (Chervonyi et al. 2025)。

这些系统缩小了验证问题的一部分，但仍留下四道缺口：

• 形式化缺口。 精确的形式化陈述必须表达出人们真正想证明的定理。错误的形式化陈述，也可以得到完全通过检查的证明。
• 库缺口。 定义、既有引理及其假设都属于证据基础。
• 内核信任。 内核是一个小型可信计算基，不是绝不会出错的神谕。构建过程、硬件和证明导出路径同样重要。
• 翻译缺口。 自然语言发现、非形式化论证与形式证明是不同产物，把它们连接起来本身就是实质工作。

发现循环需要评估器

候选结果能由代码评分时，自动发现尤其有效。AlphaEvolve 只有在由人类提供评估代码后，才会在程序空间中搜索。这些代码把候选结果映射成标量指标，因此也定义了何为改进。需要人工实验的任务不在该系统报告的适用范围内 (Novikov et al. 2025)。

这一区分可以避免一个诱人但危险的捷径。评估器分数是搜索证据，不是接受决定。在论文报告的应用中，有希望的 AlphaEvolve 候选结果仍要接受与具体案例相符的检查，例如留出测试、专家检查、硬件验证或部署后测量。以数据中心调度结果为例，验证从历史快照上的模拟，推进到未见过的工作负载，最后才到机群测量。评估循环让搜索变得可行，并没有取消发布审查。

如果评估器只是代理指标，反复优化就可能利用指标与真实目标之间的差异。如果评估器是模拟器，结果会继承模拟器的假设。如果评估器是学习得到的评判模型，相关错误可能伪装成相互印证。因此，发现流程还需要第二道边界：用独立证据验证选出的候选结果，而且这份证据不能只是生成时使用的适应度信号。

当验证者更弱时

更困难的情形，是主张的证据很复杂，而现有最强评判者仍弱于生成器。学习式验证器和可扩展监督协议试图增加审查能力，但都不应被描述成证明系统。

过程监督是一个适用范围明确的案例。PRM800K 研究为模型生成的 MATH 解题步骤收集了约 80 万个人工标签。过程奖励模型在 Best-of-N 选择上优于研究中的结果奖励基线，但实验没有通过强化学习训练生成器，也没有证明所有看似合理的思维链都忠实反映模型的推理 (Lightman et al. 2024)。生成式验证器把正确性作为下一个词元预测任务来训练，可以生成验证理由、使用思维链，并在推理时投票。这些理由是学习得到的判断，不是证书 (Zhang et al. 2025)。

更广泛的协议也只有边界明确的证据：

• 迭代放大提出递归分解，并用硬编码分解器测试了五项合成组合任务。这些实验不能证明人类可以分解困难的现实判断 (Christiano et al. 2018)。
• 最初的辩论论文在最优博弈的假设下提出对抗性论证，其实验使用 MNIST 和稀疏分类器，而不是人类评判者。这是一项研究议程，不能证明更强系统总能揭露彼此的错误 (Irving et al. 2018)。
• 弱到强实验在自然语言处理、国际象棋和奖励建模任务上，使用 GPT 系列模型提供的弱标签。一些方法恢复的能力多于简单模仿，但仍低于完整的强模型监督，也没有模拟从人类监督超人系统时的所有属性 (Burns et al. 2024)。
• AI control 在一组 5,000 项 APPS 编程任务上评估协议，把 GPT-4 当作不可信模型，把 GPT-3.5 当作可信模型，并由红队攻击策略构造带后门的代码。研究展示了该测试环境中的控制评估方法，不构成对真正失调系统的部署保证 (Greenblatt et al. 2024)。

最新的理论限制同样需要谨慎解读。Friedl 等人用因果影响图建立潜在知识提取模型。在他们的设定中，训练分布是所有可能情形的真子集；评估器在训练分布上完全正确，却会在分布外的某处出错；训练过程可能无法区分多个稳健而有能力的智能体。对这一特定类别的纯行为反馈，训练无法确定地保证得到诚实智能体 (Friedl et al. 2026)。该定理并没有证明每一种实际监督方法都会失败。它指出的是：在这些假设下，仅凭行为无法排除一个模拟评估要求的解。

独立性与来源记录

重复同一个判断，不等于增加了证据。生成器、批评模型和评判模型可能共享训练数据、架构、检索来源、提示或组织激励。它们的相关一致可以帮助搜索，却仍然只能提供很弱的确认。因此，独立性是一项必须记录的属性，不是「不同的模型名称」的同义词。

来源记录还要回答另一个问题：审查者检查的，是否就是实际发布的产物？用内容哈希保存候选结果、配置、数据版本、工具输出和证据包。记录运行了哪个检查器版本、谁有权修改，以及后续发生了哪些转换。缺少这条关联后，已经接受的证明、二进制文件、数据集或模型，都可能被未经检查的相邻版本悄悄替换。

失效模式

以下失效会在不同领域反复出现：

• 以复杂性压人。 用篇幅和技术流畅度替代可问责的主张与检查。
• 形式化错误。 内核证明的陈述与原本意图存在细微差异。
• 覆盖错误。 测试虽然通过，重要输入、环境或属性却从未执行。
• 代理劫持。 生成器学会提高评估器分数，却没有改善真实目标。
• 共享盲点。 看似独立的评判者继承了同一种失效。
• 不可重复的经验结果。 代码、数据和环境无法重新生成报告结果。
• 接受漂白。 「模型提出」在中间没有任何基于新增证据的决定时，变成「机构知道」。

对策不是寻找一个万能验证器，而是刻意组合一组边界明确、失效方式不同的检查，再由负有责任的主体作出决定。

运营台账

每项后果重大的结果，都应保存一份简洁的接受记录：

1. 主张 ID 与类别： 精确命题、产物、适用范围和风险等级。
2. 证据契约版本： 必需检查、阈值与暂缓规则。
3. 生成器与资源预算： 模型、提示或运行框架、工具、尝试次数、算力与耗时。
4. 证据哈希： 对证明、轨迹、代码、数据与实验方案的不可变引用。
5. 检查器版本与独立性： 工具版本、操作人员、数据来源、利益冲突与共享依赖。
6. 结果与局限： 硬性检查输出、诊断分数、不确定性、失败检查与未决异议。
7. 接受决定的责任主体： 具有法律或运营授权的具名责任人。
8. 决定与日期： 接受、拒绝或暂缓，以及作出决定的理由。
9. 失效条件： 时间、模型变化、证据变化、事故或领域漂移，任何一项触发后都必须重新审查。
10. 重复或复制状态： 谁在什么数据与环境上重复了计算，或复制了经验结果。

这份台账不会把薄弱证据变强，却能防止主张从模型输出流向报告、产品或政策时，不确定性悄然消失。

这如何改变前沿

模型提出一个定理，却拿不出可检查的证明，产出的只是线索，不是已接受的定理。分子在模拟中显示出可观效果，仍然只是假设，不是疗法。迁移计划没有在目标环境中运行过并通过验证，也只是草案，不是一次操作。这些并非措辞上的细枝末节，而是在标明尚未完成的工作。

前沿是一个证据工程问题。应当测量主张流、每项检查的覆盖范围与局限、待审积压、决定耗时，以及被接受主张后来失败的比例。只改进生成器而不改进这些系统，既可能创造价值，也可能制造噪声，还可能两者同时发生。实际结果取决于领域及其接受机制。

与全书后半部分的交接也很直接。第十一部分会问，这些约束如何变成市场、数据权利、开放程度的选择与制度激励。第十二部分会问，如何在这些约束下运营系统，包括审查闸门、发布证据、SLO、预算、事故记录和运营契约。能力强的系统不只生成有用的候选结果，还会让从主张走向有充分依据的行动这一过程清晰、可检查，并与风险相称。

延伸阅读