首頁 > 歷史

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

作者:由 創業邦 發表于 歷史日期:2023-01-26

如何表示文章共同一作

編者按:本文來自微信公眾號 量子位(ID:QbitAI),創業邦經授權釋出。

AI學數學,確實有點火。

且不論這兩大領域的大拿紛紛為其站臺,就是每次相關進展一出爐,就受到眾多關注,比如AI求解偏微分方程。

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

既然如此,AI學數學到底學得怎麼樣了。

現在有團隊專門梳理了十年發展歷程,回顧了關鍵任務、資料集、以及數學推理與深度學習交叉領域的方法,評估現有的基準和方法,並討論該領域未來的研究方向。

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

接下來,就帶你一文看盡。

一文看懂AI數學發展現狀

在這篇調查報告中,作者回顧了深度學習在數學推理方面的進展,主要包括了幾個方面。

任務和資料集;

神經網路和預訓練語言模型;

大型語言模型的語境學習;

現有基準和未來方向。

首先,作者梳理了目前可用於深度學習數學推理的各種任務和資料集,大體任務主要分為這幾個大類。

1、數學應用題MWP

幾十年來,開發自動解決數學應用題的演算法,一直是NLP研究方向所在。一個涉及人物、實體和數量的簡短表述,可用一組方程來模擬,方程的解法揭示了問題的最終答案。

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

MWPs對NLP系統的挑戰在於對語言理解、語義解析和多種數學推理能力的需求。

大多數MWP資料集都提供了註釋方程來解決。為了提高求解器的效能和可解釋性,MathQA用精確的操作程式進行註釋;MathQA-Python則提供具體的Python程式;還有資料集採用多步驟的自然語言,來對問題進行註釋,這樣更適合人類的閱讀。Lila用Python程式的原理註釋了許多前面提到的MWP資料集。

2、定理證明TP

即問題是透過一連串的邏輯論證來證明一個數學主張的真理。最近,人們對於互動式定理證明器(ITP)中使用語言模型來進行定理證明的關注越來愈多。

為了在ITP中證明一個定理,首先需用程式語言來陳述,然後透過生成 “證明步驟 “來簡化,直到它被簡化為已知事實。其結果是一個步驟序列,構成一個驗證的證明。

其資料來源包括與ITP對接的互動式學習環境,從ITP庫證明中得到的資料集,比如CoqGym、Isabelle、Lean、Lean-Gym、miniF2F等。

3、幾何問題解決GPS

與數學單詞問題不同,幾何問題解決(GPS)是由自然語言和幾何圖組成。多模態輸入包括了幾何元素的實體、屬性和關係,而目標是找到未知變數的數學解。

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

基於這樣的特性,用深度學習來解決GPS問題就頗具挑戰,因為它涉及解析多模態資訊、符號抽象、使用定理知識和進行定量推理的能力。

早期資料集相對較小或不公開,也就限制了深度學習方法的發展。為應對這一限制,有包括Geometry3K(由3002個幾何問題組成,並對多模態輸入進行了統一的邏輯形式註釋)、以及新出爐的GeoQA、GeoQA+、UniGeo的引入。

4、數學問答MathQA

數字推理是人類智力中的一種核心能力,在許多NLP任務中發揮著重要作用。除了定理證明、數學應用題之外,還有一系列圍繞數學推理的QA基準。

近段時間相關資料集大量誕生,比如QuaRel、McTaco、Fermi等,但最新研究表明,最先進的數學推理系統可能存在推理的脆性,即模型依靠虛假訊號來達到看上去令人滿意的效能。

為了解決這一問題,在各個方面誕生了新基準,比如MATH,由具有挑戰性的競賽數學組成,以衡量模型在複雜情況下的問題解決能力。

除此之外,還有一些其他的數學任務,作者還專門彙總了表格,梳理了各個任務的相關資料集。

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

三大深度神經網路模型

接著,團隊梳理在數學推理任務中,主要使用的幾大深度神經網路模型。

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數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

而在現有資料集和基準的分析中,研究團隊看到了一些缺陷,包括對對低資源環境的關注有限、不充分的數字表示、不一致的推理能力。

最後,團隊從泛化和魯棒性、可信的推理、從反饋中學習、多模態數學推理等方面探討了未來的研究方向。

還整理了份AI數學閱讀清單

這篇關於AI數學的調查報告,由UCLA、聖母大學、華盛頓大學等機構的研究人員共同完成。

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

第一作者是來自UCLA的Pan Lu,目前正讀博四,受到KaiWei Chang、朱松純等教授指導,此前曾獲清華碩士學位。

共同作者還有同樣是UCLA的邱亮,今年畢業已是亞馬遜Alexa AI的應用科學家,曾受朱松純和Achuta Kadambi教授的指導,是上海交大校友。

他們還整理了份數學推理和人工智慧研究課題的閱讀清單,放在GitHub上。

一文看懂AI數學發展現狀,清華校友朱松純學生一作,還整理了份必備閱讀清單

本文為專欄作者授權創業邦發表,版權歸原作者所有。文章系作者個人觀點,不代表創業邦立場,轉載請聯絡原作者。如有任何疑問,請聯絡