她筹集6400万美元，打造AI数学神童｜Axiom CEO Carina Hong

摘要

• Axiom押注6400万美元，认为可靠推理需要把生成与验证放进同一个自我改进闭环，而不只是训练一个更大的非形式化模型。 Hong 的架构由定理证明器、猜想生成器、共享知识库和自动形式化层组成，用 Lean 将概率搜索与确定性检查结合起来：「证明就是证明」（A proof is a proof）。

• Axiom早期最强的技术信号，是在Putnam 2026考试时限内解出12道题中的8道，并在Hong首次发帖两小时后又报告解出第9道，最终得分仍待确认。 9道将追平前一年约4000名人类参赛者中的最高分，并大致达到Putnam Fellow水平；而「中位数分数基本就是0分」。Hong本人得了4道，还开玩笑说要办一场「击败Carina」派对。

• 商业切入口在验证劳动：硬件设计团队的规模可能只有验证团队的1/3或1/4，验证本身可能耗时3年；Hong认为AWS曾花5年时间，才把一个hypervisor内存隔离组件形式化。 Axiom瞄准芯片验证、安全关键代码审查、遗留代码等价性和数据库一致性——这些场景的客户「只希望它不要出错」。

• Axiom并不认为每个程序都应该、或都能够进行形式化验证；Hong把市场分为关键系统、「有了更好」的场景，以及低风险的vibe-coded应用。 Lovable生成的网站「未必需要形式化验证」；她也承认「不可能验证Python里的所有代码」，但认为其中相当一部分仍可能覆盖。更难的产品问题，或许不是检查最终证明，而是在存在歧义时形式化正确的规格说明。

• Hong预计数学不会消失，而是转向更高层次的抽象：顶尖研究者提供直觉，AI则成为「勤勉的研究生或博士后」，负责证明想法、构造例子并否定错误猜想。 Biewald追问机器最终可能超过人类直觉；她回答说会是「不同的直觉」，并认为要追上最顶尖的0.00001%数学家仍需很长时间。Axiom在P versus NP或黎曼猜想上「还没到那个阶段」。

• 这笔6400万美元融资，为一家成立约6个月、称自己「还在第0天」、仍与可信合作伙伴进行早期沟通的公司提供了发展空间。 Hong希望Axiom在面对大型现有企业时「始终保持不适」，保留她在地下中国摇滚乐队身上看到的、商业化之前那种「小而强悍」的饥饿感。技术里程碑很亮眼；接下来真正的考验是商业化，以及规格说明能否被用户真正使用。

精读

1. Axiom把验证纳入推理闭环

• Hong将Axiom定义为「能够自我改进的推理引擎」，因为它把生成与验证耦合在一起。数学是最初的试验场：证明提供了异常清晰的正确性信号，也能暴露纯统计系统中容易蒙混过关的手搓式论证。

• 这套架构包括证明器、猜想生成器和共享知识库。证明器检索既有结果；猜想生成器利用反例在提出想法前淘汰薄弱方案；自动形式化层则把自然语言数学连接到这3个组件。

• Lean让自然语言模型接受确定性检查，形成Hong所说的「确定性工具与概率系统协同工作的力量」。在Erdős问题481的演示中，系统将论证拆成一张证明图，随着子目标被验证，节点逐一变绿；每个节点都能展开Lean代码，再翻译回自然语言。

2. Putnam成绩提供Axiom首个重大能力信号

• Biewald先把基准摆出来：Putnam是一项极难的本科数学竞赛，参赛者是数学能力很强的学生，而「中位数分数基本就是0分」。哪怕做对1道题都有意义，站到最前列则是性质完全不同的结果。

• 在Putnam 2026的考试时限内，Axiom解出12道题中的8道。Hong最初发帖两小时后，公司又报告解出第9道，形成一次尴尬的更正；公司仍计划发布证明和最终准确得分，而不是把临时计数当成定论。

• Hong表示，9/12将追平前一年约4000名人类参赛者中的第1名成绩，通常对应Putnam Fellow、也就是前5名左右的水平——当然，前提是当年题目没有异常简单。她本人拿到4/12，获得前250名的荣誉提名，因此Axiom最终得分「有可能是我的3倍」。

• Biewald提出了一个有用的反例：普通GPT或Gemini在奥赛题上可能表现惊艳，却会栽在简单脑筋急转弯上，说明机器的难度曲线并不遵循人类的能力排序。Hong的回答是模块化分工：形式化工具擅长细粒度检查，非形式化推理器贡献高层直觉，专用工具负责计算。

3. 形式化证明把信任变成机械属性

• Hong回忆，2024年12月，团队曾讨论由「o1 Pro或o3 Pro——我忘了」生成的Putnam解答，随后又出现o3 Preview。不同人类阅卷者给出了差异很大的分数，最终共识是每份答案都存在一个关键漏洞，只是被模型用手搓式论证带过了。「形式化系统的力量」在于，这类缺口无法蒙混过关。

• 这种严谨有时显得过度。在分析题中，Axiom可能围绕收敛、极限或一个简单的正性引理生成大量Lean代码——数学家通常会很快处理掉这些细节。Hong称之为「几乎有点烦人」，但最重的证明节点也可能正是提供最强确定性的节点。

• Biewald问，如果AI能生成一份1万行的证明，所有人都能逐步接受，却没有人凭直觉真正理解，会怎样？Hong指出，人类那些晦涩的证明本来也需要专家组审查；在删去机器多余的步骤后，她认为有效证明「可能会收敛到人类有可能找到的形式」，让AI成为另一位合作者，而不是低人一等的数学家。

• 他们以Putnam A3为例，展示了重合与分歧。在Alice和Bob的字符串博弈中，Axiom与人类得出了同一个简洁结论：Bob总能获胜，因为他的策略几乎不需要分支。其他时候，机器可能会暴力搜索一条人类会避开的路径，或找到一份不同于Axiom数学家预期的证明。

• Hong还提到更早的AlphaProof系统，称其为一个「IMO时刻」：她说AlphaProof拿到28分，距离29分的金牌线只差1分，除组合题外解决了所有问题。她将其与2025年IMO对比：许多选手拿到35分，却漏掉唯一的组合题。对她而言，这个例子再次说明，形式化系统与非形式化系统的结合有多重要。

4. 验证劳动构成初始企业切入口

• Hong的经济学论据从供需失衡开始：硬件设计团队的规模可能只有验证团队的1/3或1/4，而验证可能耗时3年。她认为AWS的自动推理团队曾花5年时间，只为将hypervisor的内存隔离组件形式化——「这个数字很惊人」，而且还不是整个系统。

• 潜在应用包括审查智能体生成的代码、证明安全关键部署中的边界情况、确认迁移后的代码与遗留代码等价、降低对稀缺形式化验证专家的依赖，以及检查恶意数据库参与者存在时的一致性。Axiom成立约6个月，结束隐身并融资6400万美元后，仍在与可信合作伙伴进行早期沟通，没有宣称已经广泛部署。

• Hong提出的更激进案例，是把生成与验证统一起来：先用Lean将Paxos一致性证明自动形式化，再根据该规格说明，用Rust等强类型语言生成实现。商业价值不只是找出bug，而是让实现与正确性从同一个产物中共同生成。

5. 形式化方法仍受制于规格说明上限

• Biewald的质疑是，软件正确性很少像定理那样非黑即白。数据库市场部分拥抱NoSQL，正是因为放宽一致性约束可以提升运行效率、存储用户数据并使其可查询；许多应用能够接受权衡，因此绝对证明的价值可能没有Hong的数学类比那么高。

• Hong将市场分成3个层级：监管要求或部署风险使验证不可或缺的系统；数据库一致性等如果不影响可用性、则非常值得验证的场景；以及不需要验证的应用。「Lovable生成的网站未必需要形式化验证」，Hong还说，她正在构建的AI数学家不会写诗。

• 因此，自动形式化是核心技术，而不只是数据生成技巧。把证明转成Lean后，可以获得检查器反馈；但形式化陈述本身更难，因为这时解决方案还不存在。在代码领域，输入输出测试可以部分锚定预期规格，但系统仍必须在不向用户抛出500个偏好问题的情况下解决歧义。

• Hong接受了Biewald提出的边界：「不可能验证Python里的所有代码」，但她认为其中多数可能仍具备可处理性。Biewald提到推理模型、更强的代码生成、可验证领域中的强化学习，以及不断扩大的Lean采用率；Hong表示，这3项发展正在汇合，使现在成为一个特别合适的时点。她还提到正在开发的CSLib，以及由Clark Barrett领导、获得DeepMind和AWS支持的Stanford Automated Reasoning Group；这些努力都在推动用Lean形式化本科计算机科学和机器学习。

6. 数学家从证明劳动上移到发现

• Hong预计数学会继续存在，但数学家「将学会在不同的抽象层次上工作」。她将这一转变类比为采用LaTeX，并指出计算机代数早已在辅助计算型研究；新工具将进一步移除逐一检查技术引理的手工劳动。

• 理想的分工是，让Terence Tao这样的数学家跟随直觉，而AI扮演「勤勉的研究生或博士后」。关键在于，发现还需要构造例子、识别模式、制造反例、提出猜想，并不断向闭环输入更多猜想和证明，而不只是解决一个固定定理。

• Biewald进一步追问替代问题：为什么认定机器不会发展出更好的直觉，甚至不会判断什么值得人类感兴趣？Hong的回答是「不同的直觉」，其基础在于机器与人的难度曲线不同；她认为，机器要达到人类数学直觉最顶尖的0.00001%，还需要很长时间。

• 替代冲击会因数学风格而异。在不需要深层理论的领域，解题型数学家可能比理论构建者更早遭遇AI替代；后者负责连接文献、开辟新领域。Axiom在P versus NP或黎曼猜想上「还没到那个阶段」，但这次出乎意料的Putnam成绩，已经在压缩理论构建者对自身时间线的预测。

7. Hong想打造带有逆袭文化的学术引擎

• Hong将自己的创始人气质追溯到5岁起聆听带有政治反叛色彩的中国地下摇滚。她从未觉得自己是「最学院派的学院派」或「最创业者的创业者」；但运营Axiom让她感觉「如鱼得水」，仿佛「每天都在过摇滚时代」。

• 团队的3根支柱——AI、编程语言和数学——也横跨芯片设计、代码验证、编译器与数学发现。Hong表示，发现研究者与形式化证明专家之间的对话，正在重塑团队对自我改进的理解；公司因此「更像学术界」，因为它不断拉伸她的智力边界。

• 她对公司文化的比喻来自一些乐队：贫困时期写下的、充满饥饿感的早期歌曲，明显好于后来创作的作品。因此，Axiom试图「始终保持不适」，意识到大型现有企业的存在以及自己的起步较晚，同时保留逆袭心态、「像孩子一样的好奇心」和小而强悍的文化。她将这一阶段比作研究生院——数学家有时会在那里产出自己最好的作品。