翻译自然杂志的2023年文章:HOW WILL AI CHANGE MATHEMATICS?

Nature | Vol 615 | 2 March 2023 | 15

由Davide Castelvecchi撰写

随着聊天机器人兴趣的迅速蔓延，数学家们开始探索人工智能（AI）如何帮助他们开展工作。研究人员表示，无论是协助验证人类撰写的工作还是提出解决难题的新方法，自动化正在以超越简单计算的方式改变这一领域。

“我们正在研究一个非常具体的问题：机器会改变数学吗？”加拿大蒙特利尔大学的数论家Andrew Granville说道。今年2月，在美国加州大学洛杉矶分校（UCLA）举行的一个研讨会探讨了这个问题，旨在在数学家和计算机科学家之间搭建桥梁。“大多数数学家完全不知道这些机会，”该活动的组织者之一，位于美国匹兹堡卡内基梅隆大学的计算机科学家Marijn Heule说道。

2018年菲尔兹奖得主、现就职于新泽西州普林斯顿高等研究院的Akshay Venkatesh，在去年10月为他举办的专题研讨会上，率先发起了关于计算机将如何改变数学的讨论。另外两位菲尔兹奖得主，巴黎法兰西学院的Timothy Gowers和UCLA的Terence Tao，也在这场辩论中发挥了主导作用。

“现在，有像菲尔兹奖得主和其他非常著名的大数学家对这个领域感兴趣，这表明它现在以一种过去没有的方式变得‘热门’了，”伦敦帝国学院的数学家Kevin Buzzard说道。

人工智能方法

讨论的一部分涉及哪种自动化工具将最有用。人工智能主要分为两大类。在“符号”人工智能中，程序员将逻辑或计算规则嵌入到他们的代码中。“这就是人们所说的‘老式的好人工智能’，”位于美国雷德蒙德微软研究院的计算机科学家Leonardo de Moura说道。

另一种在过去十年左右变得极其成功的方法是基于人工神经网络的。在这种类型的人工智能中，计算机几乎从零开始，通过消化大量数据来学习模式。这被称为机器学习，它是“大型语言模型”（包括如ChatGPT等聊天机器人；见第20页）以及能够在复杂游戏中击败人类玩家的系统的基础, 或者预测蛋白质如何折叠。尽管符号人工智能本质上是严谨的，但神经网络只能做出统计猜测，并且其操作过程往往是神秘的。

德·莫拉通过创建一个名为Lean的系统，帮助符号人工智能取得了一些早期的数学成功。这个交互式软件工具迫使研究人员写出问题的每个逻辑步骤，直至最基本的细节，并确保数学是正确的。两年前，一个数学家团队成功地将一个重要但难以理解的证明——一个如此复杂，甚至其作者都不确定的证明——转化为Lean，从而证实了它是正确的。

研究人员表示，这个过程帮助他们理解了证明，甚至找到了简化它的方法。“我认为这比检查正确性更令人兴奋，”德·莫拉说。

除了使个人工作更容易外，这种“证明助手”还可以通过消除德·莫拉所称的“信任瓶颈”来改变数学家之间的合作方式。“当我们合作时，我可能不相信你正在做的事情。但证明助手向你的合作者表明，他们可以信任你工作的一部分。”

高级的自动补全

在另一个极端，是基于神经网络的大型语言模型，类似于聊天机器人。在加州山景城的谷歌，前物理学家伊桑·戴尔和他的团队开发了一个名为Minerva的聊天机器人，它专门用于解决数学问题。本质上，Minerva是消息应用中的自动补全功能的一个非常高级的版本：通过在arXiv存储库中的数学论文上进行训练，它学会了以逐步解决问题的方式写下答案，就像一些应用可以预测单词和短语一样。与使用类似于计算机代码的通信方式的Lean不同，Minerva接受问题并用会话式英语写下答案。“自动解决其中一些问题是一项成就，”德·莫拉说。

Minerva展示了这种方法的力量和可能的局限性。例如，它可以准确地将整数分解为质数——不能被均匀分割成更小数字的数字。但是，一旦数字超过一定大小，它就开始出错，这表明它并没有“理解”一般程序。

尽管如此，Minerva的神经网络似乎能够掌握一些一般技术，而不仅仅是统计模式，谷歌团队正在试图理解它是如何做到的。“最终，我们希望有一个可以与你一起头脑风暴的模型，”戴尔说。他说，这对于需要从专业文献中提取信息的非数学家来说也可能很有用。进一步的扩展将包括书籍研究以及与专用数学软件的接口。

戴尔说，Minerva项目的动机是看看机器学习方法可以推进到什么程度；一个强大的自动化工具可能会帮助数学家，最终可能会将符号人工智能技术与神经网络结合起来。

数学与机器

从长远来看，程序将继续作为辅助角色，还是能够独立进行数学研究？人工智能可能会变得更擅长产生正确的数学陈述和证明，但一些研究人员担心，其中大多数可能无趣或无法理解。在10月的研讨会上，戈尔斯表示，可能有办法教会计算机一些数学相关性的客观标准，比如一个小陈述是否可以体现数学的许多特殊子领域。“为了擅长证明定理，计算机必须判断什么是有趣且值得证明的，”他说。如果它们能做到这一点，那么人类在该领域的未来就不确定了。

德国亚琛工业大学的计算机科学家埃里卡·亚伯拉罕对数学家的未来更为乐观。“人工智能系统只有在我们编程让它变得那么聪明时才会那么聪明，”她说。“智能不在计算机里；智能在程序员或训练者那里。”

新墨西哥州圣菲研究所的计算机科学家和认知科学家梅拉妮·米切尔表示，在人工智能的一个重大缺陷——即无法从具体信息中提取抽象概念——得到修复之前，数学家的工作将是安全的。“虽然人工智能系统可能能够证明定理，但更难的是提出有趣的数学抽象，这些抽象首先产生了定理。”