本文来自微信公众号：Nature Portfolio （ID：nature-portfolio），作者：Davide Castelvecchi，题图来自：视觉中国
随着人们对聊天机器人的热度空前高涨，数学家也开始探索人工智能（AI）可以如何协助他们的工作。研究人员表示，无论是验证人类书写的证明，还是提出不同问题的解法，自动化正在改变数学——而且不仅限于计算领域。
加拿大蒙特利尔大学数论学家Andrew Granville说道，“我们这里谈的是一个非常具体的问题：机器会改变数学吗？”加州大学洛杉矶分校最近一场座谈会探讨了这个问题，希望能在数学家和计算机科学家之间搭建桥梁。“大部分数学家完全没有看到其中的机遇。”这场活动的主办者之一、美国卡内基梅隆大学的计算机科学家Marijn Heule说。
菲尔兹奖（Fields Medal）是数学界的至高荣誉，2018年的菲尔兹奖得主、美国普林斯顿高等研究院的Akshay Venkatesh在10月以他名义举办的研讨会上开启了关于计算机将如何改变数学的对话。菲尔兹奖的另外两位得主——法兰西公学院的Timothy Gowers和加州大学洛杉矶分校的陶哲轩（Terence Tao）——也在这场辩论中领衔发言。
帝国理工学院的数学家Kevin Buzzard说：“我们能吸引到菲尔兹奖得主和世界级的大数学家加入，说明这个领域正以前所未有的方式热了起来。”
AI方法
辩论的一个内容是哪类自动化工具最实用。AI主要有两类。一类是“符号”AI（symbolic AI），需要程序员将逻辑法则或计算嵌入代码中。“也就是大家眼中‘既靠谱又传统的AI’。”华盛顿的微软研究院（Microsoft Research）的Leonardo de Moura说道。
另一类AI基于人工神经网络，过去十年左右取得了巨大成功。对于这类AI，计算机或多或少需要从头开始，并通过消化海量数据来学习其中的模式。这种方式称为机器学习，它既是“大型语言模型”（包括ChatGPT一类的聊天机器人）的基础，也是能在高难度博弈中打败人类选手或是能预测蛋白质折叠的系统的基础。符号AI本身很严密，而神经网络只能进行统计学上的猜测，其运作方式也很神秘，不为人知。
de Moura通过打造名为Lean的系统，帮助符号AI在数学上取得了一些早期进展。这是一种交互式软件工具，要求研究人员为每个问题写出每个逻辑步骤，而且需要具体到最基本的细节，同时确保在数学上是正确的。两年前，一个数学家团队成功将一个很重要但难以理解的证明——其复杂程度就连作者自己也不确定——翻译成了Lean所使用的语言，最后确认了证明是正确的。
该团队表示，这个过程帮助他们理解了这个证明，甚至帮他们找到了简化证明的方法。“我认为这是比检验结果更令人激动的事”，de Moura说，“即使在最夸张的梦里，我们也不敢这么想。”
除了让个人的独立研究更轻松，这类“证明助手”还可以消除de Moura所谓的“信任瓶颈”，改变数学家之间的合作。“如果我们合作，我可能不太信任你做的那部分。但‘证明助手’能向合作者证明，他们完全可以相信你负责的工作没问题。”
智能化自动补全
另一个极端是聊天机器人风格的、基于神经网络的大型语言模型。在加州山景城的谷歌公司，前物理学家Ethan Dyer和他的团队开发了专门解决数学问题的聊天机器人Minerva。从核心上讲，Minerva是消息App自动补全功能的超智能版本：通过利用arXiv数据库里的数学论文进行训练，它已经学会以某些App预测词汇和句子的方式，写下解题的详细步骤。
Lean的沟通方式类似计算机代码，但与Lean不同的是，Minerva能以会话式英语理解问题并给出答案。de Moura说：“能以自动化方式解决这些问题的其中一些本就是一项成就。”
Minerva既展现了这种方法的能力，也暴露了它的可能局限。比如，它能准确将整数分解成素数——素数是无法被更小素数整除的数。但如果数字超过一定大小，它就会开始犯错，这说明它还没有“理解”其中的一般方法。
当然，Minerva的神经网络似乎还是能掌握一些通用技术，而不仅仅是统计学模式，谷歌团队正在尝试理解它是如何做到的。Dyer说：“归根结底，我们想要一个能和你头脑风暴的模型。”他说，这个模型对于需要从专业文献中获取信息的非数学家也很有用。通过学习课本和与专门的数学软件连接，还可以扩展Minerva的技能。
Dyer表示，开展Minerva项目的动力是为了看一看机器学习的方法到底能走多远；一种能协助数学家的强大自动化工具或许能将符号AI技术与神经网络结合起来。
数学对机器
长远上看，AI程序会一直屈居配角地位吗？还是它也能独立开展数学研究？AI生成正确数学命题和证明的能力或许会越来越强，但一些研究人员也担心，这些命题或证明的绝大部分将是无趣或无法理解的。
在去年10月的座谈会上，Gowers表示，研究人员或许有办法教会计算机一些数学相关性的客观标准，比如一个小命题是否能代表许多特例，甚至是连接起数学的各个分支。他说：“为了在定理证明上再上一个台阶，计算机就必须学会辨别什么是有趣的和值得证明的。”如果计算机能做到这些，人类在该领域的未来地位就很难说了。
德国亚琛工业大学的计算科学家Erika Abraham则对人类数学家的未来更为乐观。“AI系统的聪明程度只能达到我们给它编程的水平”，她说，“智能的不是计算机，而是编程序或训练它的人。”
美国圣塔菲研究所的计算机科学家和认知科学家Melanie Mitchell表示，数学家暂时还不会丢饭碗，除非AI的一个主要缺陷能被攻克——即它们还无法从具体信息中提取抽象概念。“AI系统或许能证明定理，但你首先要提出这些定理背后有意思的抽象数学概念，这比证明定理难多了。”
原文以How will AI change mathematics? Rise of chatbots highlights discussion标题发表在2023年2月17日《自然》的新闻版块上，© nature，doi: 10.1038/d41586-023-00487-2
本文来自微信公众号：Nature Portfolio （ID：nature-portfolio），作者：Davide Castelvecchi