跨越非正式AI：Carina Hong与Axiom Math的Verified AI

标题：🔬超越非正式 AI——Axiom 数学的 Carina Hong

来源：https://www.latent.space/p/axiom

发布时间：2026-06-03T19:27:49+00:00

2025 年，成立仅七个月的初创公司 Axiom 解决了 Putnam 考试全部 12 道题（在时限内得分 8/12）。Putnam 考试是一项享有盛誉的本科数学竞赛，12/12 的成绩优于顶尖本科生（110/120）以及此前报告结果的最接近 AI 系统（DeepSeek 103/120），尽管在给予更多时间的情况下，人类和其他系统可能取得的分数尚不明确。无论如何，Putnam 考试以难度著称，中位数得分通常为 0 或 1 分。单看这一点，似乎不过是 AI 在精英赛事中战胜人类的又一小小成就，自 Deep Blue 击败卡斯帕罗夫以来，AI 系统在各类竞赛中已屡建奇功。

快进到 2026 年中，Claude Code 和 Codex 正在引发全球关注。2024 年，Anthropic 专注于代码与企业市场的押注，看起来比 OpenAI 的更强大模型与大规模消费级布局更为务实。如今，Amodei 通过代码实现加速的全情投入（图像和视频暂且不论）显得颇有远见。

尽管 Anthropic 势头正盛，Axiom 首席执行官 Carina Hong 却认为，编码能力只是通往 AGI 的必要而非充分里程碑。代码或许已将参差不齐的前沿推进到某些非编码领域的超级智能边缘，但 Carina 指出仍存在令人惊讶的缺口（链接），她认为这些缺口将成为 AI 进步的瓶颈。（数学基准统计）

“Verified AI”听起来像是吃西兰花1和缴税一样枯燥，但在 Axiom 看来，其含义截然不同。“对我而言，验证关乎放大卓越、叠加卓越，”Carina 告诉我们。

我花了些时间才真正理解她话中的含义（起初听起来像是营销话术，直到我恍然大悟）。Carina 以传奇数学家 Srinivasa Ramanujan（《The Man who knew Infinity》）为例来阐明这一点。当 G.H. Hardy 最终说服 Ramanujan 用正式证明取代依赖其（强大）直觉时，据说反而提升了他自身的能力。原因在于，正式证明迫使 Ramanujan 将细节条理化，从而开辟新的思考路径，等等。这就是数学中的“叠加”——在坚实而非摇摇欲坠的基础上构建……也就是所谓的 公理。

而正式证明也让他人受益于他的直觉：证明是传达直觉并说服他人其直觉正确的方式。这就是“放大”（更多人使用该结果）和“叠加”（人们能从中学习并在此基础上继续构建）。

这正是让我们理解 Axiom 方法的核心洞见。

Verified AI 体现在训练与推理两个层面。

先做个简要插曲：粗略地说，“形式化验证”意味着使用类型检查器（如 TypeScript、C++ 或 Rust 的类型系统，但能力更强）来验证用 Lean2 等语言精心指定的数学证明。将一份“非正式”证明（尽管大多数人不会将其称为“非正式”）转化为 Lean 证明需要大量工作3。Axiom 本身已开源了开创性成果 AXLE——一套用于探索、验证和操作数学证明的交互式 Lean 应用工具包。

你可以想象这在强化学习中的巨大价值：无需依赖基于统计的猜测（如 GRPO、RLHF 等），而是直接用 Lean 验证器确认证明是否正确。这显然是一种更强的奖励信号，类似于编译代码并进行测试（这也是在代码任务上进行 RL 的常见做法）。

难点在于：目前 LLM 在用 Lean 证明问题方面并不出色。

Axiom 登场：除了 12/12 的 Putnam 成绩外，他们尚未正式公布其他基准数据，但 Carina 表示，他们在 Verina 代码生成基准 上取得了非常出色的 99%（187/189）ProofGen 成绩。该基准要求为一系列问题生成代码并附带正确性证明。作为参考，OpenAI 的 o3（已知的最后一次 OpenAI 运行）在该基准上仅取得 4.9% 的成绩。

基于有限的基准数据，很难判断前沿实验室在年度 IMO 里程碑之外的表现，但 Carina 暗示，他们目前仍不直接训练生成 Lean 证明，而是依赖非正式证明。

时间会证明前沿实验室的现有方法能否弥合这一差距。

Carina 的 Ramanujan 类比相当直接：更好的证明 → 更好的 Lean 生成 → 更好的 RL。更强的信号意味着更高的样本效率和更高的性能上限。太棒了！

放大效应也很清晰：一旦我在 Lean 中证明了某件事，输出质量几乎4与人类相当，因此我的高质量训练集得以扩大，而这是非正式 rollout 数据集无法实现的。我可以信任我的 Lean 证明。

叠加效应同样清晰：未来的推理与训练都可以在此基础上继续构建。

另一方面，仅依赖统计信号（如 RL 中的 GRPO）训练的模型，无法获得使用形式化验证的系统所享有的样本效率、性能上限和叠加语料库的优势。

尽管卷心菜和报税单让人头疼，验证却在我们的对话中频繁出现。在物理系统领域，让我们回顾一下 [Applied Intuition](https://www.latent.space/p/appliedintuition) 的观点：

“我认为[可验证性]目前可能是最难的问题，因为随着模型变得更好，系统中的缺陷越来越难被发现。因此，通过适当的评估来找出这些缺陷，这一问题也会随着模型的提升而变得更加困难。”

在理论物理领域，我们记得 Alex Lupsasca 的看法：

“……现在我们已经进入了一个阶段，只需让 ChatGPT 同时处理成千上万个问题，其中相当一部分会返回证明。现在，真正需要人类去做的，就是验证所有这些输出。因此，当这成为瓶颈时，我认为形式化数学并自动化验证将变得更有价值。”

事实上，验证正是 AI 用于科学与 AI 用于计算之间的关键区别：在科学中，你必须通过进行物理实验来测试（验证）你的假设。像 Radical AI 和 Lila 这样的“实验室在环”系统正是基于这一前提构建的（我们已录制了与这两支团队的节目，即将发布！）

而且，随着运行飞行控制、核电站和起搏器等关键系统的软件和硬件变得越来越复杂，对这些系统进行形式化验证正成为一个日益重要的关注点。

Carina 对 AGI 需要经过验证的生成深信不疑，她甚至直言不讳地断言：“我们认为没有其他可能的未来。”

Lean 证明很难生成，但一旦生成，很容易被判定为正确或错误。但你如何确定自己创建的证明与你关心的问题正确对应呢？正如 Carina 所说：“任何可以被明确表述的东西都可以被证明。人类不擅长把我们想要的一切都表述清楚。”

我们是否正在进入“规格制定”行业？请收听节目，了解 Carina 的观点，以及：

• 为什么硬件验证是杀手级应用
• AXLE 开放 API 与最近发布的 Discovery 工具包的细节
• Erdos 事件
• OpenAI GPT-f 的分化

视频 5

时间轴：

• 0:00 开场：2 亿美元的 A 轮融资与数学创业论点
• 4:52 经过验证的 AI：放大卓越，而非修补平庸
• 13:42 Axiom 的系统：Lean 数据、强化学习与 Putnam 完美分数
• 22:12 数学发现——在猜想之前
• 25:12 稻除定理、不完备性与实际限制
• 30:42 带证明的代码——Verina 基准
• 37:57 证明树、上下文窗口与扩展限制
• 43:57 市场、护城河与商业案例（16 亿美元估值）
• 55:27 个人起源：牛津、UCL Gatsby、斯坦福法学院
• 1:00:57 Erdos 争议与搜索的难度
• 1:06:02 数学领域的 AlphaZero 与自我改进
• 1:08:47 创业优势与 OpenAI GPT-f 线程
• 1:13:17 Axle API——大规模 Lean 的开放基础设施
• 1:20:47 协作、Polymath 与人类注意力的瓶颈
• 1:22:21 创立故事——痴迷、法学院与 Julie Zhuo
• 1:26:17 更宏大的愿景——AGI、科学与迁移学习
• 1:35:02 瓶颈、碎片化与领域未来

1

其实我很喜欢卷心菜，但另一方面，我强烈相信测试驱动开发，所以 ¯\_(ツ)_/¯

2

形式化验证还包括模型检测（TLA+、SPIN）、基于 SMT 的工具（Dafny、F*、Why3）以及精炼类型系统（Liquid Haskell）——其中许多从用户角度来看并不像“在证明上做类型检查”，尽管底层逻辑核心可能相似。它也应用于软件和硬件的正确性，而不仅限于纯数学。

3

这其实是个轻描淡写的说法。大多数定理仍然停留在非正式层面，因为形式化工作极其困难。人们已经投入大量精力去形式化最重要的证明，但结果参差不齐。

4

有人可能会认为其难度略低，因为证明对 LLM 来说是以分布形式存在的。