夜雨聆风当AI拿下普特南数学竞赛满分、在代码领域横扫千军时，我们离通用人工智能（AGI）还有多远？Axiom Math的CEO Carina Hong给出了反常识的答案：还差一场彻底的验证革命。
本期来自AI工程师播客《Latent Space》，对话2亿融资的Axiom Math创始人Carina Hong。
普特南满分只是起点：AI的真正瓶颈在“验证”
普特南数学竞赛被称为“世界最难的数学考试”，中位数得分常年在0到1分之间。2025年，成立仅7个月的Axiom Math拿下了全部12道题的满分，远超DeepSeek的103分和人类顶尖选手的110分。
但在Carina Hong看来，这个成绩只是AI能力的初步展示，而非真正的突破。她认为，当前AI的最大瓶颈，不是解决幻觉或准确率问题，而是“验证不是补AI的漏洞，而是放大人类与AI的卓越推理能力”。
Carina用传奇数学家拉马努金的故事打了比方：这位靠直觉写出数千条定理的天才，在G.H. Hardy的敦促下开始形式化证明自己的结论。不仅自己的推理能力得到了系统性提升，更让他的成果能被其他数学家传承和复用。“验证对我来说，是放大才华、复合才华的过程。”她解释道。这正是Axiom定义的“验证式AI”：不是为了合规或纠错，而是为了让人类和AI的卓越推理能力实现规模化扩散。
Lean工具链：让严谨证明成为AI的标配
要理解验证式AI的落地路径，绕不开形式化验证工具Lean。简单来说，Lean是基于Curry-Howard对应关系的编程语言和证明检查器，数学证明和程序代码本质上是同一套逻辑，代码编译通过即可证明结论绝对正确。当前主流的LLM还不擅长直接生成Lean形式化证明，大多依赖非正式的推理过程。
Axiom的核心突破之一，就是解决了这个痛点。你能想象吗？未来AI写的代码或数学证明，能像普通程序编译一样，一次性通过严格校验？Carina透露，团队在Verina基准测试中拿下了187/189的99%正确率，这个测试要求AI生成带正确性证明的代码，而OpenAI o3的成绩仅为4.9%。 “Axiom在Verina基准测试中拿下187/189的99%正确率，远超OpenAI o3的4.9%”。
和头部AI实验室的路径不同，Axiom直接训练模型生成Lean形式化证明，而非依赖非正式的推理。这意味着，AI的输出不再是“大概率正确”的猜测，而是能被机器直接校验的严谨结论。
验证式AI的双重价值：规模化与能力复合
验证式AI的价值，体现在训练和推理两个层面。在训练阶段，形式化验证可以提供强奖励信号，替代依赖统计的RLHF或GRPO方法，让模型的学习效率大幅提升。在推理阶段，经过验证的成果可以成为可复用的知识库，让后续的AI和人类研究者站在巨人的肩膀上。
Carina用“规模化”和“复合”两个词总结了这种价值：“只有经过形式化验证的成果，才能真正成为人类协作的基础。”这意味着，AI不再是单次任务的临时工具，而是能和人类共同构建可传承、可迭代的知识网络。
反观仅依赖非正式训练的AI模型，它们虽然能在单次任务中表现出色，但无法形成可积累的知识体系，也无法实现真正的能力复合。这正是当前主流AI路径的核心局限：再强的通用模型，也只是在做统计拟合，而非严谨推理。
商业化落地：从数学到硬件的万亿级场景
验证式AI的商业化前景，早已超出了数学领域。当前硬件验证的人力成本占芯片研发总成本的70%，航空、核电、起搏器等关键系统的软件验证，更是依赖耗时数年的人工评审。 “硬件验证的人力成本占芯片研发总成本的70%，形式化AI能彻底改变这个格局”。
Axiom已经推出了针对Lean的元编程工具集Axle，开放给社区免费使用，搭配Claude Code可以大幅简化Lean开发流程。团队还即将开源Discovery toolkit，帮助数学家在正式证明前完成直觉探索，比如生成测试案例、推导猜想。
Carina在播客中提到，和OpenAI、Anthropic等头部实验室的路径不同，Axiom专注于打造验证层，为通用AI模型提供严谨的推理底座。“我们不认为有其他路径能通向真正的AGI。”她给出了这个斩钉截铁的判断。无论是企业级高可靠代码开发，还是前沿科学研究，验证式AI都将成为未来的核心基础设施。
跨界初心：从神经科学到形式化AI的创业逻辑
Carina的创业背景本身就充满跨界逻辑。她曾在牛津大学攻读神经科学硕士，在UCL Gatsby计算神经科学研究所接触前沿AI研究，之后在斯坦福数学博士项目前，特意花了一年时间攻读法学学位。
她发现，法律领域的逻辑推导和数学推理有着共通的本质，而当前的AI恰恰缺乏这种严谨的逻辑链条。“我相信，只有建立在严谨验证之上的AI，才能真正实现通用智能的突破。”她说道。
这份跨界的视角，也让Axiom的产品设计跳出了纯技术的局限，兼顾了科研和商业化的双重需求。既可以服务于数学家的严谨证明需求，也能适配工业界对高可靠系统的落地要求。
结语
这期播客打破了我们对AI竞赛成绩的迷信，告诉我们真正的AGI不是靠刷竞赛题，而是靠建立一套能规模化、可复合的严谨推理体系。从拉马努金的故事到Lean工具链，从数学竞赛到硬件验证，Carina为我们勾勒了一条通往通用智能的全新路径。
无论是AI工程师、科研人员，还是对通用人工智能抱有好奇的读者，都能从这期内容中看到AI发展的另一种可能性。觉得有收获，欢迎点赞、在看或转发给身边关注AI前沿的朋友。