Carina Hong（Axiom）——数学 AI 的前沿【完整演讲】

很高兴见到你。

知道，那是门非常有名的课。

我记得大概是十一月，那时我刚开始读数学博士。我已经看 AI for Math 的论文两个月左右了，大概从九月、十月到十一月，我对这个领域特别感兴趣。我觉得 AI for Math 会改变世界。GitHub 上有个收集了几百篇论文的仓库，我就先读摘要；摘要够有意思，我再去读全文。后来我意识到，自己上课时也只顾着在笔记本电脑上看这些论文，这就有点说不过去了。

后来我参加了一场 Knight-Hennessy 午餐会。演讲者 Julia Zhu——我记得她好像是 Facebook 最早的产品经理——讲到她写书的经历：她只是开始写，结果就停不下来。我当时问她，我也有类似的困扰，她就说：“跟着你的热情走，看看它会把你带到哪里。”于是我很快就开始筹款了。

抱歉，我今天有点不舒服。

谢谢。我开始筹款后，大概过了一个学期，就决定该退学了。

Axiom 做的是形式化数学推理：把数学转成机器可以检查的代码。这很有价值，因为 AI 正在生成大量内容，却缺少一层验证。昨天我们宣布，已经把有限单群分类定理形式化了。这个定理是人类写过的最大数学证明；没有别的证明比它更长。它太庞大，以至于没有任何一个人读完过。它汇集了几代人的 20 世纪数学成果。简单群的概念最早可以追溯到伽罗瓦；到了 19 世纪，有人提出家族里可能还包括五个左右的散在群；大约在 20 世纪 50 年代，布劳尔在著名的国际数学家大会上发起了分类所有有限单群的工作。整个证明超过 1.5 万页，散落在许多论文和书籍里。

我们的使命，是把大量数学成果，也包括其他领域的内容，转成机器可检查的代码。运行程序时，你就能确认它是正确的，达到百分之百验证。严格说，哥德尔会告诉你，任何东西都不可能让人真正确信；但这里是把庞大的证明归约到一个很小、可信的内核。因此它的正确性可以说“排除了合理怀疑”，除非发生非常重大的理论问题。最终，这个证明被写成了 Lean 程序语言里的五千多万行代码。

从商业角度看，这也很有意思：它是最大的开源软件项目，比 Linux 还大，也超过你能想到的其他开源项目。它用 Lean 这门编程语言表达的，其实就是一个定理、一个特别庞大的证明。昨天不少数学家说，他们觉得压在自己毕生工作和学术遗产上方的一团阴云终于散去了。

我想，首先是因为这件事以前从没人做成过。新兴技术总让人兴奋。关键是有了验证层之后，事情就不再只是“我有一段代码，请告诉我它对不对”，而是我可以生成新代码，立刻得到验证反馈。我觉得这会成为 AI 辅助编程的未来。

我想是这样。现在大家其实不太信任测试。你看看新闻里的国家关键基础设施：铁路停摆，或者波音 737 因为严重软件漏洞不得不返航。这些系统都经过测试了。现在代码审查的力度，已经降到了历史最低点……

……实际上很多 AI 原生公司根本不做代码审查。我知道自己公司有些部分也没有代码审查，代码就这样上线了。我觉得这会带来问题；问题严重到一定程度，就会让 AI 部署整个停下来。所以这里大致有三层价值。第一层是技术直接创造的价值，主要是生成经过验证的代码，也有一部分是验证现有代码；虽然这部分听起来较小，其实也不小。第二层，是让更多机构愿意在市场规模很大、又很关键的领域部署 AI。让 AI 得以部署，本身就有价值。

第三层，如果你关心自动化研究，那就是 AI for Science：让智能体自主开展长周期的发现工作。这和经过验证的代码生成有相似之处，但更有意思的是，你可以让系统去处理数据。我觉得这会把 AI 从现有的信息提取和交换领域，带到物理世界，也带到材料科学、新分子等领域。第三层就是走出软件，进入物理世界——不只是硬件，而是更广泛的科学。

我第一轮融资时 CTO 加入了，所以确实分担了很多压力。

我觉得第一轮种子融资，核心是“AI 将改变数学”这个想法。当时也有其他公司在做形式化推理，但我们在技术路线和愿景上投入了很多思考。我们当时就很确定，不会采用单体式的训练搜索方法，而会把搜索放在推理阶段；后来事实证明这是正确的选择，其他很厉害的团队也采取了类似方向。

第二轮融资更多是因为我们看到了迁移学习的能力。我们做出的形式化数学证明器，在其他软件验证基准上也拿到了很高、很出色的成绩，这让我们自己都很意外。Putnam 数学竞赛的成绩也达到了满分。我觉得这说明它不只是会被“苦涩的教训”压过去；但要始终走在前沿，仍然是一场持续的较量。

第一轮非常难，毕竟那时只有一个想法，我的融资幻灯片可能做得很糟。第二轮时有些东西变了：我把注意力集中在把公司建起来。

当你专心建设公司，就不会把太多精力耗在融资流程上，结果反而挺顺利。若一门心思只想着融资，可能会想太多，把流程拖长。后来我就专注于把公司做好……

……我觉得等我专心把公司建起来之后，融资就容易多了。

第二轮时，我基本上想的是：我们种子轮融来的钱还没怎么花，没必要再融资。与此同时，很多风投对我们很感兴趣，有些主动找上门，有些直接发了条款清单，所以我们拿到了“抢先投资”（preemptive offer）。如果没有人抢先出价，通常就得一家家去敲门；有了抢先报价，就像是已经有个很诱人的条件摆在面前，而且我确实有兴趣接受。那我们就可以约定一个期限，免得流程拖个没完，导致其他报价也可能失效。所以如果这是一堂创业融资课，我觉得一个好建议就是：尽量拿到抢先报价。

是自然发生的。我大概看到了苗头，也试着促成它，因为在我们达到那个里程碑之前，就有人表现出想提前投资的兴趣。我当时觉得，在里程碑即将到来时就接受报价不一定是好事。首先，融资非常分心；其次，等一等，你可能会获得更多投资人的兴趣。

被拒绝并不是世界末日。我觉得这是特别重要的一课。很多事情当下看起来很糟。创业是给敢于冒险的人做的。我也一直很敬佩那些公司最后没做成的创始人，因为一家公司为什么成功、另一家为什么失败，未必有很多清晰的理由；执行本身就有很大的随机性。每天都会遇到事情特别不顺的低谷期，融资时被拒绝很多，这种感受会被放大。

第一轮融资时，我的做法确实有变化：我意识到自己没必要在这一座山上拼到死——这件事不是我唯一想要的结果。我退一步看，市场上还有很多很好的风投机构。想通之后，压力小了很多，人也更放松、更自在；而且我觉得，这也传递出一种信号：公司很有价值。这种信心是由内而来的。所以这是一点。相反，绝望对融资过程没什么帮助。

这是个很好的问题。AI 变化太快了，所以设定目标时，不能只设一个下季度要实现的雄心勃勃的目标，而要设定未来一年的目标。否则就会落后于趋势，因为前沿进展更新得非常快。我记得三月时，我们还在问：能不能形式化“素数间有界间隔”这个结果？这是个很漂亮的结果，它说的是……

……有无穷多对素数，它们之间的差不会超过某个有限值，而这个有限值一直在被压低。要是降到 2，就证明了孪生素数猜想，那就恭喜了。2013 年，张益唐第一次证明这个差值有一个有限上界，当时是 7000 万。2014 年的纪录到了 246，后来一位数学家又把它推进到 240。那是很近的事，我们甚至和她经历了一场时间紧迫的竞赛。可是当我们想把 2014 年这个 246 的结果形式化时，公司里大多数人都认为做不到：工作量实在太大，他们不想定下这个目标。我们只能说，最终总得做点什么、真正留下些成果。我从中得到的一个重要启发是，目标要定得有野心。后来大家已经觉得，形式化素数间有界间隔是理所当然能做到的事。

第二点听起来有些矛盾：你既要什么都想自己做，又要能放手采用别人的东西。我们采取全栈路线：自己收集和管理大型数据集，不依赖数据供应商；自己制定数据策略；有模型训练团队，负责密集的中训练和后训练；我们自己构建 harness、运行基础设施和版本控制。几乎整个技术栈都不外包，唯一没做的是预训练。这就是我们全栈野心的规模。

但这样做的好处是，我们也得准备好接受现实：技术栈有些环节会被别人超过，所以需要时用别人的方案也没关系。你得广泛撒网。今天你可能不在前沿，但九个月后也许就能赶上。像 Harvey 这样的公司也在讲，他们先把收入做到相当规模，再开始训练前沿模型。所以这不是短跑，而是马拉松。

我特别关注那些不能随着技术进步及时调整的公司。举例来说，有个新模型发布时，我们第一天就试了它的分类模型；当天晚上，数据仓库里的许多分类任务已经在用它了。我们很愿意试用别人的东西，不会因为觉得自己也能做同样的东西就产生防备心——当然我说的不是刚才那个具体例子，而是我们在其他情形里也见过这种心态。

对，而且也要聚焦。有些东西是我们的重点，比如数据。我们认为，自我改进能力来自合成生成数据。因此这类东西我们会牢牢掌握在自己手里。

我觉得是。数据和基准测试大概就是模型的定义。

这个问题我们刚才也提到了。过去的模式是硬编码一个 harness，再调用一堆专用模型。

我们认为，至少现在看到的新模式，是一个尽可能精简的 harness，加上通过智能体强化学习训练出来的协调模型。

它可以递归地调用自己，也可以调用其他硬编码工具；这些工具甚至可能更像……

……这样的工具更像是智能体。所以我们看到的方向正在变化，很多人还在为旧技术栈建设基础设施；我们觉得自己最好始终领先两步。即使能力层面落后了，你仍然有机会在基础设施层面参与竞争；但如果没领先两三步，就会陷入一种僵尸状态。

我想 DDA 有一份列出 50 家公司的“新实验室”名单，我们确实在其中。

作为 CEO，很多时候不可避免地要做人员管理。对新实验室尤其如此，因为人才密度决定了企业是什么样子。如果人才模式不成立，我觉得就会进入危险区：那时你可能就不再是新实验室，而得开始拼收入了。我的日常工作有很大一部分，是理清技术管理。这和创业初期相比已经变了。

Shubho 曾在 Facebook AI Research 工作，是那里的 IC 总监。他是个有远见的人，我特别喜欢听他谈任何事情。当时 Facebook 的情况也有些动荡，时机上确实有点机缘巧合。要让每个人融入我们在 Axiom 建起来的团队，有时我得先弄清楚他们受什么驱动。理想情况下，驱动力就是我们正在解决的技术问题。Shubho 曾研究 AI 生成单元测试的评估，他相信规模化、无限数据和大规模训练。他还是 2014 年 DeepSpeech 和 DeepVoice 论文的作者之一，所以理念很契合，这为团队打下了很好的基础。

当然，初创公司的常态就是起起落落，压力大的时候尤其如此。我们会主动沟通，而且尽量坦诚。谈到留住人才，这是我学到的一点。说实话，作为创始人最难的是，有些日子你会觉得一切都在往下掉。你想照顾好自己，也要顾着团队，确保大家都还好。学会共情、在两者间找到平衡，这并不是我在学术训练中重点学到的东西。过去总是追求更高、更快、更强——怎么让分数再提高一点，像奥林匹克竞赛一样；不一定教你如何和人真心交流。但这对创业很重要。

这是新实验室面临的独特挑战之一。另一方面，新实验室不只是要做人员管理，还得做技术管理；各种优先事项可能相互冲突，而且情况一直在变化……

……你可以有雄心勃勃的目标，但不能因此忽略风险。事实证明，负责定远大目标的人，和最擅长发现执行风险的人，几乎从来不是同一类人。如果按这两种角色来划分，基本是互不重叠的。当然，公司里定目标的人技术都很扎实，但这往往是附带的；专门标出风险的人，注意力则都放在“这可能行不通”上。

他们听起来像唱反调，但实际上不是，只是在提醒你必须听到的真实问题。有时我会想，我可以让他把话说得客气点；但他说得对。所以，关键是平衡真正的技术优先级，决定该多做还是少做，有时候少即是多。前面我讲了全栈方案，但聚焦也很重要。比如做分类或有限单群分类时，我们就只专注这件事，让所有人都朝同一个方向努力。

我觉得有三件特别重要的事，是我以前没意识到的。每条建议背后都有很多天的煎熬和反复思考，我才把它们提炼出来。第一，从自己开始，再影响别人。当我状态不好、觉得精疲力尽时，团队也会感受到那种能量，大家都会很难受。所以有时要休息，让自己的状态平静、沉着。我以前总盯着解决这个问题、那个问题，或者某个人的问题，却没意识到，很多影响最大的时刻，来自调整自己的状态，以及脑子里突然想通、变清晰。

第二，我以前很不擅长描述感受。创业之前，我当然也有情绪，只是不说出来。

现在我更会给感受命名，也会留意别人的感受。要走过很长的自我探索过程，我才学会把情绪说出来，因为人很容易筑起一道墙，总是只用理性思考。我说这是个重要诀窍，是因为如果你不谈感受，感谢之情就不会像我希望的那样经常表达出来。我也不擅长让别人放松，因为我不会说出感受。

我对团队每位成员都心怀感激。

但我不是每天都说出来。有些重要时刻大家会埋头苦干，比如有限单群分类结果发布前一晚，整个办公室都在忙，至少有一半人通宵工作。

有意思的是，我们内部的基础设施和工具非常好，所以所有事情跑得很快。后来我们意识到，到了发布的时候，理想情况下应该让外部的人能够独立验证我们的成果，对吧？但他们的基础设施……

……外部验证的选择并不理想。到了最后关头，比如晚上八点、早上七点就要发布时，我们还在通知大家：运行和交叉核验这个证明可能要花很久，甚至可能会失败，让人以为它是错的。正因为这个问题，大家才通宵工作。我后来意识到，我表达感谢的方式是给大家买一大船寿司，而不是直接说出来。有时候我就是说不出口，真的挺难的。

没错。

第三件事也挺有意思：我后来才学会，人和人有时就是很不一样。我起初做事很专注于单一目标，所以也希望大家都盯住一件事。但有些人像章鱼一样，同时把触手伸向八件事，反而状态最好。我真的学会了让这种做法发生，也看到了它的好处。现在我们的模式更像自下而上、又带点“仁慈的独裁”；以前公司规模变大时，我更强调自上而下和指挥链。

不到 15 人。

大概 80 人。

什么都帮到了，真的。

这是我在法学院学到的。我很喜欢自己在法学院读的那一年。

我喜欢，非常喜欢第一年。在数学里做证明，会训练第一性原理思维，也会训练一种非常具体的能力：高度分析。于是任何事情都会变成一道待解的题。我没法过分强调这一点在日常工作中有多重要，尤其是风险很高、压力很大的时候。我在高压的数学竞赛里仍能解题，这种能力留了下来，是非常关键的训练。

数学带给我的另一项帮助，是深入钻研、对一个问题着迷的能力。我把它叫作“心理韧性”。它不是说能扛过什么苦难，而是：我想不出来，就继续想、继续想、继续想。休息一下，到了第二天还是放不下。我觉得这对建立公司非常重要；没有这种韧性，你就会躲开最关键的问题。

脑机接口。

对。我是个大书呆子，当年就是出于这种 nerdy 的兴趣读了神经科学硕士。我想选它，首先因为它还很早期，没人真正知道应该怎么做。大家还在争论该不该采用侵入式方案，技术问题也很多；我们连神经科学都还没真正弄明白，又怎么理解脑机接口？

但我也不想选一个只是特别难、完全不知道怎么解决的问题。我希望它关系到每个人：人人都需要沟通，而沟通的延迟实在太高。我第一次用 WhisperFlow 时特别受启发，它让我打字快了很多；打字是我沟通的一种方式，而沟通在我的生活里占了很大的时间成本。

第三，它连接了过去、现在和未来。过去是 AI。（Ravi：对。）现在，我觉得脑机接口正处在一个足够早期的阶段。未来则是：如果人类之间的沟通问题解决不了，那么在 AI 时代，我们可能会遇到被彻底排除在外的风险。这就是我会选择它的原因。

创业真的很难。我觉得有一点值得说：困难并不能提前给你多少提示，它会在你最没想到的时候出现。如果你是个喜欢把事情安排好、连旅行都要计划好的人，有时候很难跨过那道心理关。它会挑最奇怪的日子袭来。很多最艰难的时刻，反而会出现在取得很好的成绩、拼搏告一段落之后。我没想到不确定的痛苦和煎熬会是这样。我原以为事情可能会很难，或者会很突然，却没想到两者会同时发生。

对。你如果是个计划型的人，这就更糟了。

有一次高中数学竞赛，我记得自己特别受打击，因为离想达到的名次就差一点。后来我回头想了想原因，也意识到那正是我最大的优势造成的——至少在那个情境里，它成了我的弱点。

那场中文数学竞赛有四道题。我一头扎进最后一题——数论，通常是最难、也是我最喜欢的题。我差点没能从那题里抽身。我很执着，这就是我说的那种心理韧性，结果整场比赛时间都花在那一道题上了。我从中学到，很多特质要看情境，有时是优点，有时是缺点。我不觉得没有这种特质就会成为今天的我，但在当时那个具体的场景里，它让我……

……当时真的让我很受打击。我想，其中一个教训是，事情可能没有那么多绝对的对错。当然，时间管理是好事，缺乏优先级也确实不好，但很多时候要看具体情境。

这样可以吗？

如果我理解得没错，Axiom Math 正在打造 AI 数学家，最终愿景是构建能够递归改进的 AI 系统。你为什么认为数学推理特别适合用来实现递归自我改进的 AI 系统？

我可能会特别强调形式化数学，也就是把数学转成机器可检查的代码。转成代码之后，就能解更多数学问题：既有“用代码做数学”，也有“用数学处理代码”。所以更准确地说，我们是一家和编程关系很紧密的公司。我们会用同一套形式化数学推理引擎和技术栈来证明软件，也证明硬件。起初我有个想法：解好数学，就能解决一切。但很多关键点都藏在细节里。更准确的说法是，你搭建的技术栈中每个部分，如今都能复用来做编程，而我觉得这会改变世界。

谢谢回答。有人说，创业之前最好先去大型实验室或大公司工作，积累训练和经验。你觉得这仍然重要吗？还是建议直接跳进深水区、放手去做？

去大型实验室工作很有价值，前提是你觉得那里能让你学习、看到前沿。我有点特殊：在形式化数学 AI 这个新领域里，学术界当时其实处在前沿。我读的都是学术论文，因为大实验室那时兴趣不大。这个方向在大实验室里大概短暂出现过一阵，也就几个季度，然后就被放下了。

所以如果你所在的是一个成熟领域，前沿实验室大概就掌握着前沿，先去那里工作会是不错的选择。这是我的建议。

可是现在 AI 发展这么快，还有时间先去前沿实验室学习，再创业吗？还是应该趁现在就开始？

我觉得有一点是，你能在很短时间里学到很多东西。这可能出乎意料：一切都在加速，学习过程也被压缩了，学习本身还会进一步提速。我觉得这样挺好。另一点是，选择一个足够难的问题；问题足够难，就能给自己留出更多缓冲时间，让自己经历完整的学习过程——从“前严格”到严格，再到“后严格”。

谢谢你今天来。我叫 Will，是数学专业的学生。我想知道你觉得未来数学家的工作会是什么样子？我现在学的技能以后还能用得上吗？

你现在学的技能将来肯定用得上。关于数学以及人类数学家未来会走向哪里，我想了很多，也和许多处于不同观点光谱上的数学家谈过。……

……数学到底更像癌症生物学，还是更像下棋？每个人都得有自己的世界观，再据此做判断。如果你觉得它更像癌症生物学，那么数学就有内在价值：解决一个问题、做出一项发现、提出一个猜想，本身就有价值。AI 会缩短这些发现走向实际应用的时间，数学就会对科学、应用科学、技术和工程领域特别有用。这是我的看法：数学更像癌症生物学，而不是下棋。

当然，也有人做数学纯粹是为了乐趣。对他们来说，数学就是下棋，我后面这些论证就不适用。如果你认同数学更接近癌症生物学，也认同 AI 能缩短它走向应用的时间，那么即便数学现在已经很有用，未来也会显得更有用。就像哈代在《一个数学家的辩白》（A Mathematician’s Apology）里谈到的那样，还存在一个问题：如果事情能办成，为什么还需要人的理解？

我目前听到的最有说服力的理由是：人类的理解能带来 AI 目前想不出的范式转变。人类天才可能会发现一些方法，比如用 Maynard 筛法证明素数间隔有界，从而推动整个领域前进。但这个观点最有力的反驳是：如果 AI 持续进步——我觉得这更多是资本市场的问题，而不是技术问题——它也能提出猜想、建立数学理论，甚至想出分布外的范式转变。

接下来反过来问：人类数学家会在哪里？如果你认为数学有内在价值，那数学家会有更多类似开发者的工作流，因为编程就是一个有内在市场价值的例子。如果你不这么认为，那数学就会走下棋那条路，我觉得前面这些论点就不适用了。

最坏的情况其实是……

我觉得最坏情况是资本市场崩盘，AI 进展受阻。到时没多少人投入时间去理解数学，范式转变的想法也会变少，然后我们就会陷入停滞。这会是最坏的情况。

最好的情况是市场继续发展，更多人成为数学家——这里的数学家，是指在工作流程中把数学作为重要部分、甚至主要部分的人。他们的需求不会被 AI 机器取代。假如 AI 真的持续进步，反而会需要更多数学理论来解释收集到的数据，也需要从数据中推导出该证明什么的规格说明，同时代码库也会不断发展。当然，时间上可能有个衔接期：一开始也许很好，之后市场又可能崩盘，这可能会是个问题。

谢谢。

好。先介绍一下背景：我和一个叫 Assumptions of Physics 的团体合作，他们召集世界各地的研究者，试图找出能够导出物理学的最小物理假设集合。这也意味着，要让物理学在数学上保持一致。既然 Axiom 关注数学，你们会不会也考虑物理学？物理学的解释很重要，还需要用预测来支持这些解释。Axiom 会往这个方向做吗？

这很有意思。我们和几个应用领域的团队有合作项目……

……我们和几个应用领域的团队有合作项目。我们实际上维护一个叫 Math Econ Lib 的计量经济学库，是我们发起并维护的。我相信我们还和一个量子计算学术团队有合作。我觉得也有深度学习理论、物理学方面的合作。物理学似乎有一个由开源社区维护的库。我们还没有专门深入探索物理学领域，但我很感兴趣的是，你刚才用一阶逻辑的方式来描述如何寻找最小假设集，以及如何像依赖树一样在其上构建理论。我们之后一定要聊聊。

太好了，谢谢。

你好，很高兴认识你。我有个比较细节的问题：你提到智能体的未来会不同于我们现在看到的硬编码 harness。能不能再具体讲讲？你说我们需要可训练的 harness，对吗？

现在我觉得已经有几家实验室能对模型做智能体强化学习。这样模型就能使用所有工具和技能，甚至调用自身或自身较小的检查点。我觉得这会成为 2026 年的新词，2027 年也许又会有一个新词，我还不知道会是什么。我觉得“群体”（swarm）已经很接近了。没有 swarm，我们就做不到现在这些事。接下来一个前沿问题是优化 swarm 的成本；要做到这一点，需要非常好的小模型。因此，小实验室训练智能体强化学习模型的故事不会结束，因为你可能既需要更大的模型，也需要更小的模型。

训练起来应该更容易——希望更容易。谢谢。

抱歉。