·数学是机器学习能做什么或不能做什么的试金石。推理是数学过程的精髓，也是机器学习中尚未办理的关键问题。神经网络以某种办法直不雅观地辨别出了数学真理，但其逻辑“缘故原由”却远非那么明显。
加州理工学院和麻省理工学院研究者发布用大措辞模型证明数学定理的论文。
最近一段韶光，人工智能彷佛在数学领域取得了进展，只管一开始大措辞模型被看作并不是特殊适宜数学推理。
上周，英伟达数学家Jim Fan转发了加州理工学院和麻省理工学院研究者用ChatGPT证明数学定理的论文，称数学的AI Copilot（副驾驶）时期已经到来，未来人工智能将能够创造数学定理。这篇论文构建了一个基于大措辞模型的定理证明器，为办理大措辞模型幻觉方面的毛病开辟了一条新路子。
几天前，数学家、菲尔兹奖得主陶哲轩表示，他最近在办理一个数学难题时“利用了GPT-4”，“它给我供应了终极的解题思路，接下来我只须要连续打算就行。”为了给更多研究者参考，他晒出了自己和GPT-4的谈天记录。
如今，越来越多的数学研究者关注人工智能对该领域的影响，他们在各种谈论会上辩论，采取不同的AI工具考试测验解答数学问题。根据《纽约时报》最近对一些数学家的采访，他们正在努力应对人工智能这一最新变革力量。数千年来，数学家们已经适应了逻辑和推理方面的最新进展，他们为人工智能做好准备了吗？
数学家和打算机科学家一起开会
两千多年来，数学家欧几里得的文本一贯是数学论证和推理的典范。卡内基梅隆大学逻辑学家杰里米·阿维加德（Jeremy Avigad）在接管采访时说：“众所周知，欧几里得以近乎诗意的‘定义（definitions）’开始。” “然后，他在此根本上建立了当时的数学，利用基本观点、定义和先验定理，以每一个后续步骤‘清楚地遵照’之前的步骤来证明事物。”阿维加德说，有人抱怨欧几里得的一些“明显”步骤并不明显，但该系统仍旧有效。
但到了20世纪，数学家不再乐意将数学建立在这种直不雅观的几何根本上。相反，他们开拓了正式的系统——精确的符号表示、机器规则。终极，这种形式化使得数学能够转化为打算机代码。1976年，四色定理（该定理指出四种颜色足以添补舆图，因此没有两个相邻区域具有相同的颜色）成为第一个借助打算强力证明的紧张定理。
现在，人工智能来了。2019年，曾供职于谷歌、现供职于湾区一家初创企业的打算机科学家克里斯蒂安·塞格迪（Christian Szegedy）预测，打算机系统将在10年内遇上或超过人类最精良数学家办理问题的能力。去年他将目标年份修正为2026年。
普林斯顿高档研究院数学家、2018年菲尔兹奖得到者阿克谢·文卡特什（Akshay Venkatesh）目前对利用人工智能不感兴趣，但他热衷于评论辩论。 “我希望我的学买卖识到他们所处的领域将会发生很大的变革。”他在去年的一次采访中说。最近他又补充说：“我并不反对寻思熟虑和刻意利用技能来支持我们人类的理解。但我坚信，把稳我们利用它的办法至关主要。”
今年2月，阿维加德参加了在加州大学洛杉矶分校纯数学与运用数学研究所举办的“机器赞助证明”研讨会。这次聚会吸引了数学家和打算机科学家这一不屈常的组合。该研讨会的紧张组织者是陶哲轩，他曾在一篇博客中称，2026年AI将与搜索和符号数学工具相结合，成为数学研究中值得相信的合著者。陶指出，直到最近几年，数学家们才开始担心人工智能的潜在威胁，无论是对数学美学还是对他们自己，圈子成员现在正在提出这些问题并探索“冲破禁忌”。
帮助办理数学问题的小工具们
如今，在饮食、就寝、磨炼方面，优化人们生活的小工具十分普遍，威斯康星大学麦迪逊分校数学家乔丹·埃伦伯格（Jordan Ellenberg）在研讨会安歇期间接管采访说：“我们喜好给自己增加一些东西，以便更随意马虎把事情做好。”人工智能小工具可能对数学有同样的浸染。
个中一种数学小工具被称为证明助手或交互式定理证明器。数学家一步步将证明转化为代码，然后软件程序检讨推理是否精确。验证在一个库中积累，成为其他人可以查阅的动态参考。阿维加德说，这种“形式化”为当今的数学奠定了根本，“就像欧几里得试图编纂和整理数学、为他那个时期的数学奠定了根本一样。”
最近，开源证明赞助系统Lean备受关注。Lean由打算机科学家莱昂纳多·德·莫拉（Leonardo de Moura）开拓，当时他在微软，现在是亚马逊的打算机科学家。Lean利用自动推理，由所谓的“老式人工智能（GOFAI）”供应支持，即受逻辑启示的符号人工智能。到目前为止，Lean社区已履历证了一个翻转球体的定理和一个有助于统一数学领域的关键定理等。
但证明助手也有缺点：它常常抱怨不理解数学家输入的定义、公理或推理步骤，因此它被戏称为“证明抱怨者”。所有这些抱怨都会让研究变得很麻烦，但福特汉姆大学（Fordham University）的数学家希瑟·麦克白（Heather Macbeth）表示，供应逐行反馈的功能也使该系统对传授教化很有用。
今年春天，麦克白设计了一门“双语”课程：她把黑板上提出的每一个问题都翻译成讲义中的Lean代码，学生们用Lean和普通措辞提交作业答案。 “这给了它们信心。”麦克白说，由于它们收到了关于证明何时完成以及全体过程中的每一步是对比样错的即时反馈。
自从参加洛杉矶研讨会以来，约翰·霍普金斯大学的数学家艾米丽·里尔（Emily Riehl）利用实验性证明赞助程序来形式化她之前与合著者揭橥的证明。在验证结束时，她说：“我真的非常深入地理解了这个证明，比我以前理解的要深入得多。”
约翰·霍普金斯大学的数学家艾米丽·里尔一贯在利用一个实验性证明助理程序。
卡内基梅隆大学打算机科学家、亚马逊学者马利恩·海勒（Marijn Heule）利用另一种自动推理工具，被他称为“暴力推理”，或者更专业地说是可知足性问题求解器。他说，只要用精心设计的代码来解释你想要找到哪个“奇异物体”，超级打算机网络就会在搜索空间中进行“翻搅”，并确定该实体是否存在。
还有一组工具利用机器学习，可以合成大量数据并检测模式，但不善于逻辑、逐步推理。谷歌的DeepMind就设计了机器学习算法来办理蛋白质折叠和国际象棋得胜等问题，在2021年《自然》杂志的一篇论文中，一个团队将他们的成果描述为“通过人工智能辅导人类直觉来推进数学发展”。
前谷歌打算机科学家、现在在湾区创业的宇怀·“托尼”·吴（Yuhuai “Tony” Wu）概述了一个更宏伟的机器学习目标。在谷歌，吴探索了支持谈天机器人的大型措辞模型如何帮助数学。该团队利用的模型经由互联网数据演习，然后利用数学和科学论文的在线存档等大型数据集进行微调。吴在研讨会上说，当以日常措辞来哀求办理数学问题时，这个名为Minerva的专门谈天机器人“非常善于模拟人类”。该模型在高中数学考试中得到的成绩优于16岁学生的均匀成绩。吴说，他设想终极会有一位“自动化数学家”，具有“自行办理数学定理的能力”。
打算机科学家宇怀·“托尼”·吴设想了一位“自动化数学家”——具有“自行办理数学定理能力”的通用研究助理。
数学是试金石
对付这些颠覆式的创新，数学家们做出了不同程度的关注。
哥伦比亚大学的迈克尔·哈里斯（Michael Harris）表达了疑虑，他对研究数学与国防工业之间潜在的目标和代价不雅观冲突感到困扰。在最近的一份时势通讯中，他指出由美国国家科学院组织的一个研讨班——“AI帮忙数学推理”中，一名演讲者是博思艾伦咨询公司（Booz Allen Hamilton）的代表，该公司是情报机构和军方的承包商。哈里斯希望，能够有更多关于人工智能影响数学研究的谈论。
DeepMind的互助者、悉尼大学的乔迪·威廉姆森（Geordie Williamson）在美国国家科学院的那场聚会上揭橥了讲话，鼓励数学家和打算机科学家更多地参与此类对话。在洛杉矶的研讨会上，他以改编自乔治·奥威尔1945年文章《你和原子弹》的一句话开始了自己的演讲。威廉姆森说：“考虑到我们所有人在未来五年内都可能受到深刻影响，深度学习并没有引起像预期那么多的谈论。”他认为，数学是机器学习能做什么或不能做什么的试金石。推理是数学过程的精髓，也是机器学习中尚未办理的关键问题。
威廉姆森在接管采访时表示，在他与DeepMind互助的早期，该团队创造了一个大略的神经网络，可以预测他非常关心的数学量，而且它的预测“准确得可笑”。威廉姆森努力想要理解个中的缘故原由，但是无法理解，DeepMind的其他人也都做不到，而这个缘故原由将成为一个定理的根本。就像欧几里得一样，神经网络以某种办法直不雅观地辨别出了数学真理，但其逻辑“缘故原由”却远非那么明显。
在洛杉矶的研讨会上，一个突出的主题是如何将直觉和逻辑结合起来。但威廉姆森不雅观察到，人们很少有动力去理解机器学习的黑箱。他说：“这是科技界的黑客文化，如果它在大部分韶光都有效，那就太好了。”但这种情形让数学家们感到不满意。
他补充说，试图理解神经网络内部发生的事情会引发“令人着迷的数学问题”，而探求答案为数学家“为天下做出故意义的贡献”供应了机会。