Axiom Math 希望让人工智能远离数学

感觉人工智能每周都在解决一个新的数学问题。上个月，OpenAI 发布了 719 份手稿，声称能够解决该领域一些最棘手的问题。甚至计算机检查也可能会出错。经过多年的人工智能衰退，我们有理由怀疑数学是否会成为下一个。 Axiom Math 押注数学可以避免这种命运，不是放慢速度，而是立足更坚定。这家价值 16 亿美元的初创公司希望建立一个经过验证的基础，让人工智能代理可以依赖它来编写软件并最终进行科学研究。周三，该公司宣布已正式验证 Stacks 项目，这是人类有史以来最大的数学体系之一。数学家们通常很少重视 Stacks——哥伦比亚数学家 Peter Woit 声称“没有其他东西可以真正与之相比”，并将该项目与“著名的布尔巴基书籍”进行比较，该系列书籍在 20 世纪重建了数学的基础。 Woit 的哥伦比亚同事 Johan de Jong 于 2005 年启动了 Stacks 项目，作为开源参考。从那时起，数学家们就为它做出了贡献，从大学水平的代数一直到代数、几何和数论领域最先进的思想。该公司的人工智能代理团队将图书馆的大约 7,654 页翻译成大约 1600 万行计算机检查的代码。形式化数学是确保其底层结构健全的一种方法。数学家用一种名为 Lean 的编程语言将证明重写为代码，然后由一个名为证明助手的程序逐行检查代码。如果证明通过，数学家就可以相信它在逻辑上是合理的。工程师们使用相同的想法（称为形式验证）来确认他们的芯片设计是否有效，而法国的研究人员则使用它来捕获计算家庭福利的软件中的错误。对于像 Stacks Project 这样的库，检查每个定理只是工作的一部分。 Stacks 中的定理和定义是相互关联的，每个定理和定义都建立在前一个定理和定义的基础上。就像家谱一样，Stacks 中的许多结果都可以追溯到它之前的结果。这种相互关联性让 Axiom 不确定该项目一开始是否可行。该团队必须在大约 1600 万行精益代码中保持每个连接完好无损。 Axiom 首席执行官 Carina Hong 向 TechCrunch 表示：“生活中的大事和微妙的事情是不能并存的。” “[Stacks] 是数学结果的集合，是数学的基础。你希望 [定理] 是一致的，而不是自相矛盾的。你希望定义不会相互冲突。”这位 25 岁的首席执行官从斯坦福大学数学博士项目退学，并于 2025 年 3 月创立了该公司。3 月，Axiom 筹集了由 Menlo Ventures 领投的 2 亿美元 A 轮融资。 “我们不确定氛围编码是否能够保留 Stacks 的美丽，”洪说。为了完成该项目，该团队为其代理提供了松散的结构，并让他们并行运行。 Axiom 技术人员 Ashvin Swaminathan 表示：“通过 Stacks，我们强加了一个等级制度……但它并不是一个完整的等级制度，规定每个代理的行为。” “代理们正在为自己寻找任务，并确定他们可以并行处理的事情。” Axiom 还训练了自己的模型，使其擅长数学，洪说，大多数其他验证初创公司都没有采取这种方法。起初，该团队依靠一位内部精益专家来向代理传授人类的味觉。洪说，随着时间的推移，代理商们已经逐渐掌握了自己的品味。这一结果填补了形式化数学中最大的空白之一。 “当你观察数学中形式化的内容时，就会发现这个巨大的黑洞。这个黑洞涵盖了代数几何，”斯瓦米纳坦说。斯瓦米纳坦说，到目前为止，想要用 Lean 检查代数几何新工作的研究人员几乎没有什么基础。 “嗯，现在他们做到了。” Axiom 认为，每个经过验证的结果都会成为一个构建块，因此未来的证明可以依赖于经过检查的数学，而不是从头开始。加州大学洛杉矶分校数学家、菲尔兹奖获得者陶哲轩将一般情况变得更加简单：“你拥有的形式化证明越多，你就能做出越形式化的证明。”数学家并不是 Axiom 的唯一目标受众。开发人员长期以来一直在努力保证他们的代码没有错误和安全漏洞。随着人工智能代理编写更多的世界代码，这个问题变得越来越严重。 Axiom 认为，未来的软件将需要建立在经过验证的基础上，就像 Stacks 现在所做的那样。 “我们相信数学是你开始构建这些东西的领域，并且它是一种可转移的技能，”斯瓦米纳坦说。 “代理可以阅读我们的代码，理解它，并在其之上构建新的基础设施。我们的精益形式化现在是代理可以构建的基础。” Axiom 的代理构建 Stacks 的方式是并行工作并选择自己的任务，这是 Hong 对 A 的期望