（阅读本文需要的先决专业知识：无）

如果有人问我在人类实现通用人工智能（AGI）之前还有什么最后需要攻克的难题，那我一定会毫不犹豫地回答：

AI for Math

也就是“使用人工智能来进行数学思考”。为什么这么说呢？简而言之，

对于智能系统，进行数学思考是最困难也是最重要的任务。

最困难，所以有极高的技术门槛；最重要，因为有巨大的应用价值。可见，即便从纯商业的角度来看，AI for Math 也是兵家必争之地，更不用说它可以被看作是人类纯粹的对于理性与智能的上下求索的一种最终形态（这一点我们之后会说明）。（人话版：做 AI for Math 不仅可以让你成为亿万富翁还能让你做21世纪的爱因斯坦）

可是，为什么说 AI for Math 既最困难又最重要呢？之后我们会用几篇系列文章来细说，但现在我可以先用两个例子来从侧面简单说明一下。

ChatGPT 和 AI for Math 的困难性

说 AI for Math 最困难，因为某种程度上来说，这是从2022年有 ChatGPT 以来，所剩无几的未被AI“攻克”的问题之一。现有的像 ChatGPT 这样的AI对话系统，已经能懂人话说人话并像模像样地回答任何问题，很多人已经倾向于认为“AI已经能通过图灵测试”，“NLP不存在了”，有些程序员看到 ChatGPT / Copilot 等工具生成的代码后会同时感觉到惊叹和惶恐……而多模态的AI系统，也已经能像模像样地进行文生图、文生视频等任务，这点除了设计师、艺术家会有失业的忧虑，更有人说像 Sora 这样的AI系统已经能建立世界模型（world models）并自发地学习物理定律……然而，在这一片兴奋与哀嚎的混杂中，有一种声音从来没有出现过：从来没有人觉得数学已经或者马上就要被AI攻克。微软从19年就发起了 IMO Grand Challenge 来寻求能解决国际数学奥林匹克（IMO）级别问题的AI系统，OpenAI、Meta、Google、华为等公司都在定理证明等硬核的 AI for Math 问题上做过前沿探索，但至今这样的AI系统仍未到来（注：AlphaGeometry 解决的平面几何问题是符号方法（如吴方法）几十年前就可以达到100%正确率的问题，并不能算神经网络带来的质的突破）。有些数学家甚至认为一些数学思维如提出新的数学理论、解决未解数学问题等，是理论上都无法被AI解决的。

综上，AI for Math 的困难性可见一斑。

AIMO 竞赛和 AI for Math 的重要性

说 AI for Math 最重要，我们可以用最近一个奖金高达1000万美元的竞赛——AIMO 竞赛来说明。与19年微软发起的 IMO Grand Challenge 初衷类似，由英国量化交易公司 XTX Markets 发起的 Artificial Intelligence Mathematical Olympiad （AIMO）竞赛希望寻求能解决数学奥林匹克（IMO）的开源AI模型和算法。与微软不同的是，AIMO 竞赛设置了1000万美元的奖金。从量化公司或者大型企业的角度来说，1000万美元并不算多，但从技术和科学突破的角度来说，这个竞赛设置的奖金金额相当于

10个诺贝尔奖。

也就是说，“用AI来解决数学奥林匹克竞赛问题”这个问题的价值，（至少）相当于10个诺贝尔奖的金额总和。这合理吗？在我看来，不仅合理，这个竞赛的奖金额度还远远低于 AI for Math 这个问题的价值（这一点我之后会用一篇文章来单独说明）。

综上，AI for Math 的重要性可见一斑。

（数学）推理是什么？

上面我们讨论了关于 AI for Math 的困难性和重要性的两个例子。在下面进一步展开话题之前，有一个我们绕不过的问题，这就是：AI for Math 到底是要做什么？什么叫“进行数学思考”？为此，我们只要回答一个问题就够：

数学推理是什么？

其实，“数学推理是什么”这个问题远没有很多人想象的那么简单。从历史上看，人类花了2000多年才把这个问题想明白。确实，人类从2300多年前古希腊的《几何原本》就开始在进行某种严格的、公理化的数学推演。而真正把“数学推理是什么”这个问题彻底想明白，需等到快20世纪的大数学家希尔伯特(David Hilbert，1862-1943)。

希尔伯特意识到，流传了两千多年的《几何原本》虽然有公理化体系和一定的严谨性，但是细究下来很多地方还是经不起推敲（比如全书第一句话“点是没有部分的”里，“部分”是什么？并没有说明）。于是在他1899年出版的《几何基础》（Grundlagen der Geometrie）一书中，希尔伯特严格化了所有的术语、推导方式和公理，“几何学”过了两千多年在人类历史上第一次真正的严格了。在希尔伯特的体系中，“点”“线”“面”这些字眼都脱离了平常我们熟知的语义，成为了没有意义的词汇，而它们的“意义”侧面体现在与它们相关的一些公理里面（这其实是思想上非常重要的一个飞跃！）。在希尔伯特的体系内，推理成为了一件严格到无懈可击、可以用机械来施行的事情（也正是因为做到了这一点，才使得人类造出现代计算机成为可能！）。

具体来说，希尔伯特的严格推理体系有三个组成部分：

1. 语法（syntax/grammar）：规定了什么样的词语/字符串才是合法的、被容许的（即构成 well-formed formula）。有了一种语法，才有了一门语言，词汇才有了某种结构，而不至于是乱码。有了这种结构，我们才能明确各种关于词汇的操作（比如下面的“推理规则”）;
2. 推理规则（inference rules）：规定了新的事实（定理）如何根据已有的事实（公理或者已经证明的定理）产生。有了推理规则，逻辑系统才动态了起来，成为了一种 calculus（注意这个词不光有“微积分”的意思，它更广义地指代某种能够进行各种运算和操作的系统）。从这一点来说，推理规则可以类比物理里面的动力学方程；
3. 公理（axioms）：约定好的已经成立的事实，无需证明。如果同样对应到物理学里面，可以类比成初始条件。

*注：具体来说，《几何基础》的语法和推理规则基本是一阶逻辑的语法和推理规则。它的公理则是希尔伯特最大的贡献，他选取了能刻画几何学的五组公理（其实这些公理希尔伯特历史上有过多年的查漏补缺和修正，也可见公理选取具有一定的自由度）。值得注意的是，《几何基础》的语法已经有一点类型论（type theory）的影子，它的对象是具有类型的：点、线、面等等。

我们说个大家都熟悉的推理系统：四则运算。四则运算的语法是什么呢？它的语法就是规定得用“0123456789”这十个字符来构成“数”，用“+-×÷”这四个“运算符”与“数”来构成“表达式”，再用“=”这个字符连接两个表达式构成“等式”等等。它的推理规则可以是等式的替换原理(相等的对象可以互相替换)。而“加法口诀”“九九乘法表”等则可以看成是它的一些公理。

时间来到21世纪的今天，事情有什么改变吗？我可以很负责任地告诉你，即便到了发达的21世纪，我们仍然有：

逻辑系统 = 语法 + 推理规则 + 公理

没有变！事实上，今天的前沿研究中仍经常出现的各类形式语言如 Lean、Isabelle、Metamath 等，无一例外都是在以上这个等式的框架下，定义了自己的一套语法、推理规则和公理。

所以，逻辑推理的“物理方程”还是与希尔伯特时代的一样。而在这个系统中，每一步推理都是“几个公理或定理 + 一条推理规则 => 一个新的定理“。说的再宽泛一些，每步推理就是

事实 + 规则 => 新的事实

这就数学推理！而且不光是数学推理，生活中任何严格的推理，本质上都是以上这个过程。甚至更有一类叫做 logic programming 的编程语言，就是完全基于“事实 + 规则 => 新的事实”这件事情来设计的。

注：为了与归纳推理（inductive reasoning）区分开，数学的推理，或者说严格的推理，也叫演绎推理（deductive reasoning）

完美的AI练武场 & 下一个 AlphaGo

（阅读本段需要的先决专业知识：对AI各子领域有一定的了解）

说明白了数学推理的本质，我们来论证下这件事情：

数学是AI完美的练武场。

由“逻辑系统 = 语法 + 推理规则 + 公理”这个等式，我们已经可以望文生义地妄下推测，解决 AI for Math 至少涉及到以下一些前沿领域：

1. 编程语言：如何用严格的语法和编程语言来形式化、严格化、数字化整个现代数学，使得数学定理和证明的正确性能够用机器来自动验证，这本身就已经是个非常有意义的问题。现代形式语言如 Isabelle、Metamath 和最近风头正盛、连陶哲轩都在每天用的 Lean 语言，都是冲着这个目的来设计的。然后除了人工地用形式语言来写数学内容，如何自动地把自然语言书写的数学内容翻译成形式语言，自然也成为了一个重要问题。这个问题也被称为自动形式化（autoformalization）;
2. 数据库：既然推理的每一步都是“事实 + 规则 => 新的事实”，那我们就需要一个东西来保存所有的已有事实。于是，所有已知事实自然地构成了一个数据库。如果没有循环论证，那这个数据库就构成一个有向无环图（directed acyclic graph）。古今中外所有人发表的论文都可以看成是这个图中的一个节点，而论文的引用关系可以看成是这个图的边。如何维护和使用这个数据库，也是一个非常重要的问题。在 LLM 的时代，数据库这个问题与 retrieval augmented generation（RAG）密切相关。所以也是所谓的 AI Agent 的一个重要组成部分。
3. 表示学习：逻辑的、形式的字符串要是想被神经网络处理，免不了有一个表示学习的需求。离散的字符需要通过某种方式变成方便计算的向量或者张量才能被神经网络处理。针对数学推理，是否能有更高效的神经网络架构，是否能设计更合理的 tokenizer 都是一些很好的问题。当然，这一点与各种自然语言的任务也是同理的。
4. 强化学习：从“事实 + 规则 => 新的事实”这一点出发，我们不难联想到强化学习里面的马尔可夫决策过程（Markov decision process）。可以说这就是定义了某种转移函数（transition function）

   从而定义了某种 environment。而 reward function 则可以是在这个 environment 中走到我们想要证明的某些定理时，有一个等于1的 reward（其余时候为0）。从这个意义上讲，AI for Math 可以类比于 AlphaGo，但它的 action space 和 episode 长度都要大得多。有些时候甚至可以说它的 state space 和 action space 都是无穷大……
5. 以数据为中心的AI（data-centric AI）：因为数学和形式语言的严格性，在 AI for Math 的框架内我们可以方便地探讨“数据合成”、“data-centric AI”等问题。在理解数据配比、数据如何被学进参数里等问题时可以天然地有关于数据分布的严格假设。这一点，自然语言的任务是无法比拟的。

我完全有理由相信上面的列表还可以继续列出很多，但即便只看上面列出的几条，我们也能看出 AI for Math 是一个完美的AI练武场。我们需要用到各种最前沿的技术才有希望解决它，所以也很有可能在这些方向催生出新的想法和技术。这个珍贵的练武场，是现在日趋浮躁的AI社区非常需要的。

可以说，AI for Math 就是下一个 AlphaGo，并且难度和重要性都比 AlphaGo 要高出好几个量级！

这种级别的问题，既需要强大的强化学习技术，又需要强大的语言模型，所以也许最有前途的就是

DeepMind + OpenAI

两种路径各取所长，才能打败 AI for Math 这个最终 boss！

广告

OK，今天我们就先简单开启下 AI for Math 这个话题，之后如果大家喜欢我们还会进一步展开。如果你有任何的问题、想讨论的话题或期待看到的话题，欢迎你在文章下留言或给公众号留言～

这里我要毫不违和地打个广告。今年7月在维也纳举行的AI顶级会议 ICML 2024 大会上会举办第一届 AI for Math workshop，会有各种领域大佬演讲和讨论。三个比赛的 track 如果名列前茅还有机会获得奖金、免费会议注册名额和 travel fund。详见下图。

Workshop 链接：

https://sites.google.com/view/ai4mathworkshopicml2024

最后，如果你对 AI for Math 或者 LLM 感兴趣并且在找实习或者找工作，欢迎你在这个公众号留言和投递简历～

彩蛋：发感慨之神经与符号的纠缠