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

上一章问的是能力前沿移动到了哪里，以及衡量它的仪器为什么很快饱和。能力问题还有另一面。前沿模型可能给出一个答案、一段程序、一份证明草稿、一个定理、一种设计、一个生物学假设，或一份市场预测。随之而来的问题不是它听起来是否可信，而是谁、或者什么东西，能检查它。

这就是验证前沿。它不是算力前沿的另一个名字，也不是把整个安全问题换个说法。它指的是这样一道前沿：生成候选主张的成本，下降得比把这些主张变成可接受知识的成本更快。当生成器变得便宜而强，稀缺资源就会转移到证明、复现、对抗性审查与制度接受上。

本章把前面几部分分散出现的线索合在一起。第 21 章 解释过可检查奖励为什么能强化后训练。第 27 章 把验证器当成推理组件来讲。第 52 章 论证过，智能体评测应当验证环境状态，而不是相信自我报告。第 55 章 则追问弱人类怎样监督更强系统。还缺的那一环，是基础设施问题：当模型越过某条能力边界之后，必须出现什么证据，结果才算可信？

接受，而不只是生成

有用的抽象，是一个带证据的主张。令 $x$ 表示问题，$y$ 表示模型给出的答案，$e$ 表示它为答案提供的证据：证明对象、测试套件、轨迹、实验、数据产物、推导链，或一组反驳与回应。验证器 $V$ 把这组三元组映射成一个分数或决定。部署系统只在分数超过阈值时接受主张：

$$A(x, y, e) = \mathbf{1}[V(x, y, e) \geq \tau].$$

换句话说，$A$ 是接受规则。验证器分数 $V$ 衡量这份证据是否足以支撑这个主张， $\tau$ 则是部署系统或机构选择的接受阈值。

支配前沿的，是生成 $y$ 的成本和检查 $e$ 的成本之间的差距：

$$\Delta(x) = \log C_{\mathrm{verify}}(x, y, e) - \log C_{\mathrm{generate}}(x, y).$$

式中的 $\Delta$ 衡量的是对数成本差。它为正，表示检查已经比生成更贵；它为负，表示验证仍是循环里更便宜的一侧。

当 $\Delta(x) < 0$ 时，验证比生成便宜。这是理想区间：编译器做类型检查，单元测试抓住回归，Lean 内核检查证明，定理证明器验证证书，模拟器拒绝无效的物理轨迹。当 $\Delta(x) > 0$ 时，模型能产出比机构能检查的更多候选主张。失效不再是模型说不出有用的东西，而是世界被大量产物淹没：它们貌似可信，接受成本却高于生成成本。

因此，「模型解决了一个未解数学问题」不是终点。它只是一个主张进入接受流程。一个有用的流程会要求精确定义、证明草稿、在可能时做形式化或规约、如果领域允许则给出小检查器或证明助手证书、在形式化缺口仍存在处进行独立人类审查，并保留审计记录，把被接受的定理追溯到实际被检查的那个产物。没有这条流程，结果还不是知识，只是一个猜想性输出。

三种验证制度

「验证」这个词遮住了好几种制度。它们的差别在于，究竟是什么让答案可信。

第一种制度是可执行验证。它在主张可以规约成一个小的、确定性的检查器时最强。编译器证明程序保持语义，证明助手（本章提到的几种主要有 Coq、HOL Light、Isabelle、Lean）把定理交给可信内核检查，数据库约束拒绝不可能状态，单元测试运行产物而不是阅读解释。经过验证的编译器这条线由来已久，却很关键：CompCert 用 Coq 对一个编译器后端给出了语义保持的形式化证明 (Leroy 2009)。Flyspeck 在大型数学结果上做了同样的事，用 HOL Light 和 Isabelle 给出了 Kepler 猜想的形式化证明 (Hales et al. 2015)。它保证的不是项目周围每句非形式化话语都为真，而是某个具体形式化产物能通过一个小可信基。

第二种制度是辅助监督。证据不是证书，而是一套帮助较弱评判者评估较强系统的结构化程序。迭代放大把困难判断拆成较容易的子问题 (Christiano et al. 2018)。辩论让两个系统互相暴露错误，再由人类裁判 (Irving et al. 2018)。弱到强泛化测试弱监督能不能引出更强系统已有的潜在能力，结论是能恢复一部分，但远未完全 (Burns et al. 2024)。AI control 问的是另一个问题：即使正在使用的模型不能被信任，协议能不能仍然保持可接受的安全性 (Greenblatt et al. 2024)？这些不是证明系统。它们是在直接人类评估不再能扩展时，维持判断能力的尝试。

第三种制度是经验验证。许多主张不是形式对象。它们关乎一个药物靶点、一种用户行为、一个物理系统、一种嵌在大栈里的新算法，或一次带真实流量的部署变更。在这里，验证意味着实验设计、复现、留出数据、出处与审计轨迹。模型可以压缩寻找假设的过程，但关于世界的假设，仍要和世界接触。在这种制度里，瓶颈常常不是智能，而是时间、仪器和独立复现。

作为基础设施的形式证明

数学是最适合看清生成与接受之别的地方。模型可以写出一份很有说服力的证明草稿。形式证明助手要的是更多东西：用精确语言写出的陈述，以及每一步都能被检查的证明对象。因此，形式定理证明已经不只是一个基准类别，而成了一类前沿基础设施问题。

这条线可以从数据集和系统里看出来。GPT-f 表明，Transformer 可以生成 Metamath 证明，甚至提交被库接受的短证明 (Polu and Sutskever 2020)。MiniF2F 给领域提供了一个跨系统的奥数级形式化基准，覆盖 Metamath、Lean、Isabelle 和 HOL Light (Zheng et al. 2021)。FrontierMath 则采取另一条路线：用专家审定的原创数学题和自动验证来降低污染风险，并让基准在研究前沿保持难度 (Glazer et al. 2024)。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)。

population = seed_candidates(problem)
archive = []

while budget_remains():
    proposal = model.mutate(select(population, archive))
    score, evidence = evaluator.run(proposal)
    if evidence.is_checkable and score > threshold:
        archive.append((proposal, score, evidence))
    population = update(population, proposal, score)

return audit_and_reproduce(archive)

评估器是枢纽。如果评估器是精确的，比如证明检查器、确定性基准，或带清楚不变量的模拟器，循环可以跑得很快。如果评估器只是弱代理，循环会优化那个代理。如果评估器是人类小组，循环就受限于稀缺的人类注意力。如果评估器是一项实验，循环就受限于湿实验、现场或部署时间。

本书反复使用的「能力、效率、信任」视角在这里很有用。生成提高能力，搜索提高候选空间上的效率，信任只来自评估器。没有强评估器的发现系统，是一台修辞机器。有强评估器的发现系统，则会加速那些验证已经被工程化的领域。

当验证者更弱时

最难的情形并不是形式数学，而是这样一类任务：答案很重要，证据很复杂，最好的验证者却弱于生成者。这就是验证前沿的对齐版本。

过程监督是一种回应。它不只问最终答案是否正确，还问每一步是否有根据。在 MATH 上，逐步过程监督优于结果监督，并产生了 PRM800K 这个人类逐步标注数据集 (Lightman et al. 2023)。过程奖励模型（process reward model，简称 PRM）正是从这类标注里学会给每一步推理打分，而不只是给最终答案打分。生成式验证器则把验证器本身做成一个能推理、能解释、能在判断时花测试时算力的模型 (Zhang et al. 2024)。这些方法会改善选择，但也会把问题向上一层移动：现在验证器自己的推理也需要被评估。

可扩展监督走得更远。辩论、放大、弱到强泛化和控制，都从同一个不舒服的事实出发：直接人类判断可能不够。近期关于 eliciting latent knowledge 的不可能性结果把这一点说得更尖锐。eliciting latent knowledge（简称 ELK）要解决的是：如何让系统报告它内部真正知道的东西，而不是它预测打分者想听的东西。Friedl 等用因果影响图把 ELK 形式化，并证明：没有一种只依赖智能体行为的反馈式训练策略，能够在确定意义上保证训练出诚实智能体，即使训练反馈本身是完美的 (Friedl et al. 2026)。这个结果是理论性的，不该被读成实践监督已经结束。它对本章说的是另一件事：如果唯一证据只是人类本来就能打分的行为，那么某些隐藏知识或欺骗，不能只靠训练反馈排除。

运营上的含义，是分层验证。

1. 要求证据采用不同于模型流畅散文的媒介：代码、证明对象、检索来源、日志、测量和环境状态。
2. 优先选择不继承生成器失效模式的独立检查。
3. 用对抗性审查暴露分歧，而不是让相近模型多数投票。
4. 保留出处，使被接受的结果能追溯到实际被检查的产物。
5. 对暂时无法检查证据的主张延后接受。延后不是失败，而是机构保存标准的方式。

失效模式

验证会以一些可识别的方式失效。点名这些失效很重要，因为每一种都需要不同对策。

• 用复杂性制造压迫感。 产物很长、很技术、很像真的，但没有检查器或审查者把它规约成可负责的主张。
• 形式化错误。 证明助手检查的是一个比原定理更弱、更强，或干脆不同的陈述。
• 基准过拟合。 验证器是公开基准或评分准则，生成器学会的是它的形状，而不是底层任务。
• 代理目标被钻空子。 评估器便宜，而且只在成为优化目标之前和真实质量相关。
• 共享盲点。 评判模型、批评模型和生成模型共享训练数据、架构、提示或产品激励，所以一致并不是独立证据。
• 不可复现的经验结果。 科学主张通过了一次运行、一个笔记本或一个私有数据集，却不能被独立方复现。
• 接受被漂白。 一个结果从「模型说」移动到「论文说」再到「机构接受」，中间没有任何阶段增加新证据。

解法不是一个万能验证器，而是一组失效模式不同的检查。领域允许时用形式证明；执行足够时用测试和模拟器；文本主张用检索与来源归因；经验主张用独立复现；价值、意图或法律责任相关处保留人类判断；相关一致很便宜时，用对抗性审查。

这如何改变前沿

验证之所以是前沿，是因为它改变了能力的含义。一个模型能提出正确定理，却给不出可检查证明，它给数学家创造的是线索，不是已被接受的定理。一个模型找到有前景的分子，却不能复现实验效果，它创造的是假设，不是疗法。一个模型写出迁移计划，却不能运行并验证它，它创造的是草案，不是一次操作。

这也回答了分类问题。验证不是 HBM、电力、封装或集群可靠性那种算力前沿。它仍属于这一部分，因为前沿不只在模型之下。某些真正起约束作用的限制在模型之上：测量、证明、信任、机构审查，以及接受主张的成本。到 2026 年，领域生成候选项的速度，已经超过很多机构吸收它们的速度。这是一个基础设施事实。

它与后文的交接也很直接。第十部分会问，这些约束怎样变成市场、数据权利、开放选择和制度激励。第十一部分会问，怎样在这些约束下运营系统：审查闸门、发布证据、SLO、预算、事故记录和运营契约。验证前沿留下的判断是：最强的系统不只是能生成最好的答案，而是能让答案变得便宜可查。

延伸阅读