人工智能

ChatGPT自动证明重大突破 10年后AI将称霸数学界

字号+作者: 来源:新智元 2023-07-03 19:03 评论(创建话题) 收藏成功收藏本文

尽管许多人并不愿意承认,但是很可能,AI会在十年内赶超人类数学家。前几天,一篇加州理工和MIT研究者用ChatGPT证明数学定理的论文爆火,在数学圈引发了极大关'...

尽管许多人并不愿意承认,但是很可能,AI会在十年内赶超人类数学家。前几天,一篇加州理工和MIT研究者用ChatGPT证明数学定理的论文爆火,在数学圈引发了极大关注。Z1w品论天涯网


Z1w品论天涯网

英伟达首席科学家JimFan激动转发,称AI数学Copilot已经到来,下一个发现新定理的,就是全自动AI数学家了!Z1w品论天涯网

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


Z1w品论天涯网

而陶哲轩本人,也转发了此文。Z1w品论天涯网


Z1w品论天涯网

SiobhanRoberts参加了今年MachineAssistedProofs举办的IPAM研讨会,随后她根据自己的经历和采访,写下了这篇关于AI和数学的文章Z1w品论天涯网

AI也来颠覆数学界了!Z1w品论天涯网

如今,数学家们不得不正视一股最新的革命性力量——AI。Z1w品论天涯网

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


Z1w品论天涯网

卡内基梅隆大学的逻辑学家JeremyAvigad(蓝衣服),与学生在形式化数学暑期学校中Z1w品论天涯网

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

去年的采访中,Venkatesh表示,“我希望我的学生意识到,这个领域会发生非常大的变化。”Z1w品论天涯网

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

在今年二月,加州大学洛杉矶分校理论与应用数学研究所,曾举行了一场关于“机器辅助证明”的研讨会。Z1w品论天涯网


Z1w品论天涯网

研讨会的主要组织者,就是2006年的菲尔兹奖得主、在UCLA任职的数学家陶哲轩。Z1w品论天涯网

他指出,用AI辅助数学证明,其实是非常值得关注的现象。Z1w品论天涯网

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

而杰出的社区成员们,正在把这些问题摆上台面,开始探索如何“打破禁忌”。Z1w品论天涯网


Z1w品论天涯网

暑期学校的组织者,自左至右:Avigad,PatrickMassot和HeatherMacbethZ1w品论天涯网

从欧几里得几何原本到计算机代码Z1w品论天涯网

几千年来,数学家已经早已适应了逻辑和推理的最新进展。不过,他们准备好迎接人工智能了吗?Z1w品论天涯网


Z1w品论天涯网

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

2000多年来,欧几里得的文本一直是数学论证和推理的范式。Z1w品论天涯网

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


Z1w品论天涯网

有人抱怨说,欧几里得的一些“明显”的步骤,其实不太明显,但Avigad博士说,但这个系统奏效了。Z1w品论天涯网

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

相反,他们开发了正式的系统,这个系统中有着精确的符号表示和机械的规则。Z1w品论天涯网


Z1w品论天涯网

https://kilthub.cmu.edu/articles/journal_contribution/A_Formal_System_for_Euclid_s_Elements/6490703Z1w品论天涯网

最终,在这种系统下,数学可以被翻译为计算机代码。Z1w品论天涯网


Z1w品论天涯网

1976年,四色定理成为第一个在暴力计算的帮助下被证明的主要定理。Z1w品论天涯网


Z1w品论天涯网

四色定理:四种颜色足以填充地图,使得没有两个相邻区域颜色相同Z1w品论天涯网

会抱怨的AI:抱歉,我看不懂你们的定理Z1w品论天涯网

有这样一个数学小工具,被称为证明助手,或交互式定理证明器。Z1w品论天涯网

数学家会一步一步地将证明转换为代码,然后用软件程序检查推理是否正确。Z1w品论天涯网

验证过程会累积在一个动态规范参考库中,其他人都可以查阅。Z1w品论天涯网


Z1w品论天涯网

https://www.andrew.cmu.edu/user/avigad/Papers/formal_turn.pdfZ1w品论天涯网

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

最近,开源证明助手系统Lean再次引发了大量关注。Z1w品论天涯网


Z1w品论天涯网

Lean是现在的亚马逊计算机科学家LeonardodeMoura在微软时开发的。Z1w品论天涯网

Lean使用的是自动推理,由老式的AIGOFAI提供支持,这是一个受逻辑启发的象征式AI。Z1w品论天涯网


Z1w品论天涯网

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


Z1w品论天涯网


Z1w品论天涯网


Z1w品论天涯网


Z1w品论天涯网

但是,证明助手也有缺点:它会时常抱怨自己不理解数学家输入的定义、公理或推理步骤,因此它也被赐名“证明抱怨器”。Z1w品论天涯网


Z1w品论天涯网

这些抱怨会让研究变得繁琐,但Fordham大学的数学家HeatherMacbeth表示,这类提供逐行反馈的功能,也会让系统对教学很有用。Z1w品论天涯网


Z1w品论天涯网

https://leanprover-community.github.io/courses.htmlZ1w品论天涯网

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


Z1w品论天涯网

https://hrmacbeth.github.io/math2001/Z1w品论天涯网

“这给了他们信心,”Macbeth博士说,因为他们会收到即时反馈,关于证明何时完成,以及沿途的每一步是对还是错。Z1w品论天涯网

而在参加研讨会后,约翰霍普金斯大学的数学家EmilyRiehl也尝试了一把。Z1w品论天涯网


Z1w品论天涯网

约翰霍普金斯大学的数学家EmilyRiehl一直在使用实验证明辅助程序Z1w品论天涯网

她用了一个证明助手小程序,来证明自己此前发表过的文章中的定理。Z1w品论天涯网

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


Z1w品论天涯网

学生们在数学形式化暑期学校期间参加的一个小组项目Z1w品论天涯网

暴力推理——这很不“数学”Z1w品论天涯网

另一个计算机科学家们经常会用来解决一些数学问题的工具叫做“暴力推理”,但是数学界对于这种方法却常常嗤之以鼻。Z1w品论天涯网


Z1w品论天涯网

然而,AI科学家们好像并不太在意数学家们的想法,不断地用他们自己熟悉的办法,去攻占数学“高地”。Z1w品论天涯网

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


Z1w品论天涯网

https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltextZ1w品论天涯网

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


Z1w品论天涯网

但是在解决问题的论文作者本人,计算机科学家Heule看来,“这种方法是解决超过人类能力范围的问题所必须的。”Z1w品论天涯网


Z1w品论天涯网

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

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


Z1w品论天涯网

https://www.nature.com/articles/s41586-021-04086-xZ1w品论天涯网

而一位前Google计算机科学家,现在正在湾区创业的YuhuaiWu也表示,自己的创业的方向就是利用机器学习来解决数学问题。Z1w品论天涯网


Z1w品论天涯网

他目前的项目,Minerva,就是一个用来解决数学模型的微调大语言模型。Z1w品论天涯网

未来,他希望这个项目能成长为一个“自动化数学家”,可以作为一个通用研究助理来“独立解决数学问题”。Z1w品论天涯网


Z1w品论天涯网

数学是一个试金石Z1w品论天涯网

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

他们认为,人工智能技术经常能够“直接地”帮助数学家们“找到”自己想要的答案。Z1w品论天涯网

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


Z1w品论天涯网

与DeepMind合作过的数学家GeordieWilliamson曾经分享了一段与DeepMind合作的经历。Z1w品论天涯网

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


Z1w品论天涯网

他就很努力地去试图理解AI是如何做到的,因为这可能成为一个定理的基础。Z1w品论天涯网

但他最后还是没办法搞懂AI的逻辑,而且DeepMind的人也没法做到。Z1w品论天涯网


Z1w品论天涯网

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

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

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

AI就是这样一个黑箱。Z1w品论天涯网


Z1w品论天涯网

但是数学家们却不会满足于这种状况。Z1w品论天涯网

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

而解决这些问题,会让数学家“为世界做出有意义的贡献”。Z1w品论天涯网

假如AI能证明数学定理Z1w品论天涯网

如果AI生成的假设定理充斥整个世界,我们该怎么做?Z1w品论天涯网

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

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

这会对人们对数学的信任产生什么影响?Z1w品论天涯网


Z1w品论天涯网

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


Z1w品论天涯网

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


Z1w品论天涯网


Z1w品论天涯网

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


Z1w品论天涯网

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

本网除标明“PLTYW原创”的文章外,其它文章均为转载或者爬虫(PBot)抓取; 本文只代表作者个人观点,不代表本站观点,仅供大家学习参考。本网站属非谋利性质,旨在传播马克思主义和共产主义历史文献和参考资料。凡刊登的著作文献侵犯了作者、译者或版权持有人权益的,可来信联系本站删除。 本站邮箱[email protected]