🔬超越非正式人工智能的扩展——卡琳娜·洪，Axiom Math

2025年，成立仅七个月的初创公司Axiom在著名的普特南本科数学考试中解决了全部12道题（在规定时间内获得8/12分，但最终得分12/12）。这一成绩超过了最优秀的本科生（110/120）和此前报告成绩的AI系统（DeepSeek 103/120），尽管尚不清楚如果给予更多时间，人类或其他系统会得到多少分。尽管如此，普特南考试以其难度著称，中位数分数通常为0或1分。这一成就似乎只是AI在精英竞赛中战胜人类的一系列成就之一，始于深蓝击败卡斯帕罗夫。

然而，到2026年中期，Claude Code和Codex正在改变世界。2024年，Anthropic押注代码和企业看起来是更务实的利基策略，而OpenAI拥有更好的模型和庞大的消费者规模。如今，Anthropic CEO Amodei全力押注通过代码加速（图像和视频靠边站）似乎具有先见之明。

尽管Anthropic势头增长，但Axiom CEO卡琳娜·洪认为编码能力是通往AGI的必要但非充分里程碑。代码可以说是将前沿推至某些编码领域之外的超级智能，但存在令人惊讶的差距，卡琳娜认为这些差距将成为AI进步的瓶颈。

非正式瓶颈

“验证性AI”听起来像吃西兰花和纳税，但对Axiom而言意义不同。“验证对我来说是关于扩展才华，复合才华，”卡琳娜告诉我们。

我花了一些时间才理解她的意思（听起来像营销话术，直到恍然大悟）。卡琳娜以传奇数学家斯里尼瓦瑟·拉马努金（《知无涯者》的主人公）为例说明这一点。当G.H.哈代最终说服拉马努金正式证明定理而非依赖他强大的直觉时，据说这提升了他自己的能力。这大概是因为正式证明迫使拉马努金以开放新思路的方式阐述细节。这就是数学中的“复合”——建立在坚实而非摇摇欲坠的基础上，也称为公理。

但正式证明也让其他人受益于他的直觉：证明是传达直觉并说服他人直觉正确的方式。这就是扩展（更多人使用结果）和复合（人们可以学习并基于他的工作）。

这就是理解Axiom方法的核心洞察。

验证生成

验证性AI以两种方式出现：训练和推理。

但快速绕道：大致来说，“形式验证”意味着使用类型检查器（如TypeScript、C++或Rust类型检查器的更强大版本）来验证使用Lean语言精心指定的数学证明。将“非正式”证明转化为Lean证明需要大量工作。Axiom本人开源了开创性工作AXLE——他们的交互式Lean应用工具包，用于探索、验证和操作数学证明。

可以想象这在强化学习中非常有用：不像基于统计学的最佳猜测（GRPO、RLHF等），你可以使用Lean验证器直接验证证明是否正确。这显然是一个更强的奖励信号，类似于编译代码并测试（通常用于编码的RL）。

问题是：LLM目前不擅长用Lean证明。

Axiom出场：虽然他们尚未正式报告除12/12普特南结果之外的基准测试，但卡琳娜报告他们在Verina代码生成基准测试中取得了令人印象深刻的99%（187/189）的ProofGen分数。该基准测试要求生成代码和正确性证明。作为对比，OpenAI o3（已知的最后一次OpenAI运行）仅达到4.9%。

基于稀疏的基准测试，很难说前沿实验室目前的表现如何，但卡琳娜表明他们仍未直接训练生成Lean证明，而是依赖非正式证明。

时间会告诉我们前沿实验室的当前方法是否能缩小这一差距。

扩展和复合

卡琳娜的拉马努金类比相当直接。更好的证明→更好的Lean生成→更好的RL。更强的信号意味着更高的样本效率和更高的最大性能。太好了！

扩展也很清楚：一旦在Lean中证明了某些东西，输出的质量基本上与人类一样高，因此高质量训练集以非正式展开语料库无法做到的方式增长。我可以信任我的Lean证明。

复合也很清楚：所有未来的推理和训练都可以基于这些证明。

另一方面，仅使用GRPO等统计信号训练的模型在RL期间缺乏样本效率、最大性能和复合语料库，而使用形式验证的系统则受益。

所有道路都通向验证

尽管像吃西兰花和纳税，验证在我们许多对话中出现。在物理系统领域，回想Applied Intuition：

“我认为[可验证性]可能是目前最困难的问题，因为随着模型越来越好，发现系统故障变得越来越困难。因此，进行适当评估以发现这些故障的问题也随着模型能力的提高而变得越来越难。”

在理论物理学中，回想Alex Lupsasca：

“……现在我们处于这样一个阶段：你可以让ChatGPT同时处理数千个问题，它会返回很大一部分问题的证明。现在责任又回到了人类身上，来验证所有输出。因此，随着这成为瓶颈，我认为形式化数学和自动化验证将变得更有价值。”

事实上，验证是科学AI和计算AI的关键区别：在科学中，你必须通过物理实验来测试（验证）你的假设。像Radical AI和Lila这样的实验室在环系统正是围绕这个前提构建的（我们已录制了这两个团队的节目，很快将发布！）

是的，对关键系统（如飞行控制、核电站和心脏起搏器）进行形式验证也日益受到关注，因为运行它们的软件和硬件变得更加复杂。

卡琳娜坚信AGI需要验证生成，以至于她无条件地宣称：“我们认为没有其他可能的未来。”

生成成本高，验证成本低

Lean证明很难生成，但可以很容易地显示是否正确。但你如何知道你创建的证明正确映射到了你关心的问题？正如卡琳娜所言：“任何可以指定的事物都可以被证明。人类不擅长指定我们想要的一切。”

我们是否现在进入了指定业务？查看节目以了解卡琳娜的观点，以及：

为什么硬件验证是一个杀手级应用

AXLE开放API和最近发布的Discovery工具包的详细信息

Erdos丑闻

OpenAI GPT-f离散

完整视频播客

时间戳：

0:00 介绍：2亿美元A轮融资和数学初创论点

4:52 验证性AI：扩展才华，而非修复低劣

13:42 Axiom系统：Lean数据、RL和普特南满分

22:12 数学发现——在猜想之前

25:12 Rice定理、不完备性和实际限制

30:42 带证明的代码——Verina基准测试

37:57 证明树、上下文窗口和扩展限制

43:57 市场、护城河和商业案例（16亿美元估值）

55:27 个人起源故事：牛津、UCL盖茨比、斯坦福法学院

1:00:57 Erdos争议和搜索的难度

1:06:02 数学的AlphaZero、自我改进

1:08:47 初创公司优势和OpenAI GPTF线程

1:13:17 Axle API——规模级Lean开放基础设施

1:20:47 协作、Polymath和人类注意力作为瓶颈

1:22:21 创始故事——痴迷、法学院和Julie Zhuo

1:26:17 更大愿景——AGI、科学和迁移学习

1:35:02 瓶颈、碎片化和领域未来