🔬超越非正式AI - Carina Hong, Axiom Math

但我觉得这是第一次，经过验证的AI要开启协作。要么是人机协作。在Blueprint之前，那是人人协作，而Lean是基础，是验证，是形式语言，然后才是我们现在看到的人机协作，未来还有AI智能体之间的协作。我认为经过验证的AI是为了开放，不是为了满足封闭行业的需求。而且我觉得验证不应该像——哦，我记得有篇文章说聊天机器人搞混了，哦，这是某个数学题的解法。对我来说，验证不是关于马虎。验证是关于放大卓越，复合卓越。就像回到协作那个点。就像拉马努金已经是一个非常强的数学家了，但验证帮助他扩展了卓越，既向上扩展也向外扩展。

谢谢邀请。

真的吗？

哦，好吧，哇。

我觉得我们应该在数学研究上花更多钱。

是的，我知道。

是的。嗯，非常非常高兴能来这里。而且我觉得，你知道，这是A轮融资，所以这是一个非常非常及时的播客。我们是一家成立七八个月的公司，所以这对我们来说意义重大。这是一个很酷的里程碑。我们现在大概有30个人，对吧？所以我觉得这笔资金将为我们提供所需的动力，加速我们迄今为止强劲的执行势头。我觉得人们对Axiom有很多种看法。人们把我们看作一家数学初创公司。数学初创公司，Lean初创公司。我们做的另一件事显然是形式验证，我们认为验证是数学一个非常好的最佳优先市场。所以我认为这轮融资将让我们探索一些应用领域。正如我的同事CTO Shubo在我们A轮融资的发布视频中所说，它让我们拓宽了梦想。是的。

那么，让我们回到2024年。当O-1推理模型刚出来的时候，Anthropic当时在秘密做什么？是编程。每个人都知道他们在做编程，像OpenAI、Meta、Accenture，所有人都知道Anthropic在做编程，但他们就是忽略了。他们想，哦，他们是B2B玩法，只想要一个垂直领域。人们把编程看作一个垂直领域，现在看看我们走到了哪里。编程从编程到推理有很强的迁移学习，基本上，你知道，未来推理领域的垄断。我认为这真的非常非常令人震惊。那些做编程的人，我认为他们当时相信一些我们现在也相信的东西，类似地，数学和Lean也是如此，那就是如果你有更结构化和形式化的数据，它将会比我们正在攻克的具体垂直领域更具横向性。所以，你知道，如果我们今天在做非形式化的数学，比如标准的思维链数据，基于人类偏好训练一个数学模型，那么我会说，也许我们只是一家数学初创公司，对吧？但是，你知道，在追求数学的同时，我们也在做一些对其他领域有迁移学习的事情。所以我认为这更像是一个更广阔的图景：公司的DNA仍然是数学，我们所有人都是数学书呆子，这是一个非常强烈的文化宣言。每个人都有伟大的使命，让AI成为超人类的数学家，就像我们在Pandan上看到的一批研究猜想一样。事实上，我们还有另一批即将到来。我们也认为这将是经过验证的推理的基础，我们稍微谈到了经过验证的AI。接下来我想谈谈经过验证的AI，因为我觉得你还有另一个——

是的，是的，是的。我有——有几件事我想问，呃，所以我想听听关于经过验证的AI。我确实想深入探讨一下。那么，我们知道Anthropic和OpenAI以及所有人，他们不做形式验证并将其用于他们的发布或其他方面吗？

我觉得我有很多小道消息，可能不应该公开说出来。嗯，我觉得，你知道，研究人员会聊天，他们会打牌。是的。是的。但不管他们做还是不做，都有一些非常有趣的原因。我认为这是我得到的要点，那就是如果你在前沿实验室，方向确实会因为很多你无法控制的原因而经常变化。所以我想让我们回到AlphaProof的时刻，对吧？AlphaProof真是太棒了——对我来说，2024年42分中得28分就是IMO时刻。不是2025年的围棋，因为在2024年和2025年，AI模型可以解决所有非组合数学的问题。唯一的区别是，如果你解决了所有非组合数学的问题，2024年你得28分。2025年你得35分，因为2025年只有一个组合数学问题。在AlphaProof之后，我们并没有看到很多来自Google DeepMind的形式数学结果或进展。这实际上是因为一些不一定是技术上的原因。但如果你在一家初创公司，并且有非常单一的重点，那就是形式数学和经过验证的AI，那么你就可以长期研究一个非常酷的问题，并且在取得进展和突破方面，你成功的可能性要高得多。

是的，那么为我们定义一下这个。

是的。很多人把形式化验证看作一个古老的话题。它早在深度学习出现之前就存在了，甚至可以追溯到基于规则的计算机科学时代。自20世纪80年代以来，形式化验证就一直被大力推动。有一些非常有趣的历史轶事，比如我记得巴黎工会曾要求地铁系统的自动切换必须经过形式化验证以确保安全。所以，工会对技术提出这样的要求还挺有意思的。还有，在挑战者号事件前后，欧洲航天局一直在用形式化验证来检查阿丽亚娜航天器。波音和空客也在用形式化验证。再近一些，AWS在自动化推理方面投入了很多，因为他们有很多企业客户，要求系统100%验证，不能遗漏任何边界情况，而普通的测试无法满足这种需求。所以很多人把验证看作一件烦人的事，觉得它只是税务和合规层面的负担，确保一切就绪而已。但这并不是——我们刚才聊到了验证。我觉得我们的竞争对手在推出产品时，也提到了形式化验证和预推理。他们是在幻觉问题的背景下讨论的。对他们来说，形式化验证可能就是为了消除低质量输出和幻觉。但对我们来说不是。对我们而言，验证过的AI是关于卓越的。它是关于扩展和叠加超级智能的。这是一个相当深刻的观点，有时需要稍微解释一下。举个例子，关于卓越，比如拉马努金，他是一位杰出的数学家。他在学会如何做证明之前，就能凭直觉发现很多有趣的公式。后来他去了剑桥，与哈代和李特尔伍德合作。在著名的电影《知无涯者》中，有一条故事线讲述了哈代如何艰难地迫使拉马努金不再依赖直觉，而是去做证明。学会写证明之后，他成为了一位更强大的数学家，他的直觉成果变成了定理。后代的数学家们在这些定理的基础上继续发展。所以，这是一种扩展和叠加我们已有智能的方式。另一个例子是，数学家们几千年来一直在用英语或各自国家的自然语言“写代码”。我为什么称之为“写代码”？因为数学界有一套严格的逻辑推导标准。每一步都必须正确无误，否则你就会被数学界排斥。所以，这是社区内部的规则。这很有趣，对吧？因为这相当于人类数学家强制执行的标准。这是一个同行评审的过程。目前一篇论文的同行评审需要两年时间。但即便如此，像Lean这样的证明助手和形式化证明检查器仍然找到了自己的位置。为什么？如果我是个数学家，我的工作可以由其他人类同行评审，那为什么还要用Lean呢？为什么还要讨论基于Lean的辅助定理证明呢？因为它能处理底层细节。比如，我们甚至还没谈到AI。就拿Lean中的Grind策略来说，它目前能在非常底层的层面上处理大量繁琐的证明。这相当令人震惊，因为我见过另一家做类似领域的公司，他们的某个演示，我一看，发现那些内容其实完全可以用Lean中的Grind策略来处理。

哦，好的。嗯，我觉得我们刚才的顺序有点乱。是的。Lean是一个计算机程序，有点像用来做数学证明的。它是一种形式化语言，和它的同类Isabelle、Coq、Roc，以及更远一些的Daphne、Agda等形式化语言类似。

它是做什么的？

基本上，如果你在Lean中写了一个证明程序，假设没有发生任何奇怪的事情，比如意外使用了SORI（一种允许你默认某些东西成立的策略），并且假设一切安全，因此人们有像comparator、SafeVerify这样的工具，最近Axiom也推出了VerifyProof，速度比comparator快100倍。那么，一旦你执行这个程序，当它编译通过并告诉你证明正确时，这个证明就确实是正确的。

所以它就像一个类型检查器？

是的，它基于一个叫做柯里-霍华德对应的结果，这个结果把证明转化成了程序。我想谈谈Lean的魔力，以及为什么我认为它是一种非常好的编程语言。因为一方面，如果你完全不在乎形式化部分，不在乎逻辑部分，只想用Lean来写代码，你也可以。比如，我们有过一些候选人，实际上现在有个人在Lean FRO工作，他在Lean中写了自动微分。这是在我们面试过程中用Lean做的。

所以它是一种图灵完备的语言。

没错。你可以用Lean做很多事情。它是一种函数式编程语言。然后你也可以用它来做数学，一举两得。

好的。

回到我刚才想说的，如果数学家们已经在强制执行大多数证明的正确性——当然不是所有数学家，但学术界的象牙塔里的人们确实如此——那我们为什么还需要Lean这个模型检查器呢？因为Lean有一些策略，可以帮助他们处理底层的计算、证明或推导，这样他们就能在高层的直觉空间中自由探索。这就是我的观点：形式化验证或验证过的AI，对我们来说，不仅仅是消除低质量、幻觉和错误。它是关于扩展卓越的。它是关于超级智能的。

实际上，陶哲轩有一个很棒的视频，讲的是如何用Lean进行协作，因为你可以利用这些故事。

没错，没错。这正是我想谈的另一点。很多人认为，我们的市场一定是某个非常小众的工业领域，比如任务关键或安全关键的领域。不，那不是总可寻址市场。总可寻址市场是所有代码。它是所有AI生成代码的优先选择权。所谓优先选择权，意思是你可以选择是否要验证它。这是我想强调的重要一点：人们觉得形式化验证很痛苦，因为它有那么多严格的要求。

到目前为止确实如此。

是的，是的。对我们来说，验证生成（verified generation）实际上意味着性能提升。它意味着更高的样本效率。意味着像我们这样的初创公司——虽然也融了些钱，但计算预算和数据预算都比前沿实验室少——也能在超人类任务上匹配甚至超越它们的表现。事实上，就在2025年12月我们实时参加的PanAm考试中，MATH Arena（一个评估众多LLM的组织）发现，最好的LLM DeepSeek在120分的考试中得了103分。最佳人类考生，我们后来知道是来自MIT或芝加哥大学的学生（具体哪个不确定，因为他们不公布前五名得分），得了110分，而我们得了120分。所以这是第一次——我记得刚开始时，人们还在质疑：一个形式化数学系统，数据量少了好几个数量级，怎么可能匹配甚至超越非形式化的LLM？PaLM是第一个击败它的例子，对吧？所以我们思考的不仅是它带来的痛苦和挑战，而是验证生成带来的性能提升。就像你预期RL在编程上会带来改进一样，RL在Lean上也会带来改进。这是我想说的第二点：如何看待验证和验证型AI。

那或许可以聊聊为什么。你能描述一下你们做的和前沿实验室在构建标准RL增强型LLM时有什么不同吗？你们的方法有何独特之处？

是的，我们高度依赖一种叫做Lean数据的数据。简单说，Lean就是所有我们拥有的、经过验证的证明数据——它要么正确要么错误，这一点非常关键。所以我们有一套模型系统，这些模型经过后训练，使用RL或FFT。

所以你们用的是现成的某种基础模型，然后进行后训练或持续预训练？

对。而且我们明显倾向于开源的基础模型。

所以它懂英语，大概也会编程。

是的。

但你们还会对它进行微调或持续预训练。

对。基础模型可能和其他人用的差不多，如果他们不自己预训练模型的话。

嗯。

然后我们基本上做的是针对形式化数学的RL。我认为存在一套标准的流程或行业技巧，我们尽量在此基础上进行创新。我们发现，扩展推理几乎没有瓶颈，可以递归地将一个证明目标分解成多个子目标，并学会回溯。

分布偏移？

所以，这是一个开放问题：一个在数论上表现很好的系统，能否在另一个数学领域——比如拓扑学——也表现良好？实际上，我认为这取决于情况。取决于拓扑学中是否已有大量现有定义，就像数学基础设施一样。因为过去人们发现，在构建Mathlib时，比如代数的“书卷工作”，他们可以轻松地……

所以Mathlib就是Lean的“本科图书馆”之类的东西。没错。它包含了你在本科数学中学到的所有证明，并且都用Lean实现了。

对。比如，我一些现在在Axiom的朋友——这真是命运轮回——Kenny和我认识五六年了，他是第一个告诉我Lean的人。他当时和Kevin Buzzard一起构建Mathlib。在Mathlib中，代数比分析更容易形式化。这很有意思，因为分析中很多关于收敛、极限的定义变得棘手。所以我认为现在的Mathlib里没有太多拓扑内容，比如微分拓扑、微分几何之类。因此，我们的系统在这些领域可能表现不佳，因为它甚至没有定义可以依赖。但在有定义的领域，我们在分布多样性和性能上其实做得不错，比如已经解决了数论、交换代数、代数几何中的一些开放研究问题，以及考试中出现的离散数学和概率问题。

是IMO，国际数学奥林匹克。

我觉得是的。在数学奥林匹克中，人们发现组合数学有点棘手，步骤似乎需要很多创意。作为人类，我有一些非常擅长组合数学的朋友——我从不认为自己擅长组合数学，我更擅长数论——但我知道有些人，他们是IMO金牌、满分，Putnam Fellow、满分，一路下来。当他们展示组合数学的技巧时，我会想：你怎么想到的？但一旦你给出构造，其实就变得可追踪了。所以我认为基于Lean的系统会在这些非常需要创意的地方遇到困难。这也是为什么我们Axiom还投资了一个叫“数学发现”的项目，它不使用Lean。我们将在未来几周发布一些重大消息，基本上会开源整个数学发现的代码库。

能稍微透露一点吗？

对，没错。所以我们目前正在开源两个代码库。目标是，如果你是一位数学家或理论物理学家，有一个想要解决的问题，比如你想找到一个非常复杂的图论构造，那么我们会建议你按照我们为数学家编写的详细手册来运行代码。这是一个帮助数学家进行数学发现的工具。数学发现这个概念是说，证明对于数学来说并不足够。实际上，在你开始证明某件事之前，你根本不知道从何入手。所以你会尝试构造一些有趣的例子。这些例子通常可以是数列，对吧？如果你想理解一个数列的性质，你会写出前几项。也可以是图。如果你想弄清楚你正在寻找的图是否应该具有某种性质，你会从构建一个更简单的图开始。但有些构造无法通过 Lean 来完成。所以我们相信应该用 AI 来做大规模发现。这个领域的先驱之一，François Charton，是 Axiom 的技术人员。他之前做过模式提升和端到端工作，比如通过找到反例推翻了一个存在30年的猜想，还解决了一个130年历史的问题——全局拉普拉斯函数。这是一种在三体问题中出现的数学对象。所以我们认为，数学发现工具应该向数学界开放。因此我们正在开源整个代码库。

所以“发现”的意思是，它能提出新的猜想，还是——

实际上，那是一个预猜想阶段。

哦，我懂了。

是的。所以你先形成直觉，对吧？如果你是一位数学家，目标是解决一个非常难的猜想，Aximprover 不能直接替你解决。你可能会想尝试提出一些引理或猜想，然后交给 axiom prover。如果你是人类数学家，你会先想如何表述那个猜想。你不知道方向在哪里。你想找到构造。而我们即将开源的代码库，希望能在这方面显著帮助你。

有一件事可能——很多计算机科学家在听，他们立刻会想到，尤其是谈到形式验证之类的时候，就会想到 Rice 定理、可判定性、不完备定理，以及一些关于计算复杂性和 LLM 的争论。所以我很好奇——Rice 定理说，对于所有程序，你无法证明关于程序的非平凡性质，对吧？那么你们是如何在这个空间中运作的？显然形式验证能做某些事情。是的。

是的，我认为很清楚，理论结果告诉你，你无法形式验证所有程序。但我觉得，形式验证大多数有用的程序是好的。对吧？我记得 MIT 有一个小纪录片，或者说是给录取学生的广告，里面有 MIT 吉祥物 Tim 的一句名言：“理论能给你什么？”这大概就是说，理论不会阻止我们尽力去推进。所以我们未来的目标是，假设你在写代码，想要白盒编写一个非常复杂的任务。目前是前端网站，但未来我们可能想白盒编写更复杂的东西，甚至整个分布式系统。那么我们希望能够分解它，可能有一个高层次的草图计划，我们可以做，别人也可以做。但比如说，Claude 给你分解成10个步骤，然后在某一步它会决定调用 Axiom，Axiom 会给你一个经过形式验证的计算机程序，或者它会说，这个对我们来说还是太难了。

所以你写程序，交给 Axiom，它可能会做修改。

我们讨论的是两个阶段。有可能我们是验证伙伴。你已经有一个计算机程序，想让我们验证它。事实上，GPT 找到了一个未解决的 Erdős 问题的证明，我们的竞争对手 Harmonic（亚里士多德）验证了它。但我们想做的是验证生成，对吧？我们可能会说，嘿，这个小组件，我们生成并提供给你的所有东西都是经过形式验证的。

验证。我明白了。所以想法是，你同时生成两者。我可以想象这符合承诺的概念——或者抱歉，意思是它是一个未证明的引理，你暂时接受它，直到你有时间证明它，对吧？这是一个理解理论的好方式吗？

这是一个理解理论的好方式，但不一定适用于编码上下文。

所以我可以想象，你可以说，假设这个模块已验证，那么这个模块就是正确的。这样你就可以把问题分解到足够小，以便验证。这是这里的直觉吗？

比如说，我们想要处理网页代码的控制流。这相当难。你可能会把它分解成多个步骤，然后继续分解成更细粒度的步骤。在某一步，你想要绝对正确的东西，这也是可能实现的。然后我们想生成——我们想生成一段计算机程序，底层有一个 Gernot 保证，同时生成了证明，告诉你你指定的东西，这个程序可以为你解决。所以我们的愿景是，任何可以定义的东西都可以执行；任何可以指定的东西都可以被证明。我理解的方式是，如果你有一个程序乘以一个语句或问题，它会映射到可验证性条件乘以一个证明。编程验证社区已经给了你可验证性条件，我们正在招募一个非常强的团队来帮助我们做这件事，而 Axiom Prover 会给你证明。

那么请帮我从程序映射到证明，因为我可以这样说，这个两行的 Lean 程序验证了它声称解决的东西。我怎么知道它确实验证了我认为它验证的东西？

是的。举个例子，目前有一个叫 Codeveri 的基准测试，它是一个代码验证基准，设计为对 Lean 友好。每个问题都是一个代码问题，目标是生成——有代码部分和证明部分，两个不同的计算机程序。然后目标是生成带证明的代码。也就是说，代码应该解决这个问题，而证明则表明这个程序确实解决了这个问题。我明白了。

那人们在这个基准测试上表现如何？我挺想聊聊这个，因为挺有意思的。这个基准测试是2025年由伯克利和Meta的研究人员推出的，他们发现，无论评估的是哪个版本的GPT，pass@1大概只有3.6%，迭代版本大约是22%。那形式化数学系统模型的表现呢？Copra是一个系统，因为在系统里你可以迭代和定义，所以pass@1不太适用，但他们还是评估了系统的pass@1，大概在11-12%左右。还有DeepSeqProver和GodotProver，这两个很强的证明模型，也是11-12%。我记得我们的竞争对手去年在纯证明部分达到了96%。而我们最近，在不修改Pandem系统的情况下，达到了99%。189个问题中，我们解决了187个，只漏掉了2个带证明的代码问题。所以，如果你想训练一个能做带证明的代码的模型，并且想做强化学习，其实挺烦人的，因为你看，这很混杂。如果你希望证明是非正式的数学证明，那也很烦人，因为那就像是一个混合的目标函数。你的代码是Python，你的证明是自然语言的数学证明，这样RL的表现不会很强，对吧？但如果你用Lean做证明，代码选Rust这种强类型语言，那就更收敛了，表现会好得多。

我有点想不通怎么把这两者联系起来——比如，我可以说这个证明解决了费马大定理，对吧？

对。

嗯。但我不知道，对吧？它可能只是Lean里的两行代码。显然不是真的。那我怎么知道我写的程序和我生成的证明是匹配的呢？

你基本上会看编码问题，然后看程序，再试着检查它是否满足可验证性条件。

但我要怎么知道呢？比如，我读一下，我扫一眼就能说——传统上数学家是怎么做的？他们拿过论文读一遍，然后说，我同意这个证明解决了问题。然后另一个人说，不，它没解决，你看这里。然后大家争论，最终达成共识：这个证明解决了这个问题。所以，你怎么——

但你可以一步步检查，对吧？

对，没错。

嗯。所以你基本上会看可验证性条件，看它是否真的满足。假设我们在看一段计算机程序。

嗯。

然后它是否真的解决了编码问题，你会有一个判断，对吧？

对。

所以你不会只依赖测试，尽管那是一种方式。那只是其中一种——有人会看证明。

然后说，对，这确实解决了我们认为它应该解决的问题。

但这样一来，你实际上是在生成一个形式化验证程序，它满足关于这个程序和这个声明的可验证性条件。所以，这个函数的作用就是把你从程序和声明带到可验证性条件和证明。

好吧。那我明白这在基准测试里怎么用了。但假如我有一个飞行控制系统，它非常可靠。

那问题就变得很烦人了，主要是规格说明。我觉得这个词是关键，就算我们说成功了，任何东西都会有规格说明的问题。比如一家银行来说，请帮我做一个非常安全的财务审计，或者证明这个财务审计，那是什么意思？我们没法定义清楚。人类不擅长定义所有想要的东西。总有一些东西没被定义，而如果没被定义，就没法证明。

那你怎么处理这个问题？

嗯，我们还没到那一步。目前，愿景是任何能被定义的东西都能被证明。显然，有些人很擅长这个——这也许就是非形式化推理器发挥作用的地方，对吧？非形式化推理器可以——我想提一下测试领域的文献，测试很棒，因为它就像在问：“你考虑过这个吗？”我想强调一下XMCTO Shubo的基于突变的LM单元测试生成工作，他是Facebook AI Research的负责人。你可以这样想：AI会问：“你考虑过这个情况吗？”这有点像猜想。猜想有助于完善规格说明。

我明白了。

然后证明器来做证明。

所以这是一个交互过程，也许人参与其中，这样我们才能给出好的规格说明。

我认为这是编码的未来。

是的。

对。我认为这是编码的未来。而且我认为，即使我们假设一切都可以被形式化验证，研究自动测试生成之类的东西仍然很有趣，因为它本质上是在给你提出规格说明的建议。对吧？然后还有一件事，我们来聊聊自动形式化，也就是定义的能力。它有点像把非形式化的东西转换成形式化的东西。假设我有一个为ICPC写的编码问题，是用英文写的，比如“Alice和Bob，等等”。现在我想把它转换成一个形式化声明，比如形式化规格说明，那自动形式化这一步怎么做？因为我还没解决问题，所以没有任何信号，也没有任何依据。测试用例、输入输出对，会给我的形式化规格说明提供依据。

所以，我知道我要给这个输入，得到这个输出，它必须有这些特征。然后我写测试用例。那在Lean里有没有类似的东西？就是那种规格说明，你只知道预期的结果，比如结果的声明，但证明是完全未完成的。

Lean其实挺烦人的，因为它很多时候是证明，所以你没有数值答案来做依据。所以自动形式化很难做，因为通常的情况是，你没法给声明的自动形式化提供依据。你当然可以给证明的自动形式化提供依据，因为你可以直接运行它，但需要人来检查。

一个形式化程序，如果规模很大，它的Lean证明有多大？它是随程序规模线性增长，还是超线性增长？

嗯，实际上，每写一行代码，可能对应20行证明。情况不太乐观。

但这是线性关系吗？还是说随着程序复杂度增加，证明规模也会增长，比如变成40%？

关于这个的缩放定律，我没有很好的答案。

哦，好吧。

是的。

因为我知道这在形式化验证中是个问题。

没错，没错。

即使是很简单的程序，你也需要非常非常长的证明。那么，当你开始处理更大、更复杂的任务时，LLM的能力会不会遇到某种限制？

我们从根本上相信，我们正在构建一个推理引擎，而且我们已经看到Axiom Prover处理过非常大的树结构，比如证明树。我们已经看到它从40个节点扩展到4000个节点。

等等，抱歉，Axiom Prover就是那个LLM吗？

Axiom Prover是一个由多个模型组成的集成系统，我们对它进行了后训练（post-training）。

我明白了。

对。而且它显然也包括我们开源发布的Axle工具。抱歉，是的，在我们的系统里。所以，我们已经看到它能够处理越来越复杂的任务。我们不认为它有特别的限制。你可以问，在预训练基础模型上，它是否会在某个点上受到限制？

嗯。

我认为这是个好问题。我觉得中间训练（mid-training）可能非常有趣，因为很多能力提升确实来自那个部分。你可以这样论证：即使你试图用强化学习去训练一个天赋不高的人，这个人的表现可能远不如经过后训练的人。拉马努金。你可以说，这是很残酷的现实。所以，我们可能在某一天会考虑这么做。但我们认为还有很大的空间可以推进。

所以你只是觉得目前还有很大的空间，还没有遇到理论上的限制。我只是好奇，因为最近有一些关于LLM根本上能解决的问题的计算复杂度的研究结果。我觉得这些结果在我用Claude Code写代码时并不是什么大问题。但我可以想象，在这样的系统中，当问题变得足够大时，比如你有海量的Lean代码行，你无法把它们全部塞进上下文窗口。所以你必须巧妙地处理，然后进行总结，再总结，很快你就会有点跟不上。在一个非常大的系统中，你可能会遇到这种情况吗？

是的，我觉得这很有意思。这总是一个资源过剩的问题。假设数学发现的复兴真的到来了，AxonProver试图证明一切，最终你会得到成千上万的Lean证明。首先，自动非形式化（auto-informalization）比自动形式化（auto-formalization）容易得多，因为它没有缺乏基础的问题，对吧？每个模型都见过大量的文本和Lean代码。所以你可以随时把那个Lean代码转换回非形式化的表述。然后问题就变成了：你怎么知道它是否正确？你可以依赖循环一致性。所以你再把它形式化，然后证明程序等价性之类的。

所以那是——

哦，所以你把它非形式化，然后再形式化，以确保它仍然可用。是的。就像这样。虽然非形式化显然是一个不那么困难的问题，所以你总是可以做到。所以对于我们输出的很多Lean代码，我们可以有一个非形式化的总结器，用来总结大块的Lean代码。它实际上做得还不错。所以，这是其中一点。另一个我觉得非常有趣的问题是，我记得去年在温哥华ICML的AI for Math研讨会上有一个讨论小组。有Leo Damora、Jeremy Auigard，还有Shubo（CTO）在场，他们讨论的是：人类或数学家会不会在某个时候停止试图理解正在发生的事情？因为假设你是一个雄心勃勃的数学家，你想证明黎曼猜想，然后砰的一声，这里有一个Lean证明，而且它实际上是正确的，但问题在于，它有一百万行代码。

我正要说到这一点。那个讨论小组讨论的问题就是：这种负面影响会不会发生？这完全是假设性的。目前没有任何模型系统能证明黎曼猜想。所以免责声明，请不要剪掉这部分。请一并发送。但人们还会试图去理解它吗？我认为答案通常是肯定的。我认为好奇心，以及想要理解数学或其他领域正在发生什么的渴望，是人类的基本需求。我认为，在一个所谓的经过验证的超级智能时代，这给了我们一剂乐观的良药。假设我们达到了那个阶段，即使所有输出都以比人类可能消化的速度快得多、数量级大得多的速度产生，人们仍然会试图去消化它们。他们仍然会试图去消化那些他们认为重要的内容。所以，本质上注意力成了瓶颈。如果注意力是瓶颈，那么真正重要的是直觉和品味——哪些陈述值得人类去消化，也许在有限的计算资源下，哪些值得花费计算资源。这就是人类数学家的品味将永远指引我们的地方。我认为这非常美妙。

是的，我们最终会做到这一点。因为我认为，这个猜想可能取决于我们所说的品味和优雅是什么意思。对我来说，这感觉像是一个对齐问题。谁来决定什么是优雅？人类来决定什么是优雅。

太棒了。

太棒了。

人类的进步。这和努力有关，对吧？你努力钻研什么，你就会擅长什么。

是的。而且我认为在很多领域我们都会遇到这个问题，不仅仅是数学。比如，如何成为一个拥有出色高层理解力的资深程序员？我想是拥有全栈理解力，高层和底层都懂。你没有经过多年的训练。

我的意思是，我会说你不必——这很哲学化，但你知道，我不需要擅长汇编语言编程，对吧？没有多少人擅长那个。只有少数人擅长，因为这对他们的工作很重要。

这不是经验的问题，而是好奇心的问题。

嗯，但我觉得这有点不同，因为比如说不擅长证明东西，对吧？这似乎是一个根本性的差距，如果我不做这些，我的思维可能不会以同样的方式发展。而如果我只是不擅长汇编语言编程，但我擅长高级编程，那可能就没关系。

我认为这很可能是因为教育体系和培养路径的问题——如果你没有早期展现出才华，有时就无法经历预训练的过程。在数学领域。

是的。

对。所以也许你可以说，你不需要学习所有东西来培养品味，但你需要达到一个门槛。比如，你可能需要会写代码，即使你不懂汇编语言。而那种能力可能会迁移——我的直觉可能会从奥数题迁移到其他研究领域，我尝试去探索。组合数学的迁移更直接，非常相似；数论可能远一些，但还行。当涉及到与奥数差异很大的领域时，迁移效果就弱了，但就像你说的，你需要勤奋，对吧？你需要勤奋地经历一定量的训练。如果人们过度依赖强AI，这个过程就不会发生。

我想换个话题。

好的。

你提到了软件验证。具体是哪些领域？你们打算怎么赚足够的钱来支撑这个估值？另外，恭喜你。

谢谢。

那么，给我们一个高层次的总结吧：你向投资者展示的愿景是什么，为什么这能赚大钱？

好的。首先，这轮融资有点先发制人的性质，所以很多投资者对Axiom的兴趣非常高。至于我们的信念，我们认为编程的未来将在某种程度上受限于验证能力。我们相信解决形式化数学是一个非常自然的起点。然后，通过扩展，你可以提升硬件和软件层面的验证能力。比如在硬件方面，这相当具有革命性。据我们所知，没有所谓的"大部分验证通过"的GPU——要么全对，要么全错。而且你需要一个完美的证明器。我想强调这一点：假设我是一个热爱解决数学问题的人，比如很多Twitter用户喜欢像抓宝可梦一样追逐Erdős问题，然后我尝试用非确定性的LLM（比如GPT）来获取完整证明。我可以试很多次，可能成功也可能失败，而我不在乎是否成功。但这在硬件验证上绝对行不通。所以对于这些我称之为"硬核验证需求"的领域，这是一个痛点，一个当前的痛点。有成百上千的人和数千个许可证被用来解决一个局部网格问题的验证。

顺便问一下，据我所知，ASIC项目中设计到验证的行业标准比例大概是1比3到1比4。

1比3到1比4，没错。无论是团队规模还是时间周期都是这样。

验证方面。

对。所以如果你把这个比例乘起来，嗯，平方一下。我认为这是一个必须覆盖的领域。至于软件验证，它很有趣，对吧？因为我们可能都意识到，比如我的侄子Vaibhav写了一个可爱的网站，完全没有必要去形式化验证那段代码。但凯特·马茨给我讲过一个故事，她是《纽约时报》的记者，她说，如果你想想在智能体的时代，比如我的Open Claw可以做各种事情，也可能做坏事——比如它可能决定给我的教授发一条不好的短信。你可以说这是形式化验证的问题吗？可能还不是。你可以改变行动空间，让它更受限，这样就不需要依赖形式化验证。所以有很多情况，但你可以想象，一个处理大量监管事务的企业在使用智能体时，可能会选择这么做。但我认为，验证能力的提升——无论是延迟、准确性还是整体性能——将决定人们是否依赖形式化验证。所以从某种意义上说，我们想把它做得足够好，让人们可以做出这个选择。

那么，为什么投资者认为你能做到呢？因为人们研究验证已经很久了，而且大家都同意这是个重要问题。如果我能为我写的每个程序都拿到验证证明——比如"嘿，Claude，顺便给我个证明"，然后它直接生成，我一看"嗯，没问题"——我绝对会这么做。但你觉得投资者看到了什么，让他们相信现在是时候投进2亿美元之类的？

我认为信念这东西，要么有要么没有。要么和我们一起做梦，要么不，这没关系，因为当我们实现这个梦想时，公司会值100亿美元。这是我的感觉。我们相信验证是通往超级智能的关键部分。我们版本的超级智能是绝对经过验证的。我们认为没有其他可能的未来。我公开说，我们不相信一个非形式化的系统会成为最终的AGI解决方案。

为什么不信？

我们就是不信。

我的意思是，反方观点是，比如我们做大量好的强化学习，而且我们看到GPT解决了一些Erdős问题之类的。那你为什么觉得这条路会走不通？

你可以说，如果你在前沿数学领域，有一个前沿实验室和无限资源，那从定义上说就不会走不通，对吧？如果无限意味着不会耗尽。但我不认为它能扩展到超级智能。

所以你觉得会耗尽，比如钱花光了，或者算力不够了？

首先，我们作为一家初创公司做不到那样。但我们普遍认为，形式化数学——以及通过将数学证明转化为程序、转化为代码——能给我们带来更好的性能。

所以这只是你的样本效率论点之类的，也许如果你不使用形式化语言，就无法足够地弯曲曲线。

关键在于，非正式的东西其实我们也能接触到。如果你真的，你可以同时拥有非正式和正式系统，那会非常强大。我比较担心的是，我怀疑仅靠非正式方法能否扩展到通用人工智能（AGI）。因为你会不断遇到这样的情况：要么用大语言模型作为裁判，要么靠人类专家打分，而人类专家本身就不太容易规模化。如果你真的争论无限、无穷，那当然，你也有无限的钱，可以付无限的报酬。但真的有无限多的人能理解并证明，比如说，朗兰兹纲领中一个非平凡的结果吗？我觉得，想找到这些人可不容易。事实上，我认为 Frontier Math 之所以能成型，是因为他们无法靠自己的专家库构建一个基准测试，所以不得不与 Epoch 合作。对吧。而这正是我对 Quan Tsung 中人类部分所担忧的。他们用大语言模型作为裁判，现在又有了随机评判。问题在于，有些事情是根本不可能实现，还是极其昂贵——而且真的是极其、极其昂贵才能实现——这两者最终被混为一谈了。

当然，投资者总想知道为什么是你，对吧？我读过一些你的背景，我觉得如果不让听众了解一下你的个人故事，那会是一种失职。

我明白了。

你能稍微谈谈吗？你做过一些非常有趣的事情，所以我很想听听你和你团队的故事。是什么让 Axiom 如此特别？

是的，我认为 Axiom 非常特别，因为我们有真正的数学专家。基本上，他们是我们正在开发的系统的用户，而这个迭代循环非常快。它极其、极其快。你有一批顶尖的数学家，既包括研究领域的，也包括奥赛领域的。同时，你还有 MassLib 的贡献者、维护者、开发者，比如 Lingurus 这样的人，再加上来自应用机器学习领域的人，来自像 Meta FAIR 和 Golden Age FAIR 这样非常强的机构，以及有代码生成（CodeGen）专长的人，他们曾与编译器（如 KernelGen）合作过。把这些背景的人聚在一起，我认为这种跨学科的思维方式非常有帮助。我们觉得，AI for math 传统上就是跨学科的。人们从 AI for science 中借用技术，从代码生成文献中借用纯技术、枯燥的技术，也从更广泛的前沿领域（比如应用机器学习）借用技术，试图将其应用于 AI for math 这个细分问题。因此，我们认为拥有这样一个非常特别的团队本身就是一种差异化。我们也认为，正如你所说，没有永久的护城河。我们生成的专有数据以及我们正在看到的飞轮效应，是一种暂时的护城河。就我个人而言，我热爱数学。我觉得，我从小就开始学数学，而数学有时会变得非常难，当你解决的问题刚好超出你的能力范围时，会有点沮丧。有时候我会想，要是能有个 AI 帮我就好了。是的，我想——为什么不干脆造一个这样的东西呢。

你在牛津大学读了一个神经科学的硕士。是的。这对你的思考有影响吗？

这是个好问题。我认为我在神经科学方面的经历让我很好地了解了什么是困难的，什么是不可能的。我的意思是，这非常有趣。我觉得那一年的神经科学让我对什么是困难有了一些感觉，但对什么可能奏效几乎没什么感觉。不过，我当时算是借着神经科学的名义，在 UCL 盖茨比研究所（Gatsby Institute）待着，有幸和一些非常棒的教授一起做 AI 研究。所以我认为那是非常高效的一年 AI 学习，即使只是自学。

所以对你来说，主要是为了学习 AI？

没错。没错。我认为在英国，如果你在 20 世纪把某样东西称为 AI，你拿不到资助。但如果你把它称为脑科学，你或许有机会。所以 UCL 盖茨比研究所是一个顶级的 AI 中心，很多人从那里去了 DeepMind，包括 Demis 本人，那是一个非常棒的研究环境。我记得那些茶歇时的讨论非常精彩，而人们基本上就是在做 AI。它叫盖茨比计算神经科学研究所（Gatsby Computational Neuroscience Institute）。是的，事情是这样的：我当时在读神经科学硕士，然后很快意识到你需要杀老鼠，而我不想做这个。计算神经科学听起来更有吸引力，当你看到项目里有 Transformer（变换器）时，你会觉得，你绝对想做这个。

是的。我们都对此感到兴奋。

实际上，我先在法学院全职读了一年。哦，好的。因为 JD 博士项目的结构要求你有一整年的住校时间。那也是非常有趣的一年，学习了一些非常迷人的东西，比如刑法，研究凶杀案案例确实很刺激。不。

这是个好问题。我认为很多事情肯定是规定不足的。对于其他一些事情，我其实对从数学推理到这些特定领域的迁移学习感到相当兴奋。我认为上诉诉讼中的法律技巧，你能看到一些非常出色的上诉学者和律师，他们恰恰来自数学训练背景。比如 Laurence Tribe，哈佛法学院教授，是最强的上诉诉讼和最高法院简报撰写者之一，可以说是左翼民主党的大脑。我认为还有很多其他领域，比如反垄断法，非常流程化。合同法有时也很流程化。破产法、税法，更多偏向公司方面。我只是喜欢诉讼方面。我的意思是，是的。

有意思。实际上，既然我们谈到了诉讼，虽然不完全一样，但有一个 Erdős 问题，Axiom 遇到过。我不知道是不是 Axiom Prover 之类的。对吗？当时有一些争议，因为它声称解决了这个问题，但实际上证明已经被发现，只是被形式化了。

是的。实际情况是，我们的竞争对手 Harmonic 决定公开宣称他们解决了未解问题，Erdős 编号 124 和 481。然后我们相信了他们的文献综述，认为这些问题确实是真正未解的。我们当时是一家非常年轻的公司，想测试我们的系统能否尝试解决竞争对手能解决的问题。我们完全没想到它真的解决了。但结果发现，我们俩都错了，实际上这个问题之前已经被解决了。

我明白了。

所以这不是唯一一次我们依赖别人的文献搜索。而且，我们应该为此负责。另一次是关于一篇名为《平方自由行走中的死胡同》（Dead Ends in Square-Free Walks）的论文。Miller 教授提出的这个问题，结果发现也已经被解决了。但我们，我的意思是，我们真的应该做好自己的功课。就是这样。

我想表达的重点不是你们做错了什么，而是——

你知道，日本有个广告，一家公司，成百上千的人在广告里道歉，说"对不起，我们把价格涨了5分钱"。整个广告就是这个。我当时想，也许我也该这么做。这实在太尴尬了。

不，但我觉得信息溯源的问题，以及如何将答案与问题联系起来，这又回到了我之前问的那个问题。

对，这是个好问题。我觉得在Erdős那件事之后，我们变得极其谨慎，所以就没怎么去看其他Erdős问题。我相信Harmonix仍然声称他们解决了Erdős问题，但可能未必。我不确定。Terence Tao和其他很多人有一个数据库，记录了所有Erdős问题及其状态。其实这很容易犯错，因为很多Erdős问题确实已经被解决了。搜索和检索是个难题。你无法确定那个论证或它的等价版本是否已经存在。实际上，我觉得整个数据库最有趣的地方在于，很多问题并没有被直接解决，但可以通过另一个已解决或未解决的结果做非常简单的扩展，有时甚至是微不足道的扩展。有时候甚至根本没被解决。比如那个"无平方自由路径"的案例，和调和完备公理完全无关，我们当时没意识到。后来Kanasander Rajan教授向我和Miller教授指出，这其实来自一个Stack Overflow帖子。有个用户指出，1936年就有相关结果了。这很有意思。我觉得很难发现，因为搜索本身就是个难题。

那么，这个猜想引擎之类的工具，它的流程中是否使用了搜索？还是说，你们人类先做一部分，然后再输入进去？

我认为知识图谱或知识库是任何公司的重要组成部分。

对。

我觉得这方面讨论得还不够。

听起来你们不想透露太多细节，但你们有一个知识图谱。我还读到过，你们生成了一个非常庞大的Lean证明数据库，某种程度上算是合成数据。这可能是你们的竞争优势。

我觉得每个人都在努力积累数据，这不是模式问题，而是时间和时机问题。关键在于你能不能执行得足够快，以确保有某种缓冲，比如数据集积累带来的缓冲。但这只是缓冲而已。

这是个好问题。我觉得这确实是个很有趣的方法。我们相信，如果Axiom Prover能成为一个非常强大的数学家，那么它每天证明的东西应该能帮助它自我改进。这种自我改进的设计非常有价值。AI for Math社区里还有其他人在做类似工作。Gabriel Peresha教授的工作很有意思。还有一些偏向猜想型探索的工作。比如，我们可以改变某些特定方式，看看系统能否学会提出猜想并构建理论。

我觉得这个话题非常有趣且重要，因为你们声称，要达到超级智能，可能根本不可能。也许如果有无限资源，你可以用RL让它成功，但现实是，你无法做到样本高效，所以需要在推理过程中加入验证器，而不是只在训练过程中有验证器，推理过程中却没有。

是这样吗？我觉得很多人其实都在悄悄用这种方法来夯实推理。

是的。我本来以为，当O1即将发布但还没出来的时候，他们会宣布使用Lean来做形式化验证，生成证明并验证，从而夯实推理。那是我当时的预期。

Ilya还在的时候，有GPT-F，那是很棒的工作。还有MiniF2F。这些都是OpenAI的形式化数学工作。

好吧，那这些人应该还在做相关的事情。

不，他们都走了。

哦，他们都走了。

所以我的意思是，如果你是个初级技术人员，想花足够长的时间解决一个问题，奇怪的是，人们觉得初创公司跑道有限，随时可能崩溃。但在Axiom或其他新实验室这样的初创公司，你反而更有可能长期专注于同一个问题。

对，如果你认同公司的使命——

比在大公司好。

而不是有人决定你做的事不再重要了。

对，对。可能你的副总裁在政治斗争中输了。所以，是的。

对，完全同意。

不过，如果我们成功了，他们肯定又会开始做同样的事。

对。

然后作为人才，你也会有更多潜在的选择。

对。所以你的任务就是跑得快，让他们追赶不及。对了，我们还没聊到，你们最近发布了一个用于Lean验证的API。

对。

我实际上用Claude Code试了一下，因为比自己搭建Lean工具链容易。我试着让Lean证明一些东西。基础设施可能并不简单，尤其是在大规模场景下。你想聊聊这个吗？

是的，是的。所以我们刚刚发布了 Axle。A-X-L-E 代表 Axiom Lean Engine。它实际上是一套为 Lean 构建的证明验证和操作工具，使用 Lean 语言本身编写。所以这是一堆元编程工具。现在，元编程人才我认为极其难找。我们非常感激能拥有一支非常出色的团队在这方面工作。我们希望将其免费发布给社区使用，因为我们觉得可能还有其他人在进行大规模 Lean 操作，而这个工具能让他们的工作更稳健、更快速，并且能够规模化。Axle 目前包含大约 14 个这样的工具，从 Verify/Approve 开始，它用于确保没有异常情况，比如 Lean 代码中没有作弊行为。你不会引入公理，也不会假设奇怪的东西。如果你用公理 n n n，你可以证明 2 2 2，但这肯定不对。那不是正确答案。还有不少其他生成工具。例如，你可以尝试不同的修复方法。所以是坏的 Lean 代码输入，好的 Lean 代码输出。目前还有其他由 LLM 实现的修复方法。希望我们提供的这个工具能更便宜、更直接。我认为，强大且更好的工程可以带你走得很远。来自 LingQ 社区的很多人已经在使用 Axle，尽管才发布一周，用来做各种有趣的事情。我们看到区块链社区的人用它做有趣的事情等等。我们还听到很多人说 Claude 加上 Axle 是他们的首选配置。但目前，我们认为这些是非常有趣的工具。我记得今天有位数学家说，他用 Claude 证明了一个结果，大概是 Ramsey 结果，并形式化了 LIMB 证明，这也用到了 Axle 工具。所以我们很高兴看到人们已经在使用它了。

我觉得这是 Terence Tao 提到的协作的一个绝佳机会，一旦人们有了通用工具，事情就变得容易了。我的意思是，即使你像我一样不是很强的数学家，只要有直觉，也可能参与证明更大定理之类的努力。

是的，我觉得这个观点很有意思。想想看，数学一直不像软件工程那样协作性强。你不会看到成百上千人一起做一件事。Polymath 项目是一个例子，那很棒。所以如果你有很好的基础设施，真正普及了访问权限，那么大家都能参与进来。事实上，我认为一些大型形式化项目就是这样完成的。事情被分解成子任务，但真正重要的是像 Terence Tao 和 Alex Kondorowicz 那样的蓝图编写过程，他们把任务分配给不同的人，并让各部分协调一致。蓝图编写部分极其重要。我记得有一家其他公司做出了关于球体填充的结果。8 维部分的蓝图基本上还是基于球体填充社区、Lean 社区和人类编写的蓝图。他们其他一些结果也是如此，蓝图部分仍然是人工生成的。我认为自动生成蓝图将是一个技术瓶颈，很多人都在同时尝试解决。

那么，像我这样的 Claude Code 用户，尝试证明一些小引理之类的东西，即使我对数学没有深入理解，只有高层次的理解，这有价值吗？

这取决于你。你是想形式化，还是想证明？证明新东西。

说得好。

是的。

是的。所以可能形式化——你显然会从形式化开始，对吧？你脑子里已经有了证明。但没人能正确完成形式化。

我确实见过有人用 Lean 和形式化来学习数学，他们手动操作，不使用任何 AI。不，那是自动形式化。你没有那个过程。这很有趣，因为我很多开始研究 Lean 和 Mathlib 的朋友，是因为他们在读博士，问题真的很难。我们经常卡住，想复习一些本科课程，那时我们还能理解数学是什么，于是通过做 Lean 来学习。我觉得这很美。那些材料。是的。但如果你有像 Action Prover 这样的工具，它能形式化所有未形式化的东西，那么你就失去了学习过程中的那部分。是的，是的。但我确实认为，比如你和我，我们可以设置 Axle，看看能证明什么结果。我觉得这很有趣。而且多亏了 Axle 让速度大大提升，你不需要等很久。我记得 Pandem 考试那天，我们都在作战室。那是个周六，我们都很兴奋。我们刚拿到官方机构监考人员发来的 Pandem 考试试卷。我们看着 Axle 的工作量。没有它，我们不可能在时限内解决 8 道题，绝对不可能。我认为这些工具的一个有趣之处在于，它们可能为强化学习提供有趣的奖励。

你指的是什么？

例如，验证证明可以作为奖励，只要证明完全正确并通过验证。我明白了。我认为形式验证工具是强化学习的一个有趣方向。

是的。所以你的意思是，比如，你形式化、自动形式化非形式证明，然后验证，再将其用作奖励？还是说——

不，我的意思是，你把 Lean 程序输入这些形式工具，然后会得到一个分数。

好的。是的。我想如果我要构建 O1 之类的东西，我会用我刚才描述的方法，但你说的是仅仅学习如何做 Lean 本身。

当然，当然。关于 Frontier Lab 的价值主张，有趣的是，假设你是一个面向消费者的企业，那么你当然可以不做我们正在做的事。我们看到过 Deepseek 的例子，他们最初有一个形式化团队，后来因为战略方向变化解散了。这完全合理。现在假设你专注于编码，并且有想从事我们这项工作的人才。那么你更合理的做法是做代码生成，强化你的优势和护城河。你可以与 Axiom 合作，就像 Frontier Labs 与专注于搜索的初创公司（如 Ixa 和 Parallel）合作一样。直接调用 Ixa 的 API 进行搜索，而如果你是一个前沿实验室，我认为你应该调用 Axiom 的 API 进行验证。

是的。

更好的选择。

搭建自己的基础设施。

那没有意义。我的意思是，考虑到人才、Lean 的精细性、数据代码等方面，没有理由这么做。

是啊，我花了五分钟就搭好了。

我学数学的时间并不长。我觉得差不多一读博就开始筹钱了。所以并不是——

对。

对，对。所以，法学院那一年，对吧？从知识层面来说，它非常非常吸引我，但那也是我人生中第一年完全没有接触科学、技术或数学。那是很奇怪的一年，对吧？我读了很多书，在练习写作，学习阅读。但与此同时，我又想沉迷于技术领域的东西。那一年我脑子里一直有这个念头。所以，对，法学院那一年，对吧？它对我来说非常非常有趣，因为我觉得，好吧，我需要沉迷于某个技术问题，否则我会——我不觉得是无聊，因为我真的很喜欢法律的一切。我真的很喜欢它。学习法律本身非常有意思。但我基本上一直对推理的进展感到非常兴奋。我看了很多 post-training 类的论文，全是自学。然后到了某个节点，我觉得这一定会发生。而且，和 Shubo 聊天，对吧？每个周末都聊。这也没能平息这个想法。所以我越来越沉迷。到了某个时候，我觉得，好吧，如果我每分每秒都在想这件事，没法想别的，那我必须做点什么。我疯狂地爱上了“AI 会做数学”这个想法。然后，好吧，我现在要做数学吗？这真的很疯狂。我记得当时那种沉迷——我完全无法摆脱。后来我去了一个 NYU SC Scholar Dining House 的晚间活动，他们经常办各种免费午餐讲座。那些活动很棒，因为你能吃到免费食物，还能接触到有趣的知识。我记得 Julie Zhuo，她好像是 Facebook 的第一位产品经理，来做了演讲。之后，我直接走过去问她：如果你既想做创业，又想做学术，因为你有点喜欢数学，你会怎么办？她问我，你在这两件事上分别花了多少时间？我说，100% 和 0%。然后她说，那你得跟着你的精力走。

是啊，如果你完全沉迷其中。

对，我完全沉迷其中。我觉得它会变得很庞大。而且我觉得，它必须是一个营利性的创业公司，因为它比医学突破要广泛得多。如果你考虑递归自我改进，以及那种更高层次的概念——你真的想要 AI 科学家，那么大规模推理会是其中很重要的一部分。现在，Cursor、Claude 和其他人的信念是，好吧，大规模迁移到编码，编码也能迁移到数学。我觉得这没错。只是，为什么不直接推动它呢？我不明白。你需要直接推动它。然后还有另一个想法，也许可以回到协作这个点上。验证传统上被认为是，好吧，有些行业有很多护栏。如果你在国防、军事领域工作，你需要满足很多准入门槛来达到那些严格的要求。所以验证是为封闭行业服务的。但我觉得，现在是第一次，验证过的 AI 是为了开放协作。无论是人机协作。在 Blueprint 之前，那是人人协作。而 Lean 是基础，是验证，是形式化语言。然后是人机协作，就像我们现在看到的，以及未来的 AI agent 之间的协作。所以我认为验证过的 AI 是为了开放性，不是为了满足封闭行业的要求。而且我觉得，验证不应该只是——我记得有篇文章说聊天机器人会胡编乱造，AI 是解决方案吗？抱歉，数学是幻觉的解决方案吗？对我来说，验证不是为了消除错误。验证是为了放大才华，复合才华。这又回到了协作的点上。就像 Ramanujan 成为一个更强的数学家。他本来就已经很强了，但验证帮助他扩展了才华，既向上扩展也向外扩展。所以验证——

严谨。

对我来说，验证不是为了消除错误和瑕疵，而是为了放大才华。第三点是，验证对我来说不只是谈论严谨。它实际上是关于性能提升。它不只是关于严格的要求和需要克服的障碍。而是实际的验证生成会让它变得更好。我认为这三点——最后一点是，很多人觉得你做验证是因为你不信任技术。这在普通大众中很受欢迎，包括我父母，他们会说，哦，我们做验证是因为技术会犯错。不，我们不认为验证是基于对技术的不信任。而是因为预期的快速指数级扩展，以及技术的部署和创造，技术的进步，才迫使和要求验证。

这很数学视角，对吧？因为你说证明驱动数学，对吧？很多数学都基于证明。而数学驱动了世界上很多科学和创新。数学的创新驱动了世界的创新。

但它甚至不需要经过——就“数学解决一切”这个说法而言，显然成立。我的观点是，迁移学习并不是——迁移学习是关于推动数学推理，它只是——所以这里大概有几种叙事。对一些人来说，你解决了数学，而数学是科学的基础。所以这实际上是“AI for Math”到“AI for Science”这个激进层面的叙事。我们实际上相信一般的迁移学习。我认为 Axiom 是在基础设施层。

你认为这只是第一步，对吧？基本上是为了解锁许多领域的能力，比如科学和法律？

是的。我认为——所以，又有几种信念。一种信念是，有数学，还有形式化验证的力量。假设我们真的解决了数学，有了一个非常强的非形式化数学推理引擎，我们不期望这个时间会像通过形式化方式解决数学那么长。为什么？代码，作为一种语言，确实处于更结构化的那一端。

对。

它连接了非形式化和形式化。

对。

我们现在做的并不是非正式与正式的对立，对吧？我们并不是采用那种完全形式化的证明方法。它是在非正式与正式之间搭建桥梁，是在高层与低层之间建立连接。这是一种直接的、通过迁移学习来改进推理的方式，同时也是一种间接的方式——数学会解锁一些科学，确实如此。而这正是我们目前所看到的。

所以你认为它能实现迁移学习？

是的。

我明白了。

我认为这基本上是一个共识。我觉得这是共识，而且这个赌注在很大程度上被其他人忽视了，因为数学听起来很纯粹，似乎没有任何商业价值。当然，我显然理解其中的机会，比如如果你是一个前沿实验室，解决这个问题的机会成本。但我绝对认为，如果你是一个资源充足的初创公司，这个问题是你应该去做的。

这个观点很有意思。

是的，我觉得就像那个问题：Axiom 是做数学的还是做验证的？公司的 DNA 是数学。我们认为验证是最好的第一个市场。我们认为解决数学问题，尤其是形式化数学，将帮助我们实现验证型 AI 这个雄心勃勃的目标。当我们完成这个目标后，可能会有第二个市场，包括我们刚才讨论的 AI for science，但这是在理论层面，对吧？我认为现实世界的测试很重要，我们可能可以留在数字世界和软件领域，而其他事情则需要获取现实世界、物理世界的信号。

但你认为，一旦你拥有了那个强大的验证推理引擎，那种能够进行非常强大推理的能力，就是那个时刻——我们为软件验证、硬件等解锁了它。但现在，生物学呢？化学呢？

那可能是一个方向。另一个方向是，你离递归自我改进还有多远。

好的，所以就是 AGI？

是的，我认为存在这样一个问题，不同的人，因为背景不同，会有不同的看法——这实际上取决于你的精力和热情引导你走向何方。比如，有些人，我确实听朋友说过，他们想研究 AGI，因为他们相信解决 AGI 就能解决死亡。另一些人来自医学背景，他们真的相信可以解决死亡，而不需要解决 AGI。然后他们解决这个问题，他们只是解决 AI for science。是的。那么，哪种方式是正确的？我不知道。

所以递归自我改进的角度，听起来你是在说，验证加上那种非正式的语言，正是这种组合实现了非常好的递归自我——

我认为递归自我改进无论如何都会发生。我们试图让形式化验证占据一席之地。所以，形式化验证能否被欢迎、部署并成为共识，取决于我们执行得如何。我认为当你把这个问题归结为一个执行问题时，你就应该直接去做。

我认为我们处于一个市场，人们喜欢各自为战，比如 1000 个人，不联合起来，而是开始 1000 个项目。我认为这实际上是最大的泡沫指标。我认为有些类别是明显的泡沫，而有些类别则是登月计划。那不是泡沫，只是看起来有点泡沫化。在这个领域，如果那些真正有可靠背景的人决定为了使命而不是为了自我、为了创始人的地位而联合起来，组成团队，那么我对这个类别非常看好，反之亦然。所以我认为瓶颈实际上在于，这很烦人，因为如果你相信我们处于一个研究时代，如果你相信深度技术是值得追求的有趣方向，那么当前的市场条件既有好的一面也有坏的一面。好的一面是，它使得这些长期、长远的赌注能够获得资金。坏的一面是，市场上噪音太多，还有一些非理性的参与者。我们试图与非常出色的风投公司合作。他们是我们的合作伙伴，是我们的智力伙伴，我们有很多共识，我们会长时间地碰撞出非常酷的想法，无论是技术还是非技术方面的。我们花很多工作之外的时间，包括周末，一起真正地建设公司。但也有其他人只是想找个地方放钱。虽然我们不与他们合作，但这些市场条件鼓励了碎片化。当事情变得碎片化时，没有人能到达终点。我认为每个类别，无论想法多么正确，都基本上处于一个争取生存权的阶段。如果是这样，那么，比如伟大的深度技术公司 SpaceX，人们确实会联合起来为那个梦想而努力，可能在这种情况下，创始人也非常有魅力。我个人认为，一个非常令人担忧的问题是，对于其他一些我个人非常看好的类别，以及从整体上看，碎片化是一个问题。比如，我们看到教授被从大学里拉出来去做某件事，这确实是一个非常有趣的情况。

我认为碎片化是整个 AI 格局的瓶颈。

好的。

是的。我认为 AI for math 实际上不是一个泡沫的类别，因为它没有碎片化，因为真正优秀的人才确实喜欢联合起来。例如，让 Ken Uno 和 François Charton 加入同一个团队，这太棒了。你有一个核心贡献者，frontier math 第四层，非常出色的基准制定者，François，他从事 AI for mass 的证明和发现，他们一起工作，然后你突然就有了一个同时具备证明能力和构建能力的参与者。这太棒了。我相信，正如你所说，Harmonic 可能也有一些非常优秀的人才联合起来。我认为 AI for mass 是一个好的类别，因为它没有碎片化。但即使从我们的角度来看，比如 RL，对吧？我不认为那本身是一个类别，但 RL 人才目前对每个人来说都很难吸引和留住，有很多公司成立后三个月就被卖掉了。每个月你本可以花在解决技术问题上，却花在了交易上，这一个月就被浪费了。我这么说，也是带着一些痛苦和煎熬，因为我经历过两次融资。是的，是的，是的。

是的。

你是指Axiom，还是AI for Math这个领域？

针对AI for Math这个社区。

我预计随着Axiom和Harmonic确立品类领导地位，碎片化会开始出现。所以我觉得人们会……嗯，这是一方面。但我也认为另一个瓶颈可能是短期与长期之间的压力。我们现在做事节奏很快，但这并不意味着我们总能——或者说，以最快节奏做事总是正确的。我们之所以快节奏，是因为我们是在国际数学奥林匹克竞赛（IMO）当天成立的，所以无论如何都没法参加那届比赛。下一场数学竞赛是Putnam，我们很兴奋，因为那是本科生级别的考试。而今年的IMO（2025年IMO）在MOHS难度标尺上相对简单，Putnam可能会很难。事实上，它在MOHS标尺上比IMO更难。如果你看AI的表现，无论是平均得分还是问题最大难度，Pandemic在两个维度上都更难。所以我们想尝试一下。虽然只有4个月的时间差，但这并不意味着我总是设定4个月的目标。如果我建一家公司只设4个月的目标，我可能会打造一家非常短视的公司。所以我认为存在更长周期的问题。比如，市场力量可能迫使其他玩家进入芯片验证领域。代码验证有可能是圣杯。如果你解决了它，那么你自然也能在一定程度上解决芯片验证，只需考虑分布偏移等小问题。但我坚信，一个瓶颈可能就是这种压力。不过我认为Axiom很幸运：第一，我们起步够早；第二，我们团队由一群高度自主的人组成，执行力通常超出预期。但我认为，整个AI for Math领域可能的一个瓶颈是，试图证明商业价值会严重分散对核心能力提升的注意力。

是的，有道理。谢谢你开车过来见我们。

非常感谢。

我知道交通很糟糕。是的，谢谢。和你交谈真的很愉快。我们期待看到事情的发展。

是的，非常感谢。谢谢。

谢谢。谢谢。是的。