一文看懂AI数学发展现状，清华校友朱松纯学生一作，还整理了份必备阅读清单

杨净 发自 凹非寺

量子位 | 公众号 QbitAI

AI学数学，确实有点火。

且不论这两大领域的大拿纷纷为其站台，就是每次相关进展一出炉，就受到众多关注，比如AI求解偏微分方程。

△每年相关论文估计数量

既然如此，AI学数学到底学得怎么样了。

现在有团队专门梳理了十年发展历程，回顾了关键任务、数据集、以及数学推理与深度学习交叉领域的方法，评估现有的基准和方法，并讨论该领域未来的研究方向。

值得一提的是，他们还很贴心的整理了相关资源，在Github上放上了阅读清单以供食用。

接下来，就带你一文看尽。

一文看懂AI数学发展现状

在这篇调查报告中，作者回顾了深度学习在数学推理方面的进展，主要包括了几个方面。

• 任务和数据集；
• 神经网络和预训练语言模型；
• 大型语言模型的语境学习；
• 现有基准和未来方向。

首先，作者梳理了目前可用于深度学习数学推理的各种任务和数据集，大体任务主要分为这几个大类。

数学应用题MWP

几十年来，开发自动解决数学应用题的算法，一直是NLP研究方向所在。一个涉及人物、实体和数量的简短表述，可用一组方程来模拟，方程的解法揭示了问题的最终答案。

MWPs对NLP系统的挑战在于对语言理解、语义解析和多种数学推理能力的需求。

大多数MWP数据集都提供了注释方程来解决。为了提高求解器的性能和可解释性，MathQA用精确的操作程序进行注释；MathQA-Python则提供具体的Python程序；还有数据集采用多步骤的自然语言，来对问题进行注释，这样更适合人类的阅读。Lila用Python程序的原理注释了许多前面提到的MWP数据集。

定理证明TP

即问题是通过一连串的逻辑论证来证明一个数学主张的真理。最近，人们对于交互式定理证明器 （ITP）中使用语言模型来进行定理证明的关注越来愈多。

为了在ITP中证明一个定理，首先需用编程语言来陈述，然后通过生成 “证明步骤 “来简化，直到它被简化为已知事实。其结果是一个步骤序列，构成一个验证的证明。

其数据源包括与ITP对接的交互式学习环境，从ITP库证明中得到的数据集，比如CoqGym、Isabelle、Lean、Lean-Gym、miniF2F等。

几何问题解决GPS

与数学单词问题不同，几何问题解决（GPS）是由自然语言和几何图组成。多模态输入包括了几何元素的实体、属性和关系，而目标是找到未知变量的数学解。

基于这样的特性，用深度学习来解决GPS问题就颇具挑战，因为它涉及解析多模态信息、符号抽象、使用定理知识和进行定量推理的能力。

早期数据集相对较小或不公开，也就限制了深度学习方法的发展。为应对这一限制，有包括Geometry3K（由3002个几何问题组成，并对多模态输入进行了统一的逻辑形式注释）、以及新出炉的GeoQA、GeoQA+、UniGeo的引入。

数学问答MathQA

数字推理是人类智力中的一种核心能力，在许多NLP任务中发挥着重要作用。除了定理证明、数学应用题之外，还有一系列围绕数学推理的QA基准。

近段时间相关数据集大量诞生，比如QuaRel、McTaco、Fermi等，但最新研究表明，最先进的数学推理系统可能存在推理的脆性，即模型依靠虚假信号来达到看上去令人满意的性能。

为了解决这一问题，在各个方面诞生了新基准，比如MATH，由具有挑战性的竞赛数学组成，以衡量模型在复杂情况下的问题解决能力。

除此之外，还有一些其他的数学任务，作者还专门汇总了表格，梳理了各个任务的相关数据集。

三大深度神经网络模型

接着，团队梳理在数学推理任务中，主要使用的几大深度神经网络模型。

Seq2Seq网络，已成功应用于上述四种关键任务当中。它使用编码器-解码器架构，将数学推理形式化为一个序列生成任务，基本思路是将输入序列（如数学问题）映射到输出序列（ 如方程式、程序和证明）。常见的编码器和解码器包括LSTM、GRU等。

基于图的数学网络。一些特定的数学表达式（比如AST、图）所蕴含的结构化信息，并不能被Seq2Seq方法明确地建模。为了解决这个问题， 基于图的神经网络来模拟表达式中的结构。比如Sequence-to-tree模型、ASTactic等模型。

基于注意力的数学网络，注意力机制已成功应用于NLP、CV等问题中，在解码过程中考虑了输入的隐藏变量。最近，研究人员发现，它可以用来识别数学概念之间的重要关系，已被应用于数学应用题（MATH-EN）、几何题、定理证明。

除此之外，还有CNN、多模态网络等，在这个领域，视觉输入使用ResNet或Faster-RCNN进行编码，而文本表示则通过GRU或LTSM获得。随后，使用多模态融合模型学习联合表示，如BAN、FiLM和DAFA。

在特定任务中，有使用擅长空间推理的GNN，用于几何问题解析；WaveNet被应用于定理证明，由于其能够解决纵向时间序列数据；还有Transformer生成数学方程等。

这其中，频频出现进展的，效果惊艳的大语言模型，在数学推理上表现得又是如何呢？

事实上存在一些挑战，首先，因为模型训练并非专门针对数学数据的训练，所以在数学任务的熟练程度低于自然语言任务。而且相较于其他任务数据，数学数据相对较少；其次，预训练模型规模的增长，让下游特定任务从头训练成本很高；最后，从目标来看，模型可能很难学习数学表示或高级推理技能。

作者分析了自监督学习、特定任务微调两种表现。

而在现有数据集和基准的分析中，研究团队看到了一些缺陷，包括对对低资源环境的关注有限、不充分的数字表示、不一致的推理能力。

最后，团队从泛化和鲁棒性、可信的推理、从反馈中学习、多模态数学推理等方面探讨了未来的研究方向。

还整理了份AI数学阅读清单

这篇关于AI数学的调查报告，由UCLA、圣母大学、华盛顿大学等机构的研究人员共同完成。

第一作者是来自UCLA的Pan Lu，目前正读博四，受到KaiWei Chang、朱松纯等教授指导，此前曾获清华硕士学位。

共同作者还有同样是UCLA的邱亮，今年毕业已是亚马逊Alexa AI的应用科学家，曾受朱松纯和Achuta Kadambi教授的指导，是上海交大校友。

他们还整理了份数学推理和人工智能研究课题的阅读清单，放在GitHub上。

感兴趣的旁友，可戳下方链接了解更多~
https://github.com/lupantech/dl4math
论文链接：
https://arxiv.org/abs/2212.10535