陶哲轩：当今AI的真实数学水平冷眼贱客

日前，著名数学家陶哲轩教授在他主持的UCLA IPAM研究所举办的AI for Science论坛中做了一个演讲，其中对当今AI真实的数学水平，数学研究形式的演进等话题提供了他的独有的当今顶级数学人脑的独到见解和深刻洞察。

我今天将谈谈数学研究正在发生的变化。

现在，我们已经看到了，过去几年里，人们对人工智能和其他工具的关注度不断提升，人工智能和其他工具在数学和其他任务中变得越来越强大。但我认为一些真正的变化终于将会在今年开始发生。说实话，数学确实早就应该进行一些改革了。因为在很多方面，我们是一个极其保守的领域，不是政治意义上的，而是实践意义上的。我这里举两个例子。这是一本Cauchy在200年前写的回忆录，介绍了大部分基础复分析，比如Cauchy积分公式。这本书是用法语印刷的，而不是用现今流行的编排数学公式的软件LaTex写的。但除此之外，它几乎和你今天看到的复分析教科书一模一样。在过去200年里，我们教数学的方式只是在一些次要方面有所改变。一个学习数理工程学科的研究生基本上会认出这本书里的所有内容。而且我们仍然非常依赖黑板，你可以看到，我们几乎是唯一一个仍然在主要使用黑板的学科。

从这两个例子可以看出，我们数学家的确有点不寻常。比如，我们合作不多，至少直到最近才开始合作。如果你去看过去几十年中数学、化学和物理等学科顶刊论文的合作作者人数，数学论文的合作者人数几十年来一直停留在一两个。而其他学科的研究者们已经开始意识到，现代研究任务实际上需要广泛的合作和非常多元化的人员，并已经付诸实践。你可以从其他学科论文合作者数量的稳步增加认识到这点。而我们还没有真正做到这一点，所以我们有点错失了科学研究规模化或者产业化的机遇。这其中在我看来是有多重原因的，这不仅仅是因为我们数学家大多生性内向，有点不善交际。而真正主要的原因是：第一，数学的准入门槛很高。比如一个数学问题，你通常需要一个数学博士生才能理解问题的真正意涵是什么。第二，数学证明的标准非常高，当我们想要证明某些东西时，我们希望每一步都绝对正确。所以如果你和10个人合作，其中一个合作者不可靠，而且提出了不可信的论证步骤，那么每个人都必须验证其他人的论证。这将非常繁琐，但是否则的话你的整个证明就会被认为是垃圾。第三，我们很多工作流程无法扩展。黑板在只有两三个人的时候很好用。尤其是和一位与你心意相通的人一起在黑板前解决问题，这真是一种很棒的体验。但是，当有20到50个合作者一起解决问题时，如果他们恰好又分散在不同的国家等等，我们是无法真正通过Zoom解决问题的，它行不通。所以，我们之所以没有像其他学科那样与时俱进，是有原因的。

但我认为随着科技的发展，这种情况将会改变。我们终于会在一两年内开始开展大型的数学研究项目。在实验科学中，存在着案例研究和对特定对象进行非常深入细致的分析之间的区别。这算是数学中比较常见的做法。你会选取一个数学问题或一个数学概念，然后仔细研究它。但也还有像人口调查这样的工作，比如选取一个物种或其他物种的1000个成员进行数据分析和统计，了解有多少百分比的成员会做这件事，有多少百分比的成员会做那件事。而我们在数学中并不做这些。因为我们一直没有工具，使我们能够系统地研究大量问题。直到现在，我们才开始认真考虑进行广泛参与的研究方式。在其他一些科学领域，有时会有公民科学。你可以让业余爱好者收集蝴蝶标本、识别彗星、采集水样等等。即使数据质量达不到100%的科学标准，也有办法让我们继续研究。只是要稍微处理一下那种略有点噪声的数据。直到最近，我们还无法在数学研究领域做到这一点。除了少数几个孤立的项目，比如寻找大素数之类的，业余人士也能做到。其他真正的难题攻坚，你还是没有办法让业余人士参与进来。但是现在我们也开始能做到了。因此，我们开始开展一些项目，其中许多贡献者并非专业数学家，而是研究生、高中生，计算机科学或科技行业的人，他们有一些空闲时间，也愿意参与。所以我们正在寻找一些项目，在这些项目中，很多人可以有趣的方式做出贡献，当然还有人工智能。人工智能发展非常迅速，现在真的可以帮助这些项目实时运行，并且以节省时间的方式而不是浪费时间的方式，我们已经跨越了这个交叉点，使得规模化、人工智能和广泛参与数学研究项目成为净收益的活动。因为我们还有一个秘方，使这一切奏效，就是形式化验证。我们现在有很多办法可以自动检查某个论证是否正确。所以，即使很多来自人工智能、公众或大型项目的贡献数据不可靠，我们也有办法过滤掉不可信的输入，保留有价值的输入，这已经产生了巨大的影响。

我已经就这个话题讲过好几年了，我通常会具体指出一些人工智能或神经网络或其他技术取得一些进展的具体例子。正如我所说，我们现在正进入规模化的时代。所以我再来谈谈一个众筹数学研究的案例。我把它称之为案例研究，而且它最近在社交媒体上引起了热议，那就是Erdős问题集。它算是第一个大型数学问题数据集，我们可以应用所有这些工具，并了解哪些工具有效，以及它们的优势和劣势是什么。Erdős问题集包含大约一千三百多个问题，Thomas Bloom大约在三年前创建了一个网站，系统地收录了这些问题。Erdős是20世纪一位非常多产的数学家，他发表了超过1500篇数学论文，我认为这仍然是记录。而且他与各界人士都有合作。他没有和我合作，但是我10岁的时候见过他。他喜欢提出问题。所以当我见到他的时候，他基本上就是给了我一个问题，我们一起研究。那个问题我们当时没解决，后来其实已经解决了。但他非常喜欢提出问题来鼓励大家对他所推广的那种数学感兴趣。所以他不仅因为他的研究而闻名，还因为不断提出问题。他甚至还为其中一些问题设立了现金奖励。大多数奖励只有50美元或20美元，没什么特别的。但也有一些问题真的相当有影响力。

这是他早期提出的问题之一。问题本身是什么并不重要。但就本次演讲而言，它一直是影响最大的问题之一：一个集合需要多大才能证明它具有等差数列？他为此设立了最高奖金之一，5000美元。这个问题目前仍未解决，但我研究过这个问题的许多方面。有很多关于这个问题的部分成果，这些成果本身也发表在顶级期刊上。这是一个非常有影响力的问题。他很擅长提出非常好的问题，这些问题并非不可能，也并非微不足道，而是处于临界点，他知道任何进展都将是有趣的。所以Erdős把这些问题称为“橡子”，需要深刻而微妙的新见解，才能长成参天大树。然而，他提出了上千个问题，当然它们并非都是“橡子”。有些问题被最终发现实际上非常简单。比如他提出的另一个问题：方程：n！= xk ± yk，没有整数解。有点类似费马大定理类型的问题。结果Jonas Barfield发现了一个反例：10! = 484 − 364。Erdős其实知道这一点。所以他把这些问题称为棉花糖，就像美味的点心，带来短暂的快乐。所以这是一系列非常多样化的问题。

我应该先声明一下。因为最近在社交媒体上，某家人工智能公司声称他们解决了五个问题，而某家人工智能公司声称他们解决了六个。并暗示人工智能工具已经达到了专业数学家的水准。所以，我想先说明一点：解决问题只是数学研究的一个方面。我们也对理解概念、交流和简化事物感兴趣。我们解决问题的原因，与其说是因为问题本身有很多应用，不如说是因为寻找解决方案的过程常常会发现新的方法。很多Erdős问题都催生了新的技术。比如，研究Erdős等差数列的问题，就催生了组合运算的新领域。所以，关键不只是找到解决方案，而是找到解决方案后通常会伴随而来的一切。

Erdős问题集有超过千个，有些已经解决，有些尚未解决。对计算机科学家来说，这看起来很像一个基准测试。即使它不是基准测试，但它已经成为一个非常诱人的目标，因为你可以衡量，比如，你的新AI工具能解决多少问题。所以我认为这是一个很好的数据集，可以用来了解这些工具目前所处的状态。然后，你可以开始进行比较测试，看看哪些AI使用方法比其他方法更有效。如果你只研究一两个AI已经解决的问题，那就很难看出哪些问题更有效。但是，我们有上千个问题，我们可以开始进行数据分析之类的工作。基于最近有很多炒作，我应该马上说明一下。尽管早期问题集中存在一些重要的问题，但人工智能目前还没有真正在最受瞩目的问题上，也就是数学家们最想解决的问题，取得实质性的进展。迄今为止，它解决的问题都是那些受注意力瓶颈限制的问题，也就是Erdős在一篇论文中提出过一两次的问题，但几乎没有后续文献，没有人真正研究过这些问题。但是人工智能容易扩展。所以我们正在清理，在很多我们之前没有得到足够人类关注的问题上取得进展。即使有这么多炒作，AI的数学能力也确实有了非常明显的提升。这绝非炒作。对我而言，这些进展表明，数学研究还有另一种互补的方法。传统上，人类以小组形式花费数月时间解决难题，而且我们还会继续这样做。但我们现在也可以设置人工智能，让它能够巡视处理上千个问题，并尽可能快地完成所有容易解决的问题。检视所有可能的解决方法，比如他们可以使用 20 种不同的技术，将它们全部应用于1,000个问题，看看哪些问题可以用这些方法解决。这就是目前AI在数学领域的能力上限。

我们来进行统计汇报：我们处理这些问题的进展如何？我可以给你一些图表。我们从去年9 月开始跟踪这些数据。现在，在一千多个问题中，有 699个问题尚未解决。这里之所以出现一个很大的跳跃值，是因为Thomas在那个时候发现了一大批新的Erdős问题，大概有 50 个左右，他把它们添加进去了。那么，有多少问题被解决了？大约480个。而且随着时间的推移，被解决的问题数目一直在稳步增长。你可能已经注意到，人工智能在这个时候开始取得重大进展。实际上，深度文献检索技术出现后，这里也出现了一个激增。人工智能研究工具发现了大量文献中已有的解决方案，但我们还没有记录下来。所以，已经解决的问题数目出现了一个早期激增，然后出现了加速增长，到目前已经进入平台期。过去几周，我认为进展不多。此外，我们还在形式化许多解决方案方面取得了进展。所以不仅已经解决了很多问题，而且我们实际上已经开始用Lean语言将它们形式化。

所以我们已经让AI的数学研究工作开始取得进展。有些进展现在看有点平淡无奇，但在六个月前这都是很了不起的结果，而现在我们觉得它很平淡。就好比网络搜索，我记得在Vista系统出来之后，谷歌在2000年代出现了，当时我的下巴都惊掉了，它有多么神奇，我都可以瞬间访问整个互联网了。我们现在只是把它视为理所当然。所以六个月前，这些深度研究的工具出现了，你可以让人工智能搜索各种文献，找到与你的问题相关的冷僻晦涩资料。比如说，有一篇1970年的论文，用一种不同的语言，通常是字面意义上的，但属于不同的领域，它解决了这个问题，只需稍作修改，就可以用来解决我手头的问题。所以我们现在基本上有了我们多年来一直想要的语义搜索。它们仍然偶尔会出现错误的参考文献，但至少通过文献检索，你可以去检证原始资料。20到30多个Erdős问题都是这样解决的。

现在使用人工智能生成代码和数值数据非常容易。你可以做更多数值生成实验，而且我们现在可以更快地形式化。因为以前将非正式证明翻译成形式化证明并进行验证真的很繁琐，通常需要几周时间。现在人们可以在几个小时内完成。虽然不是每篇论文都这样，但是对于很多类型的文章来说都可以。这对于与人工智能合作至关重要。如果有人声称，我已经解决了这个问题，这里有一份人工智能生成的证明，大概有五六页人工智能生成的文本。里面通常有很多垃圾信息，而且没有人有时间去查看所有细节。如果我们现在可以自动将它们转换为形式化的证明，汲取那些有效部分，剔除那些无效部分。所以我们现在可以处理大量人工智能生成的一般的解决草案。这是一个典型的深度研究，至少有 20 个问题已经用这种方法解决了。

这是我最近写的一篇关于另一个 Erdős问题的论文。这篇论文我没怎么用到AI。我主要用 AI 来说服自己结果是正确的，我还用 AI 来画图。它们可以画出专业级的图表，比我自己用 Python 或其他什么工具瞎折腾要好得多，也快得多。就像这样的次要的事情而言，AI 基本上已经非常出色了。这个证明最早发表于大约 10 年前，是我最早解决的Erdős问题之一。之后我的证明被转换成了Lean语言。Lean语言看起来有点像数学和 Python 的混合体。对一个Lean这门语言的人来说，它们看起来有点冗长，不太精炼，但我认为这一点会得到改进，但也许这并不那么重要，因为在很多情况下，你并不真正关心证明有多么优雅，只要它能编译，能形式化，你就满意了。所以我们正在使用所有这些工具。

还有一件事，也是我们取得如此多进展的原因。就是我们现在有一个社区。Thomas确实非常努力地建立了一个社区，包括这个讨论论坛以及社区规则。重要的是，我们既不过度支持人工智能，也不反对人工智能。我们对人工智能持有中性的态度。我认为，使问题能够得到有效解决的原因在于我们欢迎人们贡献人工智能生成的解决方案，只要有一些规则。你必须披露，你不能只是发一长串文字然后声称这是人类想出来的，而实际上AI深度参与了其中，这是不对的。你必须总结，必须对内容负责。你不能只是刷屏，如果你有很长的内容想说，那就放个链接。所以，要有一些合理的规则。而且，它确实奏效了。所以在其他论坛上，确实存在一些担忧，担心会被人工智能生成的垃圾信息淹没。所以我们不得不审核，并删除一些评论。总的来说，我们一直在进行建设性的讨论，无论是通过传统方式进行数学研究的人，还是通过人工智能进行数学研究的人。