图1
文 | 董彬
数学自古以来一直被视作挑战人类智力极限的领域。然而，伴随着人工智能技术的崛起和不断发展，诸如深度学习和强化学习等技术已开始在数学推理等方面展现出令人赞叹的能力。这不仅激发了数学家们的前沿探索和科学创新，更为数学的未来发展推开了新的大门。
在数学的发展历程中，许多重大猜想都是依赖于数学其他分支的工具和思想得以证明的。然而，随着数学发展的深入，其专业化程度日益提高，各分支的研究也变得越来越深入，使得跨分支工具的应用变得更加困难。这无疑限制了我们对数学工具的有效利用。然而，如今大型语言模型的能力恰好能够整合并运用数百年甚至上千年的跨学科知识，以此发挥出无比强大的力量。这就是AI for Mathematics（简称AI4M）的核心动力。
AI4M的主要任务包括定理证明、定理生成、反例生成等等，核心工作模式可以分为全自动、交互式和AI启发三种。全自动模式中，人工智能主导整个猜想生成、证明或证伪的全流程，人类的参与度较低；交互式模式下，人工智能与人类进行深度互动，共同推动猜想的提出和证明；而在AI启发模式中，人工智能作为一种启发工具，由人类来主导。这些任务与形式都在“数学机械化”的讨论范畴之内，尽管这是一个古老的议题，但为何近期再度引起了广泛关注？关键在于近年来人工智能的飞速发展，特别是以GPT-4为代表的大型语言模型的诞生，使人们看到了实现上述愿景的可能，同时也预示着数学智能化的广阔前景。2021年底，⾕歌的 DeepMind 与著名数学家 Geordie Williamson 展开了合作，尝试运⽤机器学习⼯具来协助数学家的研究[文献1]，这属于前述的“AI启发”⼯作模式。在这次研究中，数学家们⾸次采⽤⼈⼯智能⼯具寻找灵感并提出新的数学定理，为拓扑学和表示论领域提供了成功的案例。同⼀时期，北京国际数学研究中⼼也举办了新年特别数学报告会“AI 与纯数学”，围绕这个主题展开了深⼊讨论。新年特别数学报告会现场，左上和右上分别为报告人董彬和刘毅老师
为了验证这种工作模式在纯数学研究中的广泛适用性，我和我的博士生金鹏飞，以及在北京国际数学研究中心工作的余庆超博士，与香港中文大学数学系的何旭华教授和Felix Schremmer博士，联手对算术代数几何领域中的仿射Deligne-Lusztig簇（ADLV）的核心问题进行了研究。经过一年多的时间，我们取得了一些令人振奋的进展，这在一定程度上验证了该工作模式的可推广性。2023年3月，OpenAI发布了最新的大型语言模型GPT-4。与其前任GPT-3.5相比，GPT-4的最大进步在于其逻辑推理能力。GPT-4并不是一个搜索引擎，而是一个强大的推理引擎。当我们需要寻找观点或者希望对自身关心的问题获得启发时，我们需要的是一个具备强大逻辑推理能力的引擎，把观点和概念组织好，然后以对话的形式告诉我们，GPT-4正是这样的存在。GPT-4在数学和物理领域的表现可圈可点。例如，一位北京国际数学研究中心的青年教师使用GPT-4作答了2018年北京大学的线性代数B期末考试题，尽管这份试卷被视为难度较大，但GPT-4仍取得了接近平均分的成绩；另一位青年教师让GPT-4作答了一道数学模型的试题，该老师评价GPT-4给出的答案要比标准答案更完整。量子计算专家Scott Aaronson甚至用他引以为豪的量子计算期末考试来测试GPT-4，结果GPT-4取得了B级的成绩。当然，我们并不能宣称GPT-4已经超越了人类专家在所有领域的表现，但其广泛的知识储备和强大的逻辑推理能力已经让人们对人工智能的未来充满期待。然而，GPT-4在数学推理方面的能力依然有所欠缺，正如论文[文献2]中所述，GPT-4并不擅长“plan ahead”——即主动探索不同的逻辑推理路径并评估其正确性。虽然我们可以通过更聪明的方式去引导它（如通过提示词工程，Prompt Engineering）——例如使用思维链（Chain of Thoughts，CoT）[文献3]或思维树（Tree of Thoughts，ToT）[文献4]，GPT-4处理复杂逻辑推理的能力还有待提升。无论是DeepMind提出的AI启发的工作模式，还是对GPT-4进行提问，我们都需要面对一个核心问题：如何快速理解并验证AI的结果？因此，我们需要构建一个能自动验证数学推理正确性的“数学模拟器”。构建“数学模拟器”需要对数学进行形式化。数学形式化是把数学理论表述成一套精确、形式的语句的过程。这些语句通常由基础概念、定义和公理构建，并使用特定的逻辑系统（如谓词逻辑、一阶逻辑或二阶逻辑）进行推理。数学形式化排除了因为语言、直觉和经验等因素带来的模糊性，系统化地解决数学问题。这个过程有助于发现概念和推理中的不足，也对开发新的数学理论和检验数学证明的正确性起着重要的作用。就算抛开人工智能不谈，数学的形式化对数学本身的意义也十分重大。2014年，菲尔兹奖获得者Vladimir Voevodsky在美国Institute for Advanced Study的一个报告中指出，一些复杂的数学证明中的错误可能需要数年才能被发现，这促使他开始思考利用计算机来验证数学推理的可能性。2021年，Peter Scholze在Johan Commelin的帮助下使用一个形式化验证系统验证了他自称“自己迄今为止最重要的一个定理”的证明[文献5]。他们使用的形式化验证系统称为Lean。Lean是一个定理证明器和编程语言，由Leonardo de Moura在2013年在微软研究院推出。截至2023年3月，Lean的数学数据库Mathlib已经包含了超过110,000个定理和1,100,000行代码。Mathlib的主要贡献者是Thomas Hales和Kevin Buzzard，后者在2022年的国际数学家大会（ICM）上受邀发表一小时的演讲，介绍了Lean和数学形式化验证的最新进展。对于AI4M的未来发展，我认为存在两个并行的路径值得深入探索。一方面，我们可以为数学家们定制轻量级的AI工具，比如我们与何旭华教授的合作模式，或者通过词提示工程（Prompt Engineering）为数学家量身定制个性化的AI助手，以进行深度讨论并启发其思维。另一方面，我们需要积极推动数学知识的形式化，尽可能快地构建“数学模拟器”，这可能需要人力的组织和自动化的形式化工具的开发。在拥有了这样的模拟环境后，我们就可以训练一个能在这个模拟环境中进行严谨数学推理的AI模型。回到AI4M的初衷，整合并高效利用全领域的数学知识至关重要。例如，去年的菲尔兹奖得主June Huh将代数几何领域的工具（Hodge theory）引入到组合数学领域，成功解决了该领域的一些重要问题。AI4M的最终目标就是通过人工智能技术整合全领域的数学知识，为数学家提供智能化的副驾驶（Co-Pilot），使他们能够更加高效地运用数学工具解决更具挑战性的数学问题。注：文中的图1至3由董彬老师以自然语言提示midjourney绘制而成。1. Davies, Alex, et al. "Advancing mathematics by guiding human intuition with AI." Nature 600.7887 (2021): 70-74.2. Bubeck, Sébastien, et al. "Sparks of artificial general intelligence: Early experiments with GPT-4." arXiv preprint arXiv:2303.12712 (2023).3. Wei, Jason, et al. "Chain of thought prompting elicits reasoning in large language models." arXiv preprint arXiv:2201.11903 (2022).4. Yao, Shunyu, et al. "Tree of thoughts: Deliberate problem solving with large language models." arXiv preprint arXiv:2305.10601 (2023).5. https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/作者简介
董彬，北京大学北京国际数学研究中心长聘教授、国际机器学习研究中心副主任、国家生物医学成像科学中心研究员，北京大学长沙计算与数字经济研究院副院长。2003年本科毕业于北京大学数学科学学院，2005年在新加坡国立大学数学系获得硕士学位，2009年在美国加州大学洛杉矶分校数学系获得博士学位。主要研究领域为科学计算、机器学习及其在计算成像和数据分析中的应用。2014年获得求是杰出青年学者奖，2022年受邀在世界数学家大会（ICM）做45分钟报告。