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

尽管许多人并不愿意承认，但是很可能，AI 会在十年内赶超人类数学家。

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

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

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

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

AI 也来颠覆数学界了！

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

而一位前谷歌计算机科学家，现在正在湾区创业的 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 证明了什么是真的，而人类总是关注为什么它是真的。

参考资料:

广告声明:文内含有的对外跳转链接，用于传递更多信息，节省甄选时间，结果仅供参考，IT之家所有文章均包含本声明。