陶哲轩转赞！ChatGPT自动证明重大突破，10年后AI将称霸数学界

前几天，一篇加州理工和MIT研究者用ChatGPT证明数学定理的论文爆火，在数学圈引发了极大关注。

图片

英伟达首席科学家Jim Fan激动转发，称AI数学Copilot已经到来，下一个发现新定理的，就是全自动AI数学家了！

纽约时报近日也发文，称数学家们做好准备，AI将在十年内赶上甚至超过最优秀的人类数学家。

图片

而陶哲轩本人，也转发了此文。

图片

Siobhan Roberts参加了今年Machine Assisted Proofs举办的IPAM研讨会，随后她根据自己的经历和采访，写下了这篇关于AI和数学的文章

AI也来颠覆数学界了！

如今，数学家们不得不正视一股最新的革命性力量——AI。

2019年，谷歌前雇员、现任湾区初创公司员工的计算机科学家Christian Szegedy预测，计算机系统将在十年内赶上或超过最优秀的人类数学家解决问题的能力。而去年，他把目标日期修改为2026年。

卡内基梅隆大学的逻辑学家Jeremy Avigad（蓝衣服），与学生在形式化数学暑期学校中

2018年菲尔兹奖得主、普林斯顿高等研究院的数学家Akshay Venkatesh目前还对使用AI不感兴趣，但他十分热衷于讨论AI相关的话题。

去年的采访中，Venkatesh表示，「我希望我的学生意识到，这个领域会发生非常大的变化。」

而最近他的态度是：「我不反对通过深思熟虑、甚至刻意地使用AI，来辅助人类的理解。但我坚信，对于我们使用它的方式，我们需要保持正念，慎之又慎。」

在今年二月，加州大学洛杉矶分校理论与应用数学研究所，曾举行了一场关于「机器辅助证明」的研讨会。

图片

研讨会的主要组织者，就是2006年的菲尔兹奖得主、在UCLA任职的数学家陶哲轩。

他指出，用AI辅助数学证明，其实是非常值得关注的现象。

直到最近几年，数学家才开始担心AI的潜在威胁，无论是AI对于数学美学的破坏，还是对于数学家本身的威胁。

而杰出的社区成员们，正在把这些问题摆上台面，开始探索如何「打破禁忌」。

暑期学校的组织者，自左至右：Avigad，Patrick Massot和Heather Macbeth

从欧几里得几何原本到计算机代码

几千年来，数学家已经早已适应了逻辑和推理的最新进展。不过，他们准备好迎接人工智能了吗？

图片

洛杉矶盖蒂博物馆中17世纪古希腊数学家欧几里得的肖像：他衣衫褴褛，举着自己的几何论文《元素》

2000多年来，欧几里得的文本一直是数学论证和推理的范式。

卡内基梅隆大学逻辑学家Jeremy Avigad说，欧几里得以近乎诗意的「定义」开始，在此基础上建立了当时的数学——使用基本概念、定义和先前的定理，每个连续的步骤都「清楚地遵循」以前的步骤，以这样一种方式证明事物。

图片

有人抱怨说，欧几里得的一些「明显」的步骤，其实不太明显，但Avigad博士说，但这个系统奏效了。

但是到20世纪以后，数学家们不愿意再将数学建立在这种直观的几何基础上了。

相反，他们开发了正式的系统，这个系统中有着精确的符号表示和机械的规则。

图片

https://kilthub.cmu.edu/articles/journal_contribution/A_Formal_System_for_Euclid_s_Elements/6490703

最终，在这种系统下，数学可以被翻译为计算机代码。

图片

1976年，四色定理成为第一个在暴力计算的帮助下被证明的主要定理。

四色定理：四种颜色足以填充地图，使得没有两个相邻区域颜色相同

会抱怨的AI：抱歉，我看不懂你们的定理

有这样一个数学小工具，被称为证明助手，或交互式定理证明器。

数学家会一步一步地将证明转换为代码，然后用软件程序检查推理是否正确。

验证过程会累积在一个动态规范参考库中，其他人都可以查阅。

图片

https://www.andrew.cmu.edu/user/avigad/Papers/formal_turn.pdf

霍斯金森形式数学中心主任Avigad博士说，这种类型的形式化为今天的数学奠定了基础，就像欧几里得试图将那个时代的数学转码，从而为其提供基础一样。

最近，开源证明助手系统Lean再次引发了大量关注。

图片

Lean是现在的亚马逊计算机科学家Leonardo de Moura在微软时开发的。

Lean使用的是自动推理，由老式的AI GOFAI提供支持，这是一个受逻辑启发的象征式AI。

图片

截至目前，Lean已经验证了一个将球体从内到外转动的有趣定理，以及一个统一数学领域方案的关键定理。

图片

图片

图片

图片

但是，证明助手也有缺点：它会时常抱怨自己不理解数学家输入的定义、公理或推理步骤，因此它也被赐名「证明抱怨器」。

这些抱怨会让研究变得繁琐，但Fordham大学的数学家Heather Macbeth表示，这类提供逐行反馈的功能，也会让系统对教学很有用。

图片

https://leanprover-community.github.io/courses.html

今年春天，Macbeth博士曾设计了一门「双语」课程，她将黑板上的每个问题都翻译成讲义中的Lean代码，学生们需要用Lean和自然语言提交解决方案。

图片

https://hrmacbeth.github.io/math2001/

「这给了他们信心，」Macbeth博士说，因为他们会收到即时反馈，关于证明何时完成，以及沿途的每一步是对还是错。

而在参加研讨会后，约翰霍普金斯大学的数学家Emily Riehl也尝试了一把。

图片

约翰霍普金斯大学的数学家Emily Riehl一直在使用实验证明辅助程序

她用了一个证明助手小程序，来证明自己此前发表过的文章中的定理。

使用完后，她大为震惊。「我现在很深入得了解了证明的过程，比我之前的理解要深刻得多。我的思路如此清晰，以至于我可以向最蠢的计算机解释清楚。」

图片

学生们在数学形式化暑期学校期间参加的一个小组项目

暴力推理——这很不「数学」

另一个计算机科学家们经常会用来解决一些数学问题的工具叫做「暴力推理」，但是数学界对于这种方法却常常嗤之以鼻。

然而，AI科学家们好像并不太在意数学家们的想法，不断地用他们自己熟悉的办法，去攻占数学「高地」。

卡耐基梅隆大学的计算机科学家Heule曾经在2016年用一个200T的「SAT 求解器」文件去解决「布尔毕达哥拉斯三元组问题」。

图片

https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext

《自然》杂志在文章中却说到：200T的证明是史上最大的证明过程，用这些工具解决问题是否真的算数学？

图片

但是在解决问题的论文作者本人，计算机科学家Heule看来，「这种方法是解决超过人类能力范围的问题所必须的。」

图片

同样的，在国际象棋比赛中战胜了人类（AlphaZero）之后，DeepMind又设计了机器学习算法来解决蛋白质折叠（AlphaFold）。

DeepMind发表了一篇论文，认为他们取得这些成果的方式，是通过AI来引导人类的直觉，从而推进数学发展。

图片

https://www.nature.com/articles/s41586-021-04086-x

而一位前谷歌计算机科学家，现在正在湾区创业的Yuhuai Wu也表示，自己的创业的方向就是利用机器学习来解决数学问题。

图片

他目前的项目，Minerva，就是一个用来解决数学模型的微调大语言模型。

未来，他希望这个项目能成长为一个「自动化数学家」，可以作为一个通用研究助理来「独立解决数学问题」。

图片

数学是一个试金石

另一方面，很多深度接触过AI技术的数学家也对AI在数学研究中不被重视提出了担心。

他们认为，人工智能技术经常能够「直接地」帮助数学家们「找到」自己想要的答案。

虽然数学家或者AI专家们都搞不清楚AI是如何找到这个答案的。

与DeepMind合作过的数学家Geordie Williamson曾经分享了一段与DeepMind合作的经历。

他在和DeepMind合作的过程中，DeepMind发现的一个神经网络可以预测他认为很重要的数据值，而且异常准确。

图片

他就很努力地去试图理解AI是如何做到的，因为这可能成为一个定理的基础。

但他最后还是没办法搞懂AI的逻辑，而且DeepMind的人也没法做到。

就像欧几里得一样，神经网络以某种方式找到了真理，但是逻辑原因却很难被理解。

另一方面，从这位数学家的角度看来，推理是数学的精髓，但却是机器学习中一直缺少的一块拼图。

在科技圈中，如果有一个黑箱在大部分情况下都能提供解决问题的方法，科技圈就会非常满足了。

AI就是这样一个黑箱。

但是数学家们却不会满足于这种状况。

这位数学家看来，尝试理解神经网络的原理会引发出令人着迷的数学问题。

而解决这些问题，会让数学家「为世界做出有意义的贡献」。

假如AI能证明数学定理

如果AI生成的假设定理充斥整个世界，我们该怎么做？

网友对此发出灵魂拷问，我对AI系统提出新的假设/公式是第一步有所怀疑，因为DeepMind早已在纽结理论中做到了。

我想知道，社区将如何应对AI输出的大量新假设。check人工智能创建的逻辑论点是一回事；被数百万个「哦，这可能是真的」建议淹没是另一回事。我不认为我们现有的评论和出版系统为此做好了准备。

这会对人们对数学的信任产生什么影响？

图片

有人认为，机器并不能很快就能完成数学研究，但可以看到它改变了研究方式，就像机器学习模型和计算能力如何改变了生物学领域一样。

图片

还有网友表示，从AlphaDev开始，我就一直在思考这个问题，但是同样的程序可以构建排序算法，也可以使用自动证明检查器来证明数学定理。真正的问题是它是否可以用来证明一些重要的东西，而不仅仅是微不足道的发现。

图片

图片

不过还是有网友依然对GPT类的工具能否真的发现有价值的真理持怀疑态度。

图片

也有网友指出，可能人类和AI对于数学理解和关注本就有区别，AI证明了什么是真的，而人类总是关注为什么它是真的。