AI向人类发起数学挑战

参考消息网8月30日报道据美国《纽约时报》网站近日报道，数千年来，数学家们一直适应着逻辑和推理方面的最新进展。他们准备好应对人工智能(AI)了吗？

漫长的人类数学史

(资料图片仅供参考)

在洛杉矶格蒂博物馆的藏品中，有一幅创作于17世纪的古希腊数学家欧几里德的肖像画：不修边幅的他用肮脏的双手举起自己的几何学专著《几何原本》。

2000多年来，欧几里德的著作一直是数学论证和推理的范本。卡内基-梅隆大学的逻辑学家杰里米·阿维加德在电子邮件中写道：“欧几里德潇洒地从几乎充满诗意的‘定义’出发，然后在此基础上建立了当时的数学，采用基本的概念、定义和先验定理，以一种每个后续步骤都‘明显源自于’先前步骤的方式作出各种求证。”阿维加德说，尽管有人抱怨欧几里德的某些“显而易见”的步骤并不那么一目了然，但这套系统是行得通的。

但是到了20世纪，数学家们不再甘心把数学建立在这种直觉的几何学基础上。作为替代，他们开发了形式系统——即精准的符号表示和机械的规则。最终，这种形式化使得数学可以被翻译成计算机代码。1976年，四色定理——该定理声称用四种颜色为地图着色就足以使任何两个相邻地区不会有相同的颜色——成为利用计算机强大算力帮助证明的第一个重要定理。

现在，数学家们正在努力应对最新的变革性力量：人工智能。

2019年，曾任职于谷歌、目前在旧金山湾区一家初创公司工作的计算机科学家克里斯蒂安·塞盖迪预言，10年内计算机系统将能匹敌、甚至超越人类最出色数学家的解题能力。去年，他把目标日期修正为2026年。

数学审美受到威胁

普林斯顿高等研究院的数学家、2018年菲尔兹奖获得者阿克沙伊·文卡泰什目前对使用人工智能不感兴趣，但他热衷于谈论人工智能。他去年在接受采访时曾说：“我希望我的学生们意识到他们所从事的领域将发生巨大变化。”他最近通过电子邮件补充说：“我并不反对慎重和从容地利用技术辅助我们人类的理解力。但我坚决认为，对我们使用技术的方式多加小心是必不可少的。”

今年2月，阿维加德出席了加利福尼亚大学洛杉矶分校纯粹数学与应用数学研究所一个有关“机器辅助求证”的研讨会。顺便提一句，他在研讨会的最后一天去参观了那幅欧几里德肖像。这次会议吸引了一个非典型的数学家和计算机科学家群体。该校数学家、2006年菲尔兹奖获得者和研讨会的主要组织者陶哲轩说：“感觉这个问题很重要。”

陶哲轩指出，数学家们只是在过去几年里才开始担心人工智能的潜在威胁，不管是对数学审美还是对他们自身而言。他说，这个名人圈的成员们现在正张罗着讨论这些问题，并深入探索那种“可能打破禁忌”的潜力。

一个引人注目的与会者坐在研讨会前排：它是一个名为“举手机器人”的梯形盒子，每当某个在线参会者提出问题时，它便会发出一种机械的嘀咕声并举起手来。陶哲轩说：“如果机器人聪明伶俐且不构成威胁，那么它将是有益的。”

如今我们并不缺乏优化生活——饮食、睡眠、锻炼——的小器具。威斯康星大学麦迪逊分校的数学家乔丹·埃伦伯格在研讨会某次休息时间说：“我们喜欢把器具附加在自己身体上，以便能够在解决问题的时候稍稍容易一些。”他补充说，对于数学而言，人工智能器具或许能起到同样的作用，“显而易见，真正的问题是机器可以为我们做什么，而不是机器将对我们做什么”。

代码化的数学推理

有一种数学器具名为“求证助手”或交互式定理证明器。某个数学家按部就班地把求证过程编译为代码，然后软件程序就可以核实推理是否正确。核实过程集中存放在某个程序库，即任何人都可以查阅的动态规范文献库当中。阿维加德——他是霍斯金森形式数学研究中心(该中心由加密货币企业家查尔斯·霍斯金森资助)的主任——说，这种形式化为今天的数学提供了基础，“就像欧几里德曾试图为他那个时代的数学编制法典和提供基础一样”。

最近，开源求证辅助系统Lean正吸引人们注意。由微软公司计算机科学家莱昂纳多·德莫拉开发的Lean系统采用了由所谓“有效的老式人工智能”(GOFAI)——即从逻辑学汲取灵感的符号人工智能——所驱动的自动推理。到目前为止，除其他策略外，Lean已证明了一条有关球面内外翻转的有趣定理，以及统一数学各分支的方案中的一条关键定理。

但求证助手也有不足：它经常抱怨理解不了数学家输入的定义、公理或推理步骤，因此它被称为“求证哀诉者”。所有这些哀诉都可能让研究工作变得麻烦。但是福德姆大学数学家希瑟·麦克贝思说，同样的特点——即提供逐行的反馈——也使得这些系统可以有助于教学。

今年春季，麦克贝思设计了一门“双语”课程：她在备课笔记中把出在黑板上的每一道数学题都翻译成为Lean代码，学生们提交的课外作业解题也采用Lean代码和文字表达两种形式。麦克贝思说，“这给了他们信心”，因为他们可以得到有关证明过程何时完成，以及其中的每一步是否正确的即时反馈。

参加那次研讨会之后，约翰斯·霍普金斯大学的数学家埃米莉·里尔利用一个实验性求证助手程序对她以前与别人合作发表过的证明过程进行形式化。她说，到验证结束时，“我对于证明过程确实有了深刻的理解，远比我以前任何时候都来得深刻。我的思路如此清晰，以至于我可以向一台十分愚笨的电脑作出解释”。

自动化证明将来临

另一种自动化推理工具是卡内基-梅隆大学数学科学家、亚马逊研究奖获得者马赖恩·休尔所使用的被他通俗地称为“蛮力推理”的工具(更专业的名称为“可满足性求解器”)。他说，利用精心设计的编码，你只需陈述希望找到哪一个“异常目标”，超级计算机网络就可以找遍搜索空间，并确定这个实体是否存在。

就在那个研讨会举行前夕，休尔和他的一名博士生贝尔纳多·叙贝尔卡索以一个50万亿字节的文件完成了对一个长期未得到解决的难题的解答。然而这个文件与2016年休尔200万亿字节的数学证明无法相比。《自然》杂志当时的新闻宣称“是有史以来最庞大的”。文章接着询问借助此类工具进行的解题是否还算是名副其实的数学。按照休尔的看法，这种做法对于“解答超出人类能力的题目”是必需的。

机器学习可以综合大量数据并发现规律，但并不擅长按部就班的逻辑推理。谷歌公司的“深层思维”项目设计了机器学习算法，以解决蛋白质折叠之类的任务及赢取国际象棋比赛。在《自然》杂志2021年的一篇论文中，某研究团队描述他们的研究结果“通过以人工智能指导人类直觉推动数学前进”。

曾在谷歌公司工作、目前就职于湾区一家初创企业的计算机科学家吴宇怀曾概述过更宏大的机器学习目标——“解答数学题”。在谷歌，吴宇怀探索了赋能聊天机器人的语言大模型如何能够帮助解答数学题。研究团队使用的是一个利用互联网数据进行过训练，随后又利用富含数学数据的海量数据集——例如在线数学和科学论文档案——进行了微调的模型。吴宇怀在研讨会上说，当被用日常英语要求解数学题时，这个名为“智慧女神”的专用聊天机器人“相当擅长模仿人类”。该模型在高中数学考试中的得分比16岁学生的平均得分高一些。

吴宇怀说，他设想最终将出现一种“有能力完全凭自己的力量证明数学定理”的“自动化数学家”。

数学界的忧虑加深

数学家们对于这些干扰表现出不同程度的忧虑。哥伦比亚大学的迈克尔·哈里斯在自媒体通讯平台“订阅堆栈”网站上发表的《硅算手》一文中表达了忧虑。哈里斯对缺乏关于人工智能对数学研究的宏观影响的讨论感到遗憾，尤其是在“相比之下有关这种技术的谈论在除数学外的每一个领域中都在极其热烈地进行着”的时候。

悉尼大学的乔迪·威廉姆森是“深层思维”项目的一名合作者，他在美国国家科学院的研讨会上发言鼓励数学家和计算机科学家更多地参与此类对话。在洛杉矶的研讨会上，他改动了乔治·奥威尔1945年散文《原子弹与你》中的一句话，作为自己的开场白。威廉姆森说：“鉴于我们所有人在今后5年内极有可能受到深刻影响，深度学习并没有引发预期中应有的大量讨论。”

威廉姆森认为数学将是验证机器学习可以或不可以做什么的试金石。推理是数学过程中的精髓，也是机器学习中至关重要的未解难题。

他在接受采访时说，在他与“深层思维”项目协作的早期阶段，团队曾发现某个简单的神经网络可以“预言我十分看重的数学中的数量”，而且其预言的“准确程度令人难以置信”。威廉姆森努力尝试理解其中的原因——这原本会造就某条定理，却无法做到。“深层思维”团队中的任何人也无法做到。就像古希腊几何学家欧几里德一样，神经网络曾以某种直觉的方式找到数学中的真理，但是其符合逻辑的“原因”却绝非一目了然。

在研讨会上，一个主题是如何把直觉和逻辑结合起来。如果人工智能可以同时做这两件事，那么结果将难以预料。

但是威廉姆森博士指出，人们缺乏弄懂机器学习所带来的黑匣子的动机。他说，“真正非凡的是技术界的黑客文化——前提是它在大多数时候行得通”，但是这种假想却不能让数学家们感到满意。

他补充说，尝试了解神经网络内部发生了什么将引出“极具吸引力的数学问题”，寻找这些答案将为数学家们提供一个“为世界作出有意义贡献”的机会。