Axiom CEO谈形式验证：AI扩展的关键在于可验证的数学证明

2025年，成立仅7个月的初创公司Axiom在普特南考试（一项极具声望的本科数学考试）中解决了全部12道题（限时内得分8/12）。

12/12的成绩优于顶尖本科生（110/120）以及此前报告结果的最接近AI系统（DeepSeek 103/120），尽管尚不清楚人类和其他系统若有更多时间会得到多少分。然而，普特南考试以其难度著称，中位数分数通常为0或1分。

单看这一成就，它似乎只是AI荣誉簿上的一笔；是AI系统在与人类精英竞赛中取得的一系列成就之一，始于深蓝击败卡斯帕罗夫。快进到2026年中，Claude Code和Codex正风靡全球。

2024年，Anthropic押注代码和企业，相比OpenAI更优的模型和庞大的消费规模，这看起来更像是一种务实的利基策略。如今，Amodei全力押注通过代码加速（图像和视频暂且不论）似乎颇具先见之明。

然而，尽管Anthropic势头正盛，Axiom CEO Carina Hong认为编码能力是通往AGI道路上必要但不充分的里程碑。代码可以说将锯齿形前沿推向了编码之外某些领域的超级智能，但Carina认为存在令人惊讶的差距（链接），这些差距将阻碍AI的进步。

（数学基准统计数据）。

非正式瓶颈“经过验证的AI”听起来像吃西兰花和纳税，但对Axiom而言，它意味着截然不同的东西。“验证对我来说是关于扩展才华、复合才华，”Carina告诉我们。我花了一段时间才理解她的意思（听起来像营销话术，直到恍然大悟）。

Carina引用了传奇数学家斯里尼瓦萨·拉马努金（《知无涯者》）来说明这一点。当G. H. 哈代最终说服拉马努金正式证明定理，而非依赖他（强大）的直觉时，据报道这提升了他自己的能力。这大概是因为正式证明迫使拉马努金以开辟新思路的方式阐明细节，等等。

这就是你在数学中“复合”的方式——建立在坚实而非摇摇欲坠的基础上……也称为公理。但正式证明也让其他人受益于他的直觉：证明是传达直觉并说服他人直觉正确的方式。这就是扩展（更多人使用结果）和复合（人们可以学习并基于他的工作继续推进）。

这是理解Axiom所采取方法的核心见解。验证生成经过验证的AI以两种方式出现：训练和推理。

但快速绕道：粗略地说，“形式验证”意味着使用类型检查器（如TypeScript、C++或Rust，但功能更强）来验证使用Lean等语言精心指定的数学证明。将“非正式”证明（尽管大多数人不会认为它“非正式”）转化为Lean证明需要大量工作。

Axiom自身开源了开创性工作AXLE——他们的交互式Lean应用程序工具包，用于探索、验证和操作数学证明。你可以想象这在强化学习期间会非常有用：无需依赖基于统计的最佳猜测（GRPO、RLHF等），你可以直接使用Lean验证器来验证证明是否正确。

这显然是一个更强的奖励信号，类似于编译并测试代码（这是RL在编码中通常的做法）。问题在于：LLM目前不太擅长使用Lean进行证明。

Axiom登场：尽管除了12/12的普特南结果外，他们尚未正式报告基准数字，但Carina报告称，他们在Verina代码生成基准上实现了非常令人印象深刻的99%（187/189）ProofGen。

该基准要求为一系列问题生成代码和正确性证明。作为背景，OpenAI o3（已知的最后一次OpenAI运行）在该基准上仅获得4.9%。

基于稀疏的基准测试，很难说前沿实验室目前在年度IMO里程碑之外的表现如何，但Carina表示，他们仍然没有训练直接生成Lean证明，而是依赖非正式证明。时间会证明前沿实验室当前的方法能否缩小这一差距。

扩展与复合Carina的拉马努金类比非常直接。更好的证明 → 更好的Lean生成 → 更好的RL。更强的信号意味着更高的样本效率和更高的最大性能。太好了！

扩展也很清楚：一旦我在Lean中证明了某件事，输出的质量基本上与来自人类的一样高，因此我的高质量训练集以非正式生成语料库无法做到的方式增长。我可以信任我的Lean证明。复合也很清楚：现在所有未来的推理和训练都可以建立在这些证明之上。

另一方面，在RL期间仅使用GRPO等统计信号训练的模型缺乏使用形式验证的系统所能受益的样本效率、最大性能和复合语料库。所有道路都通向验证尽管有西兰花和税收，验证已经出现在我们的许多对话中。

在物理系统领域，回想Applied Intuition：“我认为[可验证性]可能是目前最难的问题，因为随着模型变得更好，发现系统故障会越来越困难。

因此，进行适当评估以发现这些故障的问题也随着模型变得更好而越来越难。”在理论物理学中，我们回忆起Alex Lupsasca：“……现在我们处于这样一个状态，你可以让ChatGPT同时处理数千个问题，它会返回其中很大一部分的证明。

现在实际上，验证所有输出的责任又回到了人类身上。所以，是的，随着这成为瓶颈，我认为形式化数学和自动化验证将变得更有价值。”事实上，验证是科学AI与计算AI之间的关键区别：在科学中，你必须通过进行物理实验来实际测试（验证）你的假设。

像Radical AI和Lila这样的实验室在环系统正是围绕这一前提构建的（我们已与这两个团队录制了节目，即将发布！）是的，随着运行关键系统（如飞行控制、核电站和起搏器）的软件和硬件变得更加复杂，形式验证这些系统正日益成为焦点。

Carina坚信AGI需要验证生成，以至于她毫无保留地声称：“我们不相信还有其他可能的未来。”生产成本高，验证成本低Lean证明很难生成，但可以很容易地显示其正确或错误。但你怎么知道你创建的证明正确地映射到了你关心的问题上呢？

正如Carina所说：“任何可以指定的东西都可以被证明。人类不擅长指定我们想要的一切。”我们现在是否进入了规格说明业务？

请观看本期节目，了解Carina的观点，以及：为什么硬件验证是杀手级应用关于AXLE开放API和最近发布的Discovery工具包的详细信息Erdos的失败OpenAI GPT-f的离散完整视频播客时间戳：0:00 简介：2亿美元A轮融资与数学初创公司论文4:

52 验证AI：扩展辉煌，而非修复缺陷13:42 Axiom的系统：Lean数据、RL与普特南满分22:12 数学发现——猜想之前25:12 莱斯定理、不完备性与实际限制30:42 带证明的代码——Verina基准37:57 证明树、上下文窗口与扩展限制43:57 市场、

护城河与商业案例（16亿美元估值）55:27 个人起源故事：牛津、UCL盖茨比、斯坦福法学院1:00:57 Erdos争议