编辑：编辑部

7月17日，「牛津数学公开讲座」系列研讨会邀请到了陶哲轩进行演讲，主题是关于AI在科学和数学领域的潜力。
演讲结束后，陶哲轩还和CMU数学教授、IMO美国队前教练罗博深进行了对谈。
此前，陶哲轩就在一次采访中详细阐述了他眼中的AI将如何颠覆数学研究。那就让我们看看，这次他又发表了哪些新的观点。

人工智能是「猜测机器」

「科学就像能产生一定量饮用水的水龙头，而突然之间，我们有了AI这个大消防水管」。
陶哲轩又做出了一个精彩的类比。
他认为，虽然AI的缺陷在医疗、财务决策这类领域显得相当危险，但在某些领域是可以接受的，特别是科学领域，因为科学就是关于验证，尤其是独立验证的过程。
如果有一种设置，可以将AI不可预测但功能强大的输出与独立验证相结合，以过滤掉垃圾，只保留有用的东西。那么我们将会看到大量潜在应用的涌现。
AI这个「大消防水管」，可以输出10倍甚至100倍的液体，但输出的并不是可饮用的水。
但如果我们拥有一个过滤装置以后呢？它可以帮助我们过滤掉那些杂质，我们就可以得到干净的水（科学）了。
这就是陶哲轩看待科学的方式——以数学的方式来看待它。
在许多科学领域，寻找解决问题的「候选答案」成为了瓶颈。
比如在药物设计领域，我们想为某种疾病找到一种药物。为此，我们必须要合成它。
首先可能需要从自然界中找到一种药物，或者对药物进行改良。然后，必须要合成、试验，第一阶段试验，第二阶段试验……
这是一个长达数年的试验过程，而且非常昂贵。因此，只有最大的制药公司才能负担得起全程研发直至最终获得批准。
许多测试的药物实际上并不奏效，它们在研发过程中的某个阶段不得不被放弃。有时候你会幸运一点，虽然它们没有治愈你想要治疗的问题，但它们对其他某些问题有益。
但即便如此，这还是一个非常不确定，有很多试错的过程。
如果有一种方法可以减少试验候选对象，那么一定是利用人工智能。
现在科学家真的在用AI来模拟蛋白质。并且很快，如果有足够的数据，就可以开始根据现有临床试验的数据模拟药物功能，为各种疾病找到有潜力的候选药物。
在这个过程中，我们仍然需要遵循科学验证的标准。但不必筛选100个候选者，或许只需10个，你就能找到那一个有效的方法。
陶哲轩还谈到了材料科学领域。
室温超导体是否存在，这个问题已经困扰了我们数十年。人们尝试了不同的材料，虽然偶尔有所突破，但通常都以失败告终。
但是，AI有潜力跳过昂贵的合成过程，如果科学家能将候选者数量大幅减少，以大比例缩小范围，那将是革命性的改变。
实际上，这些科学问题中的设计部分不仅正在被人工智能自动化，甚至合成过程本身也是如此。
人们还在开发由AI驱动的实验室，以更加自动化的方式进行危险性的化学品的合成。
因此，减少昂贵测试候选对象，这是AI加速科学发展的一个应用领域。
另一个领域是模型加速。
在现代社会，我们必须对各种事物进行建模。
大气、交通、经济……几乎每一件事，每一个复杂的系统，我们希望为宇宙建模。
但是，建模常常需要我们做的是，必须要运行物理定律。
如果我们想预测地球未来20年的气候状况，我们会收集大量数据，并运用已知的物理定律，为了提高准确性，我们需要将时间划分得非常细小，还需要把地球划分成非常细小的网格。
这需要使用超级计算机，而且需要数月的时间来完成。
如果想预测气候，比如假设二氧化碳浓度保持在这个水平，20年后会发生什么，则需要花费数月时间才能得到一个相对准确的答案。
但是，原则上，人工智能可以大大缩短这个过程。如果有大量通过超级计算机获得的模拟数据，就可以用于AI训练，找出基于未见过的输入数据预测结果的最佳拟合方案。
气候模拟领域的人们已经能够在几小时内恢复传统超级计算机模拟的准确性，而不是几个月。
陶哲轩强调说，这种加速真的是非常、非常地显著。
作为一名数学家，我对人工智能可能如何改变数学感到非常兴奋。
提升AI数学推理能力可能会是一个非常广阔的领域，提升许多应用场景中的可用性。
目前我们已经看到了一些用例，但还是远远不够。虽然革命尚未发生，但我认为它即将到来。
将AI应用于学和数据学科有一些缺点，就像上面的乘法题一样，它可能给出错误的结果。
但这也不是世界末日，我们有很多方法进行独立验证，例如Lean这类的辅助证明软件，从而不必完全信任AI。
辅助证明软件类似于一种计算机编程语言，但输出并不是可执行程序，而是用于验证某个陈述是否正确。与AI不同，这类软件可以100%按照程序设定运行。
目前，数学家们编写一个中等规模问题的证明大概需要几个月的时间，将其形式化所需的时间还要更久，至少是前者的10倍，还需要团队合作才能完成。
但得益于辅助证明软件，这个进程正在加快。
下图列出了数学领域的一些知名成果。上个世纪，定理从成功证明到形式化往往需要几十年时间，比如四色定理和开普勒猜想。
到了2020年提出的液体张量实验，仅用了18个月就完成了形式化。
去年11月，我和一些合作者证明了一个关于交换代数的猜想。当时我们立即决定，这是一个很好的测试案例，可以用来观察计算机的形式化技术是如何工作的。
最终，我们组建了一个大约20人的大团队，用三周的时间完成了形式化。
虽然依旧没有那么方便，但这个过程的难度在降低，每个定理都会在不久的将来被形式化。
目前，速度的提升大部分还是来自传统方法，比如更好的语言和软件库。
GitHub这样的平台能让更多的数学家在一起协同工作，不仅仅止步于5个人或者一两个小组，而是组织起更大的、20～50人参与的项目，这在以前是很难做到的。
而且，就像Copilot的代码自动补全一样，AI可以自动填补证明中的小步骤。
随着时间的推移，我认为AI不仅能自动完成单行证明，还能完成双行证明，最终在编写证明语句方面超越人类的速度。
甚至，未来数学家编写证明时，可能是向AI口述。只需像对学生那样，向AI解释证明的过程，让AI尝试对我们解释的每一个步骤进行形式化验证，再进行迭代改进。
这会比传统方式的数学研究更快，而且可以确保不会出错。所以我认为人工智能与数学将会产生巨大的协同效应。

与罗博深的炉边对谈

对谈中，罗博深问到了前段时间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