一文看懂AI數(shù)學(xué)發(fā)展現(xiàn)狀，清華校友朱松純學(xué)生一作，還整理了份必備閱讀清單

白交 2022-12-31 13:53:49 來(lái)源：量子位

楊凈 發(fā)自 凹非寺

量子位 | 公眾號(hào) QbitAI

AI學(xué)數(shù)學(xué)，確實(shí)有點(diǎn)火。

且不論這兩大領(lǐng)域的大拿紛紛為其站臺(tái)，就是每次相關(guān)進(jìn)展一出爐，就受到眾多關(guān)注，比如AI求解偏微分方程。

△每年相關(guān)論文估計(jì)數(shù)量

既然如此，AI學(xué)數(shù)學(xué)到底學(xué)得怎么樣了。

現(xiàn)在有團(tuán)隊(duì)專門梳理了十年發(fā)展歷程，回顧了關(guān)鍵任務(wù)、數(shù)據(jù)集、以及數(shù)學(xué)推理與深度學(xué)習(xí)交叉領(lǐng)域的方法，評(píng)估現(xiàn)有的基準(zhǔn)和方法，并討論該領(lǐng)域未來(lái)的研究方向。

值得一提的是，他們還很貼心的整理了相關(guān)資源，在Github上放上了閱讀清單以供食用。

接下來(lái)，就帶你一文看盡。

一文看懂AI數(shù)學(xué)發(fā)展現(xiàn)狀

在這篇調(diào)查報(bào)告中，作者回顧了深度學(xué)習(xí)在數(shù)學(xué)推理方面的進(jìn)展，主要包括了幾個(gè)方面。

• 任務(wù)和數(shù)據(jù)集；
• 神經(jīng)網(wǎng)絡(luò)和預(yù)訓(xùn)練語(yǔ)言模型；
• 大型語(yǔ)言模型的語(yǔ)境學(xué)習(xí)；
• 現(xiàn)有基準(zhǔn)和未來(lái)方向。

首先，作者梳理了目前可用于深度學(xué)習(xí)數(shù)學(xué)推理的各種任務(wù)和數(shù)據(jù)集，大體任務(wù)主要分為這幾個(gè)大類。

數(shù)學(xué)應(yīng)用題MWP

幾十年來(lái)，開發(fā)自動(dòng)解決數(shù)學(xué)應(yīng)用題的算法，一直是NLP研究方向所在。一個(gè)涉及人物、實(shí)體和數(shù)量的簡(jiǎn)短表述，可用一組方程來(lái)模擬，方程的解法揭示了問題的最終答案。

MWPs對(duì)NLP系統(tǒng)的挑戰(zhàn)在于對(duì)語(yǔ)言理解、語(yǔ)義解析和多種數(shù)學(xué)推理能力的需求。

大多數(shù)MWP數(shù)據(jù)集都提供了注釋方程來(lái)解決。為了提高求解器的性能和可解釋性，MathQA用精確的操作程序進(jìn)行注釋；MathQA-Python則提供具體的Python程序；還有數(shù)據(jù)集采用多步驟的自然語(yǔ)言，來(lái)對(duì)問題進(jìn)行注釋，這樣更適合人類的閱讀。Lila用Python程序的原理注釋了許多前面提到的MWP數(shù)據(jù)集。

定理證明TP

即問題是通過一連串的邏輯論證來(lái)證明一個(gè)數(shù)學(xué)主張的真理。最近，人們對(duì)于交互式定理證明器?（ITP）中使用語(yǔ)言模型來(lái)進(jìn)行定理證明的關(guān)注越來(lái)愈多。

為了在ITP中證明一個(gè)定理，首先需用編程語(yǔ)言來(lái)陳述，然后通過生成 “證明步驟 “來(lái)簡(jiǎn)化，直到它被簡(jiǎn)化為已知事實(shí)。其結(jié)果是一個(gè)步驟序列，構(gòu)成一個(gè)驗(yàn)證的證明。

其數(shù)據(jù)源包括與ITP對(duì)接的交互式學(xué)習(xí)環(huán)境，從ITP庫(kù)證明中得到的數(shù)據(jù)集，比如CoqGym、Isabelle、Lean、Lean-Gym、miniF2F等。

幾何問題解決GPS

與數(shù)學(xué)單詞問題不同，幾何問題解決（GPS）是由自然語(yǔ)言和幾何圖組成。多模態(tài)輸入包括了幾何元素的實(shí)體、屬性和關(guān)系，而目標(biāo)是找到未知變量的數(shù)學(xué)解。

基于這樣的特性，用深度學(xué)習(xí)來(lái)解決GPS問題就頗具挑戰(zhàn)，因?yàn)樗婕敖馕龆嗄B(tài)信息、符號(hào)抽象、使用定理知識(shí)和進(jìn)行定量推理的能力。

早期數(shù)據(jù)集相對(duì)較小或不公開，也就限制了深度學(xué)習(xí)方法的發(fā)展。為應(yīng)對(duì)這一限制，有包括Geometry3K（由3002個(gè)幾何問題組成，并對(duì)多模態(tài)輸入進(jìn)行了統(tǒng)一的邏輯形式注釋）、以及新出爐的GeoQA、GeoQA+、UniGeo的引入。

數(shù)學(xué)問答MathQA

數(shù)字推理是人類智力中的一種核心能力，在許多NLP任務(wù)中發(fā)揮著重要作用。除了定理證明、數(shù)學(xué)應(yīng)用題之外，還有一系列圍繞數(shù)學(xué)推理的QA基準(zhǔn)。

近段時(shí)間相關(guān)數(shù)據(jù)集大量誕生，比如QuaRel、McTaco、Fermi等，但最新研究表明，最先進(jìn)的數(shù)學(xué)推理系統(tǒng)可能存在推理的脆性，即模型依靠虛假信號(hào)來(lái)達(dá)到看上去令人滿意的性能。

為了解決這一問題，在各個(gè)方面誕生了新基準(zhǔn)，比如MATH，由具有挑戰(zhàn)性的競(jìng)賽數(shù)學(xué)組成，以衡量模型在復(fù)雜情況下的問題解決能力。

除此之外，還有一些其他的數(shù)學(xué)任務(wù)，作者還專門匯總了表格，梳理了各個(gè)任務(wù)的相關(guān)數(shù)據(jù)集。

三大深度神經(jīng)網(wǎng)絡(luò)模型

接著，團(tuán)隊(duì)梳理在數(shù)學(xué)推理任務(wù)中，主要使用的幾大深度神經(jīng)網(wǎng)絡(luò)模型。

Seq2Seq網(wǎng)絡(luò)，已成功應(yīng)用于上述四種關(guān)鍵任務(wù)當(dāng)中。它使用編碼器-解碼器架構(gòu)，將數(shù)學(xué)推理形式化為一個(gè)序列生成任務(wù)，基本思路是將輸入序列（如數(shù)學(xué)問題）映射到輸出序列（ 如方程式、程序和證明）。常見的編碼器和解碼器包括LSTM、GRU等。

基于圖的數(shù)學(xué)網(wǎng)絡(luò)。一些特定的數(shù)學(xué)表達(dá)式（比如AST、圖）所蘊(yùn)含的結(jié)構(gòu)化信息，并不能被Seq2Seq方法明確地建模。為了解決這個(gè)問題， 基于圖的神經(jīng)網(wǎng)絡(luò)來(lái)模擬表達(dá)式中的結(jié)構(gòu)。比如Sequence-to-tree模型、ASTactic等模型。

基于注意力的數(shù)學(xué)網(wǎng)絡(luò)，注意力機(jī)制已成功應(yīng)用于NLP、CV等問題中，在解碼過程中考慮了輸入的隱藏變量。最近，研究人員發(fā)現(xiàn)，它可以用來(lái)識(shí)別數(shù)學(xué)概念之間的重要關(guān)系，已被應(yīng)用于數(shù)學(xué)應(yīng)用題（MATH-EN）、幾何題、定理證明。

除此之外，還有CNN、多模態(tài)網(wǎng)絡(luò)等，在這個(gè)領(lǐng)域，視覺輸入使用ResNet或Faster-RCNN進(jìn)行編碼，而文本表示則通過GRU或LTSM獲得。隨后，使用多模態(tài)融合模型學(xué)習(xí)聯(lián)合表示，如BAN、FiLM和DAFA。

在特定任務(wù)中，有使用擅長(zhǎng)空間推理的GNN，用于幾何問題解析；WaveNet被應(yīng)用于定理證明，由于其能夠解決縱向時(shí)間序列數(shù)據(jù)；還有Transformer生成數(shù)學(xué)方程等。

這其中，頻頻出現(xiàn)進(jìn)展的，效果驚艷的大語(yǔ)言模型，在數(shù)學(xué)推理上表現(xiàn)得又是如何呢？

事實(shí)上存在一些挑戰(zhàn)，首先，因?yàn)槟Ｐ陀?xùn)練并非專門針對(duì)數(shù)學(xué)數(shù)據(jù)的訓(xùn)練，所以在數(shù)學(xué)任務(wù)的熟練程度低于自然語(yǔ)言任務(wù)。而且相較于其他任務(wù)數(shù)據(jù)，數(shù)學(xué)數(shù)據(jù)相對(duì)較少；其次，預(yù)訓(xùn)練模型規(guī)模的增長(zhǎng)，讓下游特定任務(wù)從頭訓(xùn)練成本很高；最后，從目標(biāo)來(lái)看，模型可能很難學(xué)習(xí)數(shù)學(xué)表示或高級(jí)推理技能。

作者分析了自監(jiān)督學(xué)習(xí)、特定任務(wù)微調(diào)兩種表現(xiàn)。

而在現(xiàn)有數(shù)據(jù)集和基準(zhǔn)的分析中，研究團(tuán)隊(duì)看到了一些缺陷，包括對(duì)對(duì)低資源環(huán)境的關(guān)注有限、不充分的數(shù)字表示、不一致的推理能力。

最后，團(tuán)隊(duì)從泛化和魯棒性、可信的推理、從反饋中學(xué)習(xí)、多模態(tài)數(shù)學(xué)推理等方面探討了未來(lái)的研究方向。

還整理了份AI數(shù)學(xué)閱讀清單

這篇關(guān)于AI數(shù)學(xué)的調(diào)查報(bào)告，由UCLA、圣母大學(xué)、華盛頓大學(xué)等機(jī)構(gòu)的研究人員共同完成。

第一作者是來(lái)自UCLA的Pan Lu，目前正讀博四，受到KaiWei Chang、朱松純等教授指導(dǎo)，此前曾獲清華碩士學(xué)位。

共同作者還有同樣是UCLA的邱亮，今年畢業(yè)已是亞馬遜Alexa AI的應(yīng)用科學(xué)家，曾受朱松純和Achuta Kadambi教授的指導(dǎo)，是上海交大校友。

他們還整理了份數(shù)學(xué)推理和人工智能研究課題的閱讀清單，放在GitHub上。

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