陶哲轩牛津对谈罗博深：解密DeepMind如何让AI拿到IMO银牌

新智元报道

编辑：编辑部

【新智元导读】陶哲轩一场新鲜出炉的演讲，为我们带来了一场干货满满的思想盛宴。

7月17日，「牛津数学公开讲座」系列研讨会邀请到了陶哲轩进行演讲，主题是关于AI在科学和数学领域的潜力。

演讲结束后，陶哲轩还和CMU数学教授、IMO美国队前教练罗博深进行了对谈。

人工智能是「猜测机器」

「通俗来讲，人工智能基本上就是一台猜测机器。」

陶哲轩的这次演讲建立在一个基调之上，那就是「AI会改变科学和数学，这是一项令人惊叹的技术」，但「AI并不是魔法」。

LLM是一个让我们输入（比如一个文本查询请求或其他请求），继而产生输出（文本、图像或数字）的软件。

这种做法在数学上其实很平常。

实际上，LLM的本质就是在解一个巨大的方程组！通过反复几百次的权重调整，LLM最终找到了每个单词后面的下一个单词是什么。

对于人类来说，这个过程相当复杂，但在数学上，这是一个非常无聊的过程。有趣的是如何找到这些权重的方法。

说到这里，陶哲轩又打了一个比方，AI就像是「飞机的发明」。

喷气式发动机刚刚出现时，汽车、火车和船只已经是相当成熟的交通工具了，因此这种新引擎看起来仅仅是个玩具，几乎无法完成任何实际工作。

但随着时间的推移，它会变得越来越强大，终有一天让人类的旅行速度达到当时最快陆地交通工具的10倍。

但你不能仅仅因为看到了引擎，就直接期待未来的成果，这中间还有许多工作。

为了造出有实际用途的飞机，我们需要设计新的安全协议、新的仪表设备，找到新的方法，以便更好地理解物理定律——飞机仍然遵循物理定律。

是的，AI就是这样。它不是魔法，而是与规模有关。AI就像我们日常生活中已经使用的许多软件一样。

但是有一个关键的区别，那就是我们现在倾向于使用的软件往往相当无聊，缺乏创意。你输入什么，每次都会得到相同的输出。

在浏览器中输入一个网址，就会直接跳转到相应的网页。而且软件常常很挑剔，如果你稍微犯了个小错误，输入了错误的网址，那么你可能会被带到其他的地方。但是这一切都非常可预测。

Karpathy也曾表达类似观点，过去的搜索引擎没有幻觉，但也没有创造力：LLM is 100% dreaming

但人工智能不同，特别是去年流行起来的那些大语言模型，它们更有创意。

用相同的查询问LLM两次，你可能会得到不同的答案，而且无法保证答案是正确的。

看起来更加离谱且难以理解的是，大模型有时能成功解决非常复杂的数学证明题，比如——

但大多数情况下，它们很难答对「9.9和9.11哪个大」这种问题，简单的算术题也经常算不准。

这正是陶哲轩将其比喻为「猜测机器」原因——它猜测出一个接近于它曾看到的其他问题的正确答案，而不是经过它的独立思考。

这是一种与我们习惯的技术不同的新技术。

我们习惯的技术是那种「在我们眼皮子底下犯错」的，它们会制造出一些不怎么样的输出，让我们易于察觉。

但由于AI的本质，这些权重被特意选择，以便让答案尽可能接近正确答案。所以即使它们错了，看起来也会非常具有说服力。

那么问题来了，我们该如何使用这项新技术呢？

陶哲轩承认，在医疗、财务决策等领域，AI的安全性真的还没有达到标准。尽管有许多潜在的好处，我们依旧需要抱持谨慎的态度。

这就像我们花了几十年时间，才让飞行器达到一个对普通公众来说真的很安全的状态。

英雄所见略同，LeCun在谈到AI的安全性问题时，也喜欢将其与飞行器做比

但AI正在一些领域取得应用，比如陶哲轩此次演讲时的背景幻灯片就是自动生成的，有一种浓浓的「AI味儿」。

看起来的确很像MidJourney或DALL-E的默认风格

但陶哲轩笑谈道，「其实也还好，它只需要看起来足够令人信服即可。背景图片并不是我演讲的核心内容」。

详解AI潜力

「消防水管」加速科学发展

「科学就像能产生一定量饮用水的水龙头，而突然之间，我们有了AI这个大消防水管」。

陶哲轩又做出了一个精彩的类比。

他认为，虽然AI的缺陷在医疗、财务决策这类领域显得相当危险，但在某些领域是可以接受的，特别是科学领域，因为科学就是关于验证，尤其是独立验证的过程。

如果有一种设置，可以将AI不可预测但功能强大的输出与独立验证相结合，以过滤掉垃圾，只保留有用的东西。那么我们将会看到大量潜在应用的涌现。

AI这个「大消防水管」，可以输出10倍甚至100倍的液体，但输出的并不是可饮用的水。

但如果我们拥有一个过滤装置以后呢？它可以帮助我们过滤掉那些杂质，我们就可以得到干净的水（科学）了。

这就是陶哲轩看待科学的方式——以数学的方式来看待它。

在许多科学领域，寻找解决问题的「候选答案」成为了瓶颈。

比如在药物设计领域，我们想为某种疾病找到一种药物。为此，我们必须要合成它。

首先可能需要从自然界中找到一种药物，或者对药物进行改良。然后，必须要合成、试验，第一阶段试验，第二阶段试验……

这是一个长达数年的试验过程，而且非常昂贵。因此，只有最大的制药公司才能负担得起全程研发直至最终获得批准。

许多测试的药物实际上并不奏效，它们在研发过程中的某个阶段不得不被放弃。有时候你会幸运一点，虽然它们没有治愈你想要治疗的问题，但它们对其他某些问题有益。

但即便如此，这还是一个非常不确定，有很多试错的过程。

如果有一种方法可以减少试验候选对象，那么一定是利用人工智能。

现在科学家真的在用AI来模拟蛋白质。并且很快，如果有足够的数据，就可以开始根据现有临床试验的数据模拟药物功能，为各种疾病找到有潜力的候选药物。

在这个过程中，我们仍然需要遵循科学验证的标准。但不必筛选100个候选者，或许只需10个，你就能找到那一个有效的方法。

陶哲轩还谈到了材料科学领域。

室温超导体是否存在，这个问题已经困扰了我们数十年。人们尝试了不同的材料，虽然偶尔有所突破，但通常都以失败告终。

但是，AI有潜力跳过昂贵的合成过程，如果科学家能将候选者数量大幅减少，以大比例缩小范围，那将是革命性的改变。

实际上，这些科学问题中的设计部分不仅正在被人工智能自动化，甚至合成过程本身也是如此。

人们还在开发由AI驱动的实验室，以更加自动化的方式进行危险性的化学品的合成。

因此，减少昂贵测试候选对象，这是AI加速科学发展的一个应用领域。

另一个领域是模型加速。

在现代社会，我们必须对各种事物进行建模。

大气、交通、经济……几乎每一件事，每一个复杂的系统，我们希望为宇宙建模。

但是，建模常常需要我们做的是，必须要运行物理定律。

如果我们想预测地球未来20年的气候状况，我们会收集大量数据，并运用已知的物理定律，为了提高准确性，我们需要将时间划分得非常细小，还需要把地球划分成非常细小的网格。

这需要使用超级计算机，而且需要数月的时间来完成。

如果想预测气候，比如假设二氧化碳浓度保持在这个水平，20年后会发生什么，则需要花费数月时间才能得到一个相对准确的答案。

但是，原则上，人工智能可以大大缩短这个过程。如果有大量通过超级计算机获得的模拟数据，就可以用于AI训练，找出基于未见过的输入数据预测结果的最佳拟合方案。

气候模拟领域的人们已经能够在几小时内恢复传统超级计算机模拟的准确性，而不是几个月。

陶哲轩强调说，这种加速真的是非常、非常地显著。

从20年到3周：革命即将到来

作为一名数学家，我对人工智能可能如何改变数学感到非常兴奋。

提升AI数学推理能力可能会是一个非常广阔的领域，提升许多应用场景中的可用性。

目前我们已经看到了一些用例，但还是远远不够。虽然革命尚未发生，但我认为它即将到来。

将AI应用于学和数据学科有一些缺点，就像上面的乘法题一样，它可能给出错误的结果。

但这也不是世界末日，我们有很多方法进行独立验证，例如Lean这类的辅助证明软件，从而不必完全信任AI。

辅助证明软件类似于一种计算机编程语言，但输出并不是可执行程序，而是用于验证某个陈述是否正确。与AI不同，这类软件可以100%按照程序设定运行。

目前，数学家们编写一个中等规模问题的证明大概需要几个月的时间，将其形式化所需的时间还要更久，至少是前者的10倍，还需要团队合作才能完成。

但得益于辅助证明软件，这个进程正在加快。

下图列出了数学领域的一些知名成果。上个世纪，定理从成功证明到形式化往往需要几十年时间，比如四色定理和开普勒猜想。

到了2020年提出的液体张量实验，仅用了18个月就完成了形式化。

去年11月，我和一些合作者证明了一个关于交换代数的猜想。当时我们立即决定，这是一个很好的测试案例，可以用来观察计算机的形式化技术是如何工作的。

最终，我们组建了一个大约20人的大团队，用三周的时间完成了形式化。

虽然依旧没有那么方便，但这个过程的难度在降低，每个定理都会在不久的将来被形式化。

目前，速度的提升大部分还是来自传统方法，比如更好的语言和软件库。

GitHub这样的平台能让更多的数学家在一起协同工作，不仅仅止步于5个人或者一两个小组，而是组织起更大的、20～50人参与的项目，这在以前是很难做到的。

而且，就像Copilot的代码自动补全一样，AI可以自动填补证明中的小步骤。

随着时间的推移，我认为AI不仅能自动完成单行证明，还能完成双行证明，最终在编写证明语句方面超越人类的速度。

甚至，未来数学家编写证明时，可能是向AI口述。只需像对学生那样，向AI解释证明的过程，让AI尝试对我们解释的每一个步骤进行形式化验证，再进行迭代改进。

这会比传统方式的数学研究更快，而且可以确保不会出错。所以我认为人工智能与数学将会产生巨大的协同效应。

与罗博深的炉边对谈

关于DeepMind的IMO银牌

对谈中，罗博深问到了前段时间IMO竞赛的重大消息——DeepMind研发的AlphaProof和AlphaGeometry 2模型取得了相当于银牌的成绩。

在对谈中，他承认这个结果是自己没有预料到的。原本预计的时间线是未来3～4年，但没想到今年就能见证了AI解决IMO级别的数学问题。

这是非常好的工作，也很令人兴奋，又有点trick的成分在里面，但似乎进步往往来自cheap tricks。

IMO中的几何问题一般是确定可解的，但问题是，如果让AI直接写下全部的，比如20个语句，并执行标准算法，会有指数级的运行时间增长。

但是，如果你能做出一个有创意的构建，比如加上一个中点，然后根据这个新坐标重新排列现有信息，就可以大幅降低问题的复杂度。

DeepMind所做的事情就是让AI找到了这个捷径，再应用更标准的自动化工具，所以实际上只有很小一部分涉及到了AI，而且很有策略性。

但这种通用流程是可以扩展的。在复杂的数学问题，最困难的就是要找出关键的中间步骤。

比如，要证A⭢B，如果你能找到合适的中间点C，将问题转变为证明A⭢C且C⭢B成立，让两个子问题都是原问题难度的一半，这就是一个重大的进步。

也许AI在未来会很擅长这项工作，但我们没有这方面的数据。DeepMind之所以成功，背后的秘密是他们生成了大量几何问题进行测试。

参考资料：

https://www.youtube.com/watch?v=_sTDSO74D8Q

https://www.maths.ox.ac.uk/node/68242