本文约5500字，建议阅读11分钟本文先容了最新发布的 DeepMath 数学大模型。


[ 导语 ] 为了探索数学与人工智能深度领悟的可能性，集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师，共同发起“人工智能与数学”读书会，希望从 AI　for　Math，Math　for　AI 两个方面深入磋商人工智能与数学的密切联系。

在人工智能与数学读书会第一期，陈小杨老师磋商了符号回归、强化学习布局反例、AI赞助创造数学规律，以及大措辞模型在数学研究中的运用，并分享了一些最新研究成果。
在以 ChatGPT 为代表的大措辞模型集中爆发确当下，如何利用措辞大模型，构建一个人机交互的数学研究平台？陈老师先容了最新发布的 DeepMath 数学大模型。
本文是这次读书会的笔墨整理。

读书会回放***已上线，欢迎感兴趣的朋友报名读书会，不雅观看回放***

https://pattern.swarma.org/study_group_issue/518

研究领域：AI for Math，符号回归，强化学习，大措辞模型

目录

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

2. 打算机赞助数学研究

2.1 符号回归探求数学表达式

2.2 强化学习布局猜想反例

2.3 AI 赞助创造数学规律

3. 大措辞模型在数学研究中的运用

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

5. 展望：如何借助 AI 创造新的数学观点？

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

回顾人工智能和神经网络的发展历史，人工智能（Artificial Intelligence）是指让机器具有人类的智能，其出身的标志性事宜是1956 年的达特茅斯（Dartmouth）会议，在这次会议 上，“人工智能”被提出并作为本研究领域的名称。

图：人工智能的发展历史与标志性事宜

神经网络在数学上可以被解读为一种分外的函数。
这种函数通过自变量x的线性组合，然后通过激活函数φ进行处理，再进行线性组合后得到输出。
φ函数可以有多层，构成复合函数。

图：人工神经网络（Artificial Neural Network）

通用近似定理

在数学里，对付任何一个连续函数，总是可以找到一个多项式函数或者三角基数去逼近它。

然而，神经网络这一类分外的函数在根本数学里并没有被广泛运用。
只管如此，打算数学领域已经利用神经网络来办理一些传统数学方法难以办理的问题。
例如，利用神经网络去办理一些多尺度建模的问题。

2. 打算机赞助数学研究

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

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

符号回归探求数学表达式：这种方法从数据中探求精确的数学表达式，不仅仅是拟合数据，而是在给定的函数库内探求函数，并通过组合和算术运算来天生一个函数，以拟合数据。
这种方法已被用于创造物理学和数学中的精确公式。
强化学习布局猜想反例：利用强化学习，研究职员能够布局出猜想的反例，例如在图论中。
这种方法可以用于验证某些猜想是否成立，从而创造新的数学性子。
AI 赞助创造数学规律：通过AI赞助，研究职员已经建立了不同数学领域的规律，包括建立扭结不变量、创造新的矩阵乘法算法以及天生关于基本常数的猜想。
这些事情突显了AI在数学研究中的主要浸染。

2.1 符号回归探求数学表达式

符号回归（symbolic regression）是一种从数据中探求精确数学表达式的方法。
与通用逼近理论不同，符号回归在给定一组输入和输出数据的情形下，试图找到一个函数来精确拟合这些数据。
但这个函数是从一个事先定义好的函数库中选择的。
这个库可以包含对数函数、三角函数、多项式函数等可能的函数。
通过组合和基本算术运算，我们可以天生一个函数，以最好地拟合数据。

符号回归的主要性在于，它能够挖掘出物理学和数学中的第一性事理或精确公式，而不是像传统神经网络一样用一个近似的函数去逼近数据。
这使得符号回归天生的函数具有可阐明性。
近年来，这种方法已被物理学家用于创造许多已知规律，如万有引力定律、爱因斯坦质能方程，以及费曼物理学讲义里很多已有的物理规律。
然而，尚未通过这种方法创造未知的新规律，这可能是未来的研究方向。

就详细方法而言，符号回归方法可以通过向量化数学表达式来实现。
它将数学表达式分解为单元，比如前缀表达式（即波兰表示法 Polish Notation，1920 年，波兰科学家扬 · 武卡谢维奇（Jan ukasiewicz）发明了一种不须要括号的打算表达式的表示法，将操作符号写在操作数之前）。
类似于自然措辞处理中把一个繁芜的语句拆分成基本token的方法，一个繁芜的数学表达式也可以被拆分成一些小token。
然后，将token序列作为输入，利用机器学习模型进行演习，天生新的token序列，然后利用规则将其还原为数学表达式。

在演习方面，可以运用传统的机器学习方法，如线性回归、非线性回归、Transformer 架构、强化学习，或在网络构造中加入一些物理、数学或其他学科的先验知识来约束搜索空间。

图：各种方法的数学工具，表达式，参数集和搜索空间

（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.

另一个令人激动的领域是利用强化学习布局猜想反例。
以图论为例，先将图编码为毗邻矩阵，然后将毗邻矩阵转化为向量作为神经网络的输入，并根据环境反馈打算褒奖，最后进行策略优化。

下面这个例子是图论里一个猜想，

作者用强化学习布局出了这个猜想的一个反例，天生了一个图，使得这个图不知足这个假设。
布局反例的核心思想是让不等式的左边小于右边，以是褒奖函数可以设置为负的左边表达式，然后最大化褒奖函数。
对付n<=18, 这个猜想是成立的。
但当n=19时, 利用强化学习算法迭代，找到了反例。

2.3 AI 赞助创造数学规律

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

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

扭结是三维欧氏空间或者三维球面中的大略闭合曲线。
为了区分两个扭结是否等价，即是否可以将一个扭结变形成另一个，人们引入了扭结不变量。
扭结不变量有很多种，个中最著名的便是Jones Polynomial。
为了探索不同的扭结不变量之间的关系，作者通过演习AI然后人工反馈从而找到一些规律。

详细来讲，模型演习了一个前馈神经网络来评估扭结的几何和代数不变量之间是否存在关系，根据随机采样的扭结数据集上的几何不变量来预测代数特色。
为了理解网络是如何做出这一预测的，他们利用了基于梯度的归因技能来确定哪些几何不变量与代数特色最干系。
通过人工反馈的办法，他们预测到了这个不等式，然后进一步又在另一篇论文里严格证明了这个不等式。
以是这项事情是AI赞助创造了数学定理。

图：各种扭结及其对应的几何不变量与代数不变量

（2）AI创造矩阵乘法新算法

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

在矩阵乘法领域，AI的运用也引人瞩目。
研究职员创造了更快的矩阵乘法算法，通过强化学习将乘法运算次数降落到最低。
比如，对付一个22的矩阵，标准的矩阵乘法要做8次乘法，而他们用强化学习探求出一个新算法，把乘法运算减少到了7次。

图：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. 大措辞模型在数学研究中的运用

近期人工智能大模型成为最热门的话题之一。
作为措辞大模型最具影响力的产品，ChatGPT引发了一场新的家当革命。

大措辞模型的演习路线如下：

措辞模型预演习 → 有监督指令微调 → 褒奖模型演习 → 强化学习

大措辞模型的思维链推理

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

这篇论文用大模型跟其余一套形式化的措辞Lean去进行交互。
Lean是一种形式化的措辞，它将数学措辞转化成打算机措辞，然后在这个措辞框架下去进行严格的推理。
以是可以确保它的推理准确性频年夜模型要高。
微软开拓了Lean这个库，把很多数学知识变成了这种措辞，涵盖上至本科数学的知识。
LeanDojo基于已有的库，把打算机措辞还原整天然措辞，利用思维链 (chain-of-thought) 推理，把证明过程放到大模型里去演习，然后做微调，以提升大模型的能力。

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创造新的数学观点？如何将神经网络视为分外函数，用于办理根本数学问题？

期待和更多朋友一起探索！

学者简介:

陈小杨，同济大学特聘研究员。
2014年5月得到美国圣母大学数学博士学位，2014-2016年在澳门大学从事博士后研究，并于2016年底入职同济大学。
陈小杨的紧张研究方向为黎曼几何，在 Geometry and Topology, Advances in Mathematics 等期刊揭橥了多篇研究论文。
近期，陈小杨与研究团队开展了大模型在根本数学的运用研究，并操持开拓机器学习算法用于创造数学规律，布局数学猜想反例等。