Scaling Past Informal AI - Carina Hong, Axiom Math
Latent Space · 2026-06-03
Axiom Math 的创始人 Karina Hong 用 2 亿美元融资证明：形式化验证不是 AI 的“合规成本”，而是让 AI 推理能力规模化、复合化的“性能放大器”，其真正市场是所有 AI 生成的代码。
这期内容适合所有关注 AI 推理能力、AI 安全、以及 AI 如何从“聊天”走向“可靠执行”的从业者。值得花时间看，因为它直接挑战了“形式化验证=慢、贵、麻烦”的普遍认知，并提出了一个极具颠覆性的观点：验证不是为了消除幻觉（lousiness），而是为了放大智能（brilliance）。最值得注意的冲突在于，当所有前沿实验室都在卷更大模型、更多数据时，Axiom 用更少的算力和数据，在普特南数学竞赛中击败了所有 LLM 和人类，证明了“结构化数据+验证”这条路径的威力。
这期播客深入探讨了 Axiom Math 这家 AI 数学初创公司的核心理念、技术路径和商业愿景。创始人 Karina Hong 解释了为什么他们选择“形式化验证”这个看似古老且小众的领域作为切入点，以及他们如何将 Lean（一种形式化证明语言）作为 AI 推理的“黄金数据源”。她将 Axiom 的路径与 Anthropic 早期押注“编码”进行类比，认为“数学”和“形式化验证”同样是一个看似垂直、实则能横向迁移到所有推理场景的入口。节目还讨论了形式化验证的局限性（如哥德尔不完备定理、规范制定难题）、AI 数学发现工具（如自动生成猜想），以及未来 AI 生成代码的“验证即服务”模式。
- 形式化验证 ≠ 合规成本，而是性能放大器：这是 Karina 最核心的论点。她认为，人们通常把形式化验证看作一种“痛苦”的合规要求（如航天、金融领域），但 Axiom 将其视为“规模化智能”的工具。就像拉马努金学会写证明后，他的直觉才变成了可被后人继承的定理，验证让 AI 的“天才”变得可靠、可复用、可叠加。
- 数学是 AI 推理的“编码”时刻：她将 Axiom 的路径类比为 Anthropic 早期押注“编码”。当时大家以为编码只是一个垂直应用，但后来发现编码能力通过迁移学习，成为了通用推理能力的基础。Axiom 认为，数学（尤其是形式化数学）是更结构化、更纯净的推理数据，其训练出的“推理引擎”将同样具有强大的横向迁移能力，能应用于代码验证、复杂系统设计等。
- “验证生成”比“后验验证”更强大：Axiom 的目标不是等别人写完代码再去验证，而是在生成代码的同时就生成对应的形式化证明。这被称为“验证生成”（Verified Generation）。在 Code-Marena 基准测试中，他们的系统能以 99% 的成功率同时生成代码和证明，这比先写代码再找 bug 的效率高得多。
- “规范”问题是形式化验证的真正瓶颈：Karina 坦诚，形式化验证最大的挑战不是证明本身，而是“规范”（Specification）。你无法证明一个你没有明确定义的东西。例如，你无法形式化地证明一个“安全的金融审计”是什么。因此，未来的方向可能是 AI 通过“猜想”和“测试”来帮助人类完善规范，然后由形式化验证器来证明。
- 注意力是稀缺资源，人类的“品味”依然重要：当 AI 能生成海量、冗长的形式化证明时，人类数学家不会消失，但他们的角色会转变。他们不再需要验证每一个步骤，而是需要运用“品味”和“直觉”来判断哪个猜想值得被证明、哪个证明路径更优雅。这就像资深程序员不需要懂汇编，但需要具备系统级的设计眼光。
验证不是为了消除 AI 的“低级错误”，而是为了放大 AI 的“高级智慧”，让它的每一次推理都能成为下一轮推理的可靠基石。
这对 AI 从业者，尤其是做 Agent、代码生成或安全对齐的团队，有两点非常具体的启发：
- 重新定义“数据质量”：大家都在追求海量数据，但 Axiom 证明了“结构化、可验证的数据”比“海量、无结构的数据”在特定推理任务上效率高得多。对于做 AI 产品的团队，这意味着可以思考：在你的领域里，是否存在类似“Lean 代码”这样的“黄金数据”？例如，对于代码 Agent，能否将用户反馈、单元测试结果、代码评审记录等转化为一种“半形式化”的训练信号，而不是简单地用 RLHF 去拟合人类偏好？
- “验证”是 Agent 系统的核心基础设施：当前 Agent 的最大问题是“不可靠”。Axiom 的路径提供了一个清晰的蓝图：未来的 Agent 系统应该内建一个“验证层”。这个验证层不一定是 Lean，但可以是任何能提供“确定性保证”的模块（如类型系统、形式化规范、数学证明）。当 Agent 生成一个计划或一段代码时，系统不是直接执行，而是先通过这个验证层进行“编译”。编译通过，则执行；编译失败，则回溯。这比单纯依赖 LLM 的“自我反思”要可靠得多，因为它引入了外部、非神经网络的确定性约束。
