一家新AI公司用数学新方法解决了4个长期未解的难题

陈（Chen）最近花了数小时向ChatGPT提问，希望借助人工智能找到一个尚未解决的数学难题的解法，但并未成功。上个月，在华盛顿特区一场数学会议的招待会上，陈遇到了知名数学家肯·奥诺（Ken Ono）。奥诺刚从弗吉尼亚大学离职，加入了由他的学生卡琳娜·洪（Carina Hong）联合创办的人工智能初创公司Axiom。
陈向奥诺讲述了这个难题，第二天早上，奥诺就借助其初创公司的数学解题AI——AxiomProver，为他呈现了一个证明。“从那以后，一切都水到渠成了。”陈说。他与Axiom合作撰写了这一证明，目前已发布在学术论文预印本平台arXiv上。
Axiom的AI工具发现了该难题与19世纪首次研究的一种数值现象之间的联系，随后设计出证明，并进行了自我验证。“AxiomProver发现的东西是所有人类都忽略了的。”奥诺告诉《连线》杂志。
这一证明是Axiom称其系统近几周内解决的多个未决数学问题之一。虽然该AI尚未解决数学领域中任何最著名（或最有价值）的难题，但它已经找到了困扰不同领域专家多年的问题的答案。这些证明证明了AI的数学能力在稳步提升。近几个月，已有其他数学家报告使用AI工具探索新想法和解决现有问题。
Axiom开发的技术可能在高等数学领域之外也有用武之地。例如，同样的方法可用于开发对某些网络安全攻击更具抵御能力的软件，这需要利用AI来验证代码的可靠性和可信度。
“Axiom的首席执行官洪表示：‘数学确实是现实的绝佳试验场和沙盒。我们坚信，这里有很多具有高商业价值的重要应用场景。’
Axiom的方法包括将大型语言模型与名为AxiomProver的专有AI系统相结合，该系统经过训练，能够通过推理解决数学问题，得出可证明正确的解决方案。2024年，谷歌通过名为AlphaProof的系统展示了类似理念。洪表示，AxiomSolver融合了多项重要进展和更新的技术。
奥诺说，针对陈-金德隆猜想的AI生成证明表明，AI现在能够切实协助专业数学家。“这是一种证明定理的新范式。”他说。
Axiom的系统不仅仅是一个普通的AI模型，它能够使用一种名为Lean的专业数学语言来验证证明。这使得AxiomProver不仅能检索文献，还能开发出真正新颖的解题方法。
AxiomProver生成的另一个新证明展示了该AI完全自主解决数学问题的能力。这一证明也已发布在arXiv的一篇论文中，它为费尔猜想（Fel’s Conjecture）提供了解答。该猜想涉及合冲（syzygies），即代数中数字排列的数学表达式。值得注意的是，这一猜想涉及的公式最早出现在100多年前印度传奇数学家斯里尼瓦瑟·拉马努金（Srinivasa Ramanujan）的笔记中。在这个案例中，AxiomProver并非只是填补了拼图中缺失的一块，而是从头到尾设计出了证明。
“即使是像我这样多年来密切关注AI数学工具发展并亲自使用它们的人，也觉得这非常惊人。”哈佛商学院教授斯科特·科米纳斯（Scott Kominers）说，他既熟悉费尔猜想，也了解Axiom的技术。“AxiomProver不仅成功全自动解决了这样的问题，还能即时验证，这本身就很了不起，而且它得出的数学结论还兼具优雅与美感。”
Axiom的AI生成的第三个证明涉及数论中所谓“死胡同”的概率模型。第四个证明则借鉴了最初为攻克并最终解决费马大定理（数学领域最著名的难题之一）而开发的数学工具。
奥诺表示，他希望AxiomProver不仅能协助数学家工作，还能揭示关于新发现如何产生的更基本规律。“我感兴趣的是，能否让这些‘顿悟时刻’变得可预测。”他说，“而且我也从中学到了很多关于自己当初是如何证明一些定理的。”
最近亲眼见证自己的猜想被Axiom解决的陈表示，他对AI将对其领域产生的影响持乐观态度。“计算器发明后，数学家并没有忘记乘法表。”陈说，“我相信AI将成为一种新颖的智能工具——或许称之为‘智能伙伴’更恰当——为数学研究开辟更丰富、更广阔的视野。”