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
