AI向人类发起数学挑战

2023-08-30

美国《纽约时报》网站：数千年来，数学家们一直适应着逻辑和推理方面的进展。他们准备好应对人工智能(AI)了吗？

漫长的人类数学史

2000多年来，欧几里德的著作一直是数学论证和推理的范本。但是到了20世纪，数学家们不再甘心把数学建立在直觉的几何学基础上。作为替代，他们开发了形式系统——即精准的符号表示和机械的规则。最终，这种形式化使得数学可以被翻译成计算机代码。1976年，四色定理【声称用四种颜色为地图着色就足以使任何两个相邻地区不会有相同的颜色】成为利用计算机算力帮助证明的第一个重要定理。现在，数学家们正在努力应对最新的变革性力量：人工智能。2019年，计算机科学家克里斯蒂安·塞盖迪预言，10年内计算机系统将能匹敌、甚至超越人类最出色数学家的解题能力。

数学审美受到威胁

数学家阿克沙伊·文卡泰什热衷于谈论人工智能：“我希望我的学生们意识到他们所从事的领域将发生巨大变化。我并不反对利用技术辅助人类的理解力。但对这些技术必须多加小心。”数学家陶哲轩说：数学家们只是在过去几年里才开始担心人工智能的潜在威胁，不管是对数学审美还是对他们自身而言。如果机器人聪明伶俐且不构成威胁，那么它将是有益的。数学家乔丹·埃伦伯格说：“我们喜欢把器具附加在自己身体上，以便能够在解决问题的时候稍稍容易一些。对于数学而言，人工智能器具或许能起到同样的作用，真正的问题是机器可以为我们做什么，而不是机器将对我们做什么”。

代码化的数学推理

有一种数学器具名为“求证助手”或交互式定理证明器。数学家按部就班地把求证过程编译为代码，软件程序就可以核实推理是否正确。核实过程集中存放在任何人都可以查阅的动态规范文献库当中。这种形式化为今天的数学提供了基础，就像欧几里德曾试图为他那个时代的数学编制法典一样。最近，开源求证辅助系统Lean正吸引人们注意。它采用了由所谓“有效的老式人工智能”(GOFAI)所驱动的自动推理，并已证明了两条定理。但它经常抱怨理解不了数学家输入的东西。

自动化证明将来临

另一种自动化推理工具，被通俗地称为“蛮力推理”的工具。利用精心设计的编码，你只需陈述希望找到哪一个“异常目标”，超级计算机网络就可以确定这个实体是否存在。休尔以一个50万亿字节的文件完成了对一个长期未得到解决的难题的解答。当时的新闻宣称“是有史以来最庞大的”，询问借助此类工具进行的解题是否还算是名副其实的数学。休尔认为，这种做法对于“解答超出人类能力的题目”是必需的。机器学习可以综合大量数据并发现规律，但不擅长逻辑推理。谷歌公司的“深层思维”项目设计了机器学习算法，以解决蛋白质折叠之类的任务及赢取国际象棋比赛。通过以人工智能指导人类直觉推动数学前进。计算机科学家吴宇怀曾概述过机器学习目标——“解答数学题”。在谷歌，吴宇怀探索了赋能聊天机器人的语言大模型如何能够帮助解答数学题。研究团队使用的是一个利用互联网数据进行过训练，随后又利用富含数学数据的海量数据集微调了模型。当被用日常英语要求解数学题时，这个名为“智慧女神”的专用聊天机器人的得分比16岁学生的平均得分高一些。最终将出现一种“有能力完全凭自己的力量证明数学定理”的“自动化数学家”。

数学界的忧虑加深

数学家们对此表现出忧虑。哥伦比亚大学的迈克尔·哈里斯对缺乏关于人工智能对数学研究的宏观影响的讨论感到遗憾。

悉尼大学的乔迪·威廉姆森说：数学将是验证机器学习可以或不可以做什么的试金石。推理是数学过程中的精髓，也是机器学习中至关重要的未解难题。如何把直觉和逻辑结合起来。如果人工智能可以同时做这两件事，结果将难以预料。