数学家的最新助手是人工智能

人工智能与人类的合作可能在数学领域实现超人的伟大

数学家通过提出猜想并用定理证明来探索思想。几个世纪以来，他们逐条仔细地建立了这些证明，并且大多数数学研究人员今天仍然这样做。但人工智能有望从根本上改变这一过程。绰号为“副驾驶”的人工智能助手开始帮助数学家开发证明，这很有可能有一天让人类回答一些目前我们无法解决的问题。

加州理工学院正在开发一种有前景的人工智能副驾驶。它可以自动提出证明中的后续步骤，并帮助完成中间数学目标，帮助在较大步骤之间建立逻辑结缔组织。“如果我正在开发一个证明，这位新副驾驶会给我提供多种前进建议，”加州理工学院计算和数学科学教授 Animashree Anandkumar 说。阿南德库玛 (Anandkumar) 与她的团队一起展示了人工智能副驾驶最近的预印本论文，尚未经过同行评审。她说，最重要的是，这些建议“都是正确的。”

副驾驶是一个大型语言模型 (LLM)，它与 ​​OpenAI 的 ChatGPT 和 Google 的 Gemini 背后的机器学习系统相同。虽然它的训练有所不同，但它也类似于为 Google AlphaProof 和 A​​lphaGeometry 2 提供支持的技术，两者都生成了复杂的数学证明银牌是今年国际数学奥林匹克 (IMO) 世界上最优秀高中生的标准。尽管法学硕士可以产生技术意义上的“废话”副驾驶的错误建议会被检查并拒绝。就加州理工学院副驾驶的情况而言，这要归功于人工智能运行的软件 Lean，它使用严格的数学逻辑来筛选有效的陈述。

关于支持科学新闻

如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻事业订阅。通过购买订阅，您将有助于确保有关塑造当今世界的发现和想法的影响力故事的未来。

代码证明

在过去的几年里，精益在一小部分但不断增长的用户群中变得越来越受欢迎。该开源软件允许数学家通过编码输入数学，这一过程称为形式化。有什么优势？这永远不会错。在精益和其他证明辅助应用程序中，软件会自动检查数学语句的准确性。这与传统的所谓非正式数学截然不同，在传统数学中，审阅者和同事会煞费苦心地审核此类陈述的页面。这个过程很容易出现人为错误，并且错误会被遗漏。

如果您正在加州理工学院副驾驶的帮助下编写证明，您可以单击一个按钮来请求 Lean 编程语言的新行来表示您正在使用的数学。Anandkumar 称之为“战术建议”的几个选项将出现在屏幕的右侧；然后您只需选择看起来最合适的选项即可。如果你的证明朝着具有明显或众所周知的中间结论的方向发展，副驾驶还可以建议如何完成该轨迹。

洛桑瑞士联邦理工学院和伦敦帝国理工学院的纯数学教授 Martin Hairer 表示，精益“不存在信任问题”，因为软件会检查工作。尽管如此，许多学者尚未采用它。“它很难使用，因为你必须以代码的形式输入所有数学内容，”海尔说。他指出，精益编码需要输入撰写论文时会省略的细节，因此可能需要多页代码才能显示不言而喻的真实或明显的内容。

但未参与加州理工学院项目的海勒相信，人工智能副驾驶最终将取代所有繁重的工作。“一旦你提出了对大多数数学家来说显而易见的陈述，法学硕士就应该能够为其生成代码，”他说，并补充说，这个更快的过程可能“可能会吸引新一代数学家”精益。

阿南德库马尔也预测更多的研究人员将接受正式的人工智能辅助数学。“今天，当我与年轻的数学家甚至职业生涯早期的本科生交谈时，我发现他们对这些人工智能系统很熟悉，”她说。– 他们将尽一切努力让工作更快、更容易，从而获得竞争优势。”

数学变换

在国际数学界以有意义的方式采用人工智能工具之前，这些平台需要变得更加强大。凭借今年 IMO 的银牌标准，Google 的 AlphaProof 和 A​​lphaGeometry 2 表现出了非凡的成果。但它们还没有达到研究数学家需要帮助进行复杂证明的水平；从这方面来说，人类仍然是更有能力的数学家。

然而，谷歌 DeepMind 强化学习副总裁 David Silver 表示，“很快就会出现接近这一水平的系统”。“我认为这将从根本上将人类数学家提升到一个能够在更高水平上进行操作和思考想法的地方。”他说，数学正在开始转变，就像电子时代那样计算器被发明了。“在计算器出现之前，数学的范围很广，需要付出很大的努力，”他说。“我认为我们现在正处于证明的阶段，将来我们将看到人工智能自动解决非常复杂的证明。”

通过人工智能进行协作

采用人工智能副驾驶也将改变数学家之间的合作方式。通常，他们单独或以小组形式行动。值得信赖的同事逐一评估他们的证明。但正式的人工智能助手可以让更多的人类协作者群体通过将最大的问题分解为子问题来解决这些问题。每个部分都将分批由不同的专家人工智能与人类合作团队来解决。“数学被视为一项孤独的事业，尤其是在大众媒体中，但现在看来人工智能将成为数学家之间合作的推动者，”阿南德库马尔说。

数学家们普遍乐观地认为，人工智能副驾驶很快就会给人类专家带来助力，让他们能够将时间投入到更复杂、更困难的问题上。例如，在未来几年中，人工智能与人类的合作伙伴关系可能会尝试解决众所周知的困难的千年奖问题，甚至可能是像这样具有挑战性的问题P 与 NP，这是理论计算机科学中一个长期存在的问题，即是否每个可以快速验证其解决方案的问题也可以快速解决。

“这就是我们很快就会发现自己要去的地方，”西尔弗在考虑解决此类问题的想法时说道。“像“P 与 NP”这样复杂的问题，或者一些困难的问题，远远超出了我们今天的水平，甚至不知道如何开始，”他说。“但我可以想象，也许在三年左右的时间里，我们可能会实现这样的目标。”