数学家通过提出猜想并用定理证明它们来探索想法。几个世纪以来，他们小心翼翼地逐行构建这些证明，大多数数学研究人员今天仍然这样工作。但人工智能正准备从根本上改变这一过程。被称为“副驾驶”的人工智能助手开始帮助数学家开发证明——这真有可能在未来让人类回答一些目前超出我们思维能力范围的问题。
加州理工学院正在开发一种很有前景的人工智能副驾驶。它可以自动提出证明中的下一步，并帮助完成中间数学目标，从而帮助构建更大步骤之间逻辑上的连接组织。“如果我正在开发一个证明，这个新的副驾驶会为我提供多个前进的建议，”加州理工学院计算和数学科学教授阿尼玛什里·阿南德库马尔说。阿南德库马尔和她的团队在一篇最近的预印本论文中介绍了这款人工智能副驾驶，该论文尚未经过同行评审。她说，至关重要的是，这些建议“都将是正确的”。
这款副驾驶是一个大型语言模型（LLM），与 OpenAI 的 ChatGPT 和 Google 的 Gemini 背后的机器学习系统是同一种类型。虽然它的训练方式不同，但它也类似于 Google 的 AlphaProof 和 AlphaGeometry 2 的技术——这两者都在今年的国际数学奥林匹克竞赛（IMO）中生成了达到银牌水平的复杂数学证明，参赛者是世界上最优秀的高中生。尽管 LLM 可以生成在技术意义上是“胡说八道”的东西，但副驾驶的错误建议会受到检查和拒绝。在加州理工学院的副驾驶案例中，这要归功于人工智能运行的软件 Lean，该软件使用严格的数学逻辑来筛选有效陈述。
支持科学新闻报道
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻报道 订阅。通过购买订阅，您正在帮助确保有关塑造我们当今世界的发现和想法的具有影响力的故事的未来。
代码证明
在过去几年中，Lean 越来越受到一小部分但不断增长的用户群的欢迎。这款开源软件允许数学家通过编码输入他们的数学，这个过程被称为形式化。这样做有什么好处？它永远不会出错。在 Lean 和其他证明助手应用程序中，软件会自动检查数学陈述的准确性。这与传统的、所谓的非正式数学截然不同，在非正式数学中，审稿人和同事会费力地审核一页又一页的此类陈述。这个过程容易出现人为错误，并且会遗漏错误。
如果您正在 Caltech 副驾驶的帮助下编写证明，您可以单击一个按钮来请求新的 Lean 编程语言行，以表示您正在使用的数学。屏幕右侧将出现几个选项，阿南德库马尔称之为“策略建议”；然后您只需选择看起来最合适的选项。如果您的证明朝着具有明显或众所周知的中间结论的方向发展，副驾驶还可以建议如何完成该轨迹。
洛桑瑞士联邦理工学院和伦敦帝国学院的纯数学教授马丁·海雷尔说，“Lean 没有信任问题”，因为该软件会检查工作。尽管如此，许多学者尚未采用它。“它很难使用，因为你必须将所有数学都输入为代码，”海雷尔说。他指出，用 Lean 编码需要输入在撰写论文时会被省略的细节，因此可能需要多页代码来显示不言自明或显而易见的内容。
但海雷尔没有参与 Caltech 项目，他认为人工智能副驾驶最终会消除所有这些繁琐的工作。“一旦你提出了一个对大多数数学家来说显而易见的陈述，LLM 应该能够生成它的代码，”他说，并补充说，这种更快的流程“可能会吸引新一代数学家使用 Lean”。
阿南德库马尔也预测，更多的研究人员将接受形式化的人工智能辅助数学。“今天，当我与年轻的数学家甚至职业生涯早期的本科生交谈时，我看到他们熟悉这些人工智能系统，”她说。“他们会不惜一切代价让工作更快更容易，以获得竞争优势。”
数学变革
在国际数学界以有意义的方式采用人工智能工具之前，这些平台需要变得更加强大。凭借今年国际数学奥林匹克竞赛的银牌标准，谷歌的 AlphaProof 和 AlphaGeometry 2 已经显示出卓越的成果。但它们尚未达到研究数学家在复杂证明方面需要协助的水平；在这方面，人类仍然是更有能力的数学家。
然而，谷歌 DeepMind 强化学习副总裁大卫·西尔弗说，“很快就会有系统达到那个水平”。“我认为这基本上会将人类数学家提升到一个更高的水平，让他们能够以更高的水平进行操作和思考想法。”他说，数学正开始发生转变，就像电子计算器发明时一样。“在计算器出现之前，有大量的数学运算非常费力，需要花费大量精力，”他说。“我认为我们现在正处于证明的阶段，在未来，我们将看到非常复杂的证明被人工智能自动解决。”
通过人工智能协作
采用人工智能副驾驶也将改变数学家彼此合作的方式。通常，他们单独或小组运作。受信任的同事会逐个评估他们的证明。但形式化的人工智能助手可以使更大规模的人类合作者能够通过将最大的问题分解为子问题来解决它们。每个部分都将被分批分配给不同的专家人工智能-人类伙伴关系团队来解决。“数学被认为是一项非常孤独的事业，尤其是在大众媒体中，但现在看来人工智能将成为数学家之间协作的推动者，”阿南德库马尔说。
数学家普遍乐观地认为，人工智能副驾驶很快将为人类专家提供助力，使他们能够将时间投入到更复杂和更困难的问题中。例如，在未来几年，人工智能-人类伙伴关系可能会尝试解决臭名昭著的千禧年难题——甚至可能是像P 与 NP 这样具有挑战性的问题，这是一个理论计算机科学中长期存在的问题，它询问每个其解决方案可以快速验证的问题是否也可以快速解决。
“这就是我们很快将发现自己所处的位置，”西尔弗在考虑解决此类问题的概念时说。“像‘P 与 NP’这样复杂的问题——或者像它一样困难的问题——远远超出了我们今天的水平，甚至不知道如何开始，”他说。“但我可以想象，也许在三年左右的时间里，我们可能会朝着类似的方向前进。”