一文看懂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
- 清华新VLA框架加速破解具身智能止步实验室“魔咒”,LLM内存开销平均降低4-6倍。2024-11-30
- 智源发布心脏模型!超实时仿真人体生理功能,速度提升180倍2024-11-29
- 乌镇最火AI议题,原来答案藏在这份报告里2024-11-25
- Scaling Law百度最早提出!OpenAI/Claude受它启发,致谢中有Ilya2024-11-28