人工智能与数学前沿综述：如何借助 AI 发现数学规律？

1. 人工智能和神经网络的背景知识

2. 计算机辅助数学研究 

自人工智能诞生以来，探索 AI 在数学研究中的应用一直是一个重要的研究方向，并取得了许多重要成果。在符号主义的影响下，A. Newell 和 H. Simon 研发的“逻辑理论家“证明了《数学原理》中多条定理，这是符号主义的成功实践之一。而符号主义的另一重大成果，则是吴文俊先生开创的几何定理机器证明。吴先生利用代数几何，成功的将平面几何表述成一套精确的形式语句，从而可以借助计算机进行推理，实现平面几何定理的机器证明。

计算机辅助数学研究已经取得了一些令人瞩目的成就。例如，图论里经典的四色定理（任何平面上的地图只需要使用最多四种颜色来进行着色，以确保相邻的地区颜色不同）曾被计算机用穷举法证明。最近5年内，用神经网络辅助数学研究比较重要的工作包括：

• 符号回归寻找数学表达式：这种方法从数据中寻找精确的数学表达式，不仅仅是拟合数据，而是在给定的函数库内寻找函数，并通过组合和算术运算来生成一个函数，以拟合数据。这种方法已被用于发现物理学和数学中的精确公式。

• 强化学习构造猜想反例：利用强化学习，研究人员能够构造出猜想的反例，例如在图论中。这种方法可以用于验证某些猜想是否成立，从而发现新的数学性质。

• AI 辅助发现数学规律：通过AI辅助，研究人员已经建立了不同数学领域的规律，包括建立扭结不变量、发现新的矩阵乘法算法以及生成关于基本常数的猜想。这些工作突显了AI在数学研究中的重要作用。

2.1 符号回归寻找数学表达式

线性符号回归（Linear SR）的目标表达式有m个组成部分，单个目标表达式就是m=1的情况。每个部分可以表示成一个函数的线性组合，而这些函数来源于事先设定的函数库里。优化的目标是学习每个线性表达式的系数。如果用监督学习的话，就定一个损失函数，然后最小化损失函数。

而非线性符号回归（Nonlinear SR）将深度神经网络中的激活函数替换成数学算子，从数据中学习数学表达式。

因此，符号回归与传统回归方法核心的不同在于，事先给定了函数库，然后在这个函数库里去选取函数进行线性或非线性的组合，再去优化参数。

（2）基于强化学习的符号回归方法：深度符号回归

Brenden K. Petersen, et al. Deep Symbolic Regression:Recovering Mathematical ExpressionsFrom Data Via Risk-Seeking Policy Gradients. ICLR 2021

基于强化学习的符号回归方法引入了智能体，即深度神经网络。按照数学公式的树表达式法，建立由一些数学符号构成的库，这样每个符号就编码成token，比如一个由四个符号构成的库，每个符号可以编码成一个 4 维的 one-hot 向量。通过约束搜索空间和优化常数，对符号表达式进行约束，例如限制表达式长度、表达式不能全是常数等。通过强化学习进行策略优化，最大化奖励函数来指导生成合适的数学表达式。

图：智能体（深度神经网络）生成树表达式

（3）物理启发的深度符号回归方法

Wassim Tenachi, et al. Deep symbolic regression for physics guided by units constraints: toward the automated discovery of physical laws. arXiv:2303.03192.

物理学领域也应用了深度符号回归方法。这些方法引入物理量纲约束，要求得到的方程必须在物理量纲方面保持平衡。这种方法已经用于发现爱因斯坦的质能方程等已知物理规律。

图：搜索空间

图：搜索空间被物理量纲约束

图：用物理量纲约束的深度符号回归寻找粒子的相对论能量

在物理学中，这种方法已被用于发现一些已知的方程，但对于一些未知的物理规律，目前还没有得出明确的结论。在数学领域，由于大多数基础数学研究者不太关注应用数学或神经网络，因此尚未广泛应用于发现定理。然而，理论上来说，这个方法有巨大的发展潜力，因为数学中的公式比物理中的多得多，而且不像物理那样需要通过实验验证，相对来说验证反馈时间较短。

2.2 强化学习构造猜想反例

Adam. Zsolt. Wagner . “Constructions in combinatorics via neural networks”.arXiv:2104.14516.

2.3 AI 辅助发现数学规律

（1）AI 辅助建立扭结不变量间的联系

Davies. Alex, et al. “Advancing mathematics by guiding human intuition with AI. ” Nature 600 (2021): 70-74.

（2）AI发现矩阵乘法新算法

Fawzi. Alhussein, et al. “Discovering faster matrix multiplication algorithms with reinforcement learning”. Nature 610 (2022): 47-53.

图：Strassen's algorithm 示意图，其中图a是三维情形的矩阵乘法的张量表征,  ai, bi, ci构成一个size为 (4,4,4) 的三维张量；图b展示了 Strassen’s algorithm 中使用的7个乘法；图c展示了将张量分解为7个秩为1的项的和

（3）AI生成关于基本常数的猜想

Gal Raayoni ,et al. Generating conjectures on fundamental constants with the Ramanujan Machine. Nature , 590 (2021): 67-73.

3. 大语言模型在数学研究中的应用

大语言模型的思维链推理

Jason Wei, et al. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. arXiv:2201.11903 [cs.CL]

Kaiyu Yang et al. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. arXiv:2306.15626

4. 人机交互的数学研究平台

如何利用语言大模型，构建一个人机交互的数学研究平台？

数学研究大体分为两个过程：发现数学新命题，证明或证否数学命题。基于这两个基本过程，我们认为人机交互的数学研究平台应该包含如下基本组件：语言大模型 + 符号计算+ 符号回归 + 构造反例 + 自动证明。

语言大模型已经逐渐成为人工智能时代的操作系统，也必将在人机交互的数学研究中发挥基础作用。在数学的发展历程中，许多重大猜想都是依赖数学其他分支的工具和思想得以证明的。由于语言大模型广泛的知识储备，数学家可以通过自然语言与计算机进行交互，整合全领域的数学知识，发现新的数学现象，并借助语言大模型的逻辑推理能力，实现数学命题的证明。然而，现阶段语言大模型在数学推理方面的能力仍然有所欠缺。如何搜集更多的专业数据并开发更强大的算法，改进现有语言大模型的数学推理能力是未来急需解决的重要问题。

在以上基本组件中，语言大模型是一个基础设施，其他组件作为插件部署并被调用。数学家可以借助该平台，通过自然语言与计算机进行交互，实现对数学命题更高效的发现，证明或证否。

经过几个月的努力，DeepMath 研究团队近日发布了 DeepMath 数学大模型，并正在构建人机交互的现代数学研究平台。模型已上传到 Huggingface，感兴趣的朋友可以登录 www.deepmath.cn 通过邀请码注册，在线体验实际效果。 

DeepMath 大模型的特点：

DeepMath 大模型基于 Llama2 微调，显著提升了大模型在现代数学知识问答的能力。为了验证模型效果，我们在线问了一个拓扑学问题：what is a compact topological space? 得到的答案是：A topological space X is compact if every open cover of X has a finite subcover. 回答相当准确！

而如果使用原始 Llama2，会得到怎样的回复呢? 可以参考如下测试结果的截图：

可以看出，尽管原始 Llama2 的回复比较详尽，但是结果并不准确。我们又测试了分析、代数等学科的问题，发现 DeepMath 大模型的效果都相当不错。那么，我们是怎么训练出这种效果呢？

答案还是在于高质量数据集的构建。我们耗费了数月时间人工标注了几千条现代数学知识问答指令，涵盖了微积分，实分析，复分析，概率论，泛函分析，抽象代数，微分方程，微分几何，拓扑学等多个方向。DeepMath大模型正是基于这个高质量的数据集监督微调而来。

为了增强语言大模型的计算能力，我们将 DeepMath 数学大模型与开源数学软件 Sagemath 结合起来。我们构建了一个 Sagemath 代码数据集，并与现代数学知识问答数据集结合，共同微调训练 Llama2，显著提升了模型使用工具与计算能力。

我们将陆续开发符号回归，构造反例，自动证明等组件，并基于AI智能体的思想，将所有组件有效组织起来，从而达到通过自然语言交互并调度各组件，实现对数学命题更高效的发现，证明或证否。

5. 展望：如何借助 AI 发现新的数学概念？

最后，陈小杨老师提出了几个未来AI和数学结合的发展方向：

• 数学对象如何向量化？我们讨论了函数表达式和图的向量化方法，但数学里还有很多其他的数学对象，比如代数结构（如群环域）、几何结构（如流形、代数簇），等等。如何将它们向量化还没有引起大家的关注。

•  怎么用AI发现新的数学概念？

•  如何将神经网络视为特殊函数，用于解决基础数学问题？

数十年来，人工智能的理论发展和技术实践一直与科学探索相伴而生，尤其在以大模型为代表的人工智能技术应用集中爆发的当下，人工智能正在加速物理、化学、生物等基础科学的革新，而这些学科也在反过来启发人工智能技术创新。在此过程中，数学作为兼具理论属性与工具属性的重要基础学科，与人工智能关系甚密，相辅相成。一方面，人工智能在解决数学领域的诸多工程问题、理论问题乃至圣杯难题上屡创记录。另一方面，数学持续为人工智能构筑理论基石并拓展其未来空间。这两个关键领域的交叉融合，正在揭开下个时代的科学之幕。

为了探索数学与人工智能深度融合的可能性，集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师，共同发起“人工智能与数学”读书会，希望从 AI　for　Math，Math　for　AI 两个方面深入探讨人工智能与数学的密切联系。本读书会是“AI+Science”主题读书会的第三季。读书会自9月15日开始，每周五晚20:00-22:00，预计持续时间8～10周。欢迎感兴趣的朋友报名参与！

详情请见：

人工智能与数学读书会启动：AI for Math，Math for AI