不得不說，科學(xué)家們最近都在癡迷給AI補數(shù)學(xué)課了。

這不，臉書團隊也來湊熱鬧，提出了一種新模型，能完全自動化論證定理，并顯著優(yōu)于SOTA。

要知道，隨著數(shù)學(xué)定理愈加復(fù)雜，之后再僅憑人力來論證定理只會變得更加困難。

因此，用計算機論證數(shù)學(xué)定理已經(jīng)成為一個研究焦點。

此前OpenAI也提出過專攻這一方向的模型GPT-f，它能論證Metamath中56%的問題。

而這次提出的最新方法，能將這一數(shù)字提升到82.6%。

與此同時，研究人員表示該方法使用的時間還更短，與GPT-f相比可以將計算消耗縮減到原本的十分之一。

難道說這一次AI大戰(zhàn)數(shù)學(xué)，是要成功了?

還是Transformer

本文提出的方法為一種基于Transformer的在線訓(xùn)練程序。

大致可以分為三步：

第一、在數(shù)學(xué)證明庫中預(yù)訓(xùn)練;

第二、在有監(jiān)督數(shù)據(jù)集上微調(diào)策略模型;

第三、在線訓(xùn)練策略模型和判斷模型。

具體來看是利用一種搜索算法，讓模型在已有的數(shù)學(xué)證明庫中學(xué)習(xí)，然后去推廣證明更多的問題。

其中數(shù)學(xué)證明庫包括3種，分別是Metamath、Lean和自研的一種證明環(huán)境。

這些證明庫簡單來說，就是把普通數(shù)學(xué)語言轉(zhuǎn)換成近似于編程語言的形式。

Metamath的主庫是set.mm，包含基于ZFC集合論的約38000個證明。

Lean更為人熟知的，是微軟那個可以參加IMO賽事的AI算法。Lean庫就是為了教會同名算法所有的本科數(shù)學(xué)知識，并讓它學(xué)會證明這些定理。

這項研究的主要目標，是為了構(gòu)建一個證明器，讓它可以自動生成一系列合適的策略去論證問題。

為此，研究人員提出了一個基于MCTS的非平衡超圖證明搜索算法。

MCTS譯為蒙特卡洛樹搜索，常用于解決博弈樹問題，它因為AlphaGo所被人熟知。

它的運行過程，就是通過在搜索空間中隨機抽樣來找尋有希望的動作，然后根據(jù)這個動作來擴展搜索樹。

本項研究采用的思路類似于此。

搜索證明過程從目標g開始，向下搜索方法，逐步發(fā)展成一個超圖(Hypergraph)。

當(dāng)出現(xiàn)一個分支下出現(xiàn)空集時，就意味著找到了一個最優(yōu)證明。

最后，在反向傳播過程中，記下超樹的節(jié)點值和總操作次數(shù)。

在這個環(huán)節(jié)中，研究人員假設(shè)了一個策略模型和一個判斷模型。

策略模型允許判斷模型進行抽樣，判斷模型可以評估當(dāng)前策略找到證明方法的能力。

整個搜索算法，就以如上兩個模型作為參照。

而這兩個模型都是Transformer模型，且權(quán)值共享。

接下來，就到了在線訓(xùn)練的階段。

這個過程中，控制器會將語句發(fā)送給異步HTPS驗證，并收集訓(xùn)練和證明數(shù)據(jù)。

然后驗證器會將訓(xùn)練樣本發(fā)送給分布式訓(xùn)練器，并定期同步其模型副本。

實驗結(jié)果

在測試環(huán)節(jié)，研究人員將HTPS與GPT-f進行了比較。

后者是OpenAI此前提出的數(shù)學(xué)定理推理模型，同樣基于Transformer。

結(jié)果表明，在線訓(xùn)練后的模型可以證明Metamath中82%的問題，遠超GPT-f此前56.5%的記錄。

在Lean庫中，這一模型可以證明其中43%的定理，比SOTA提高了38%，以下是該模型證明出的IMO試題。

不過目前它還不是十全十美。

比如在如下這道題中，它并沒有用最簡便的辦法解出題目，研究人員表示這是因為注釋中出現(xiàn)了錯誤。

One More Thing

用計算機論證數(shù)學(xué)問題，四色定理的證明便是最為人熟知的例子之一。

四色定理是近代數(shù)學(xué)三大難題之一，它提出“任何一張地圖只用四種顏色就能使具有共同邊界的國家，著上不同的顏色”。

由于這一定理的論證需要大量計算，在它被提出后100年內(nèi)，都沒有人能完全論證。

直到1976年，在美國伊利諾斯大學(xué)兩臺計算機上，經(jīng)過1200小時、100億次判斷后，終于可以論證任何一張地圖都只需要4種顏色來標記，由此也轟動了整個數(shù)學(xué)界。

加之隨著數(shù)學(xué)問題愈加復(fù)雜，用人力來檢驗定理是否正確也變得更加困難。

近來，AI界也把目光逐步聚焦在數(shù)學(xué)問題上。

2020年，OpenAI推出數(shù)學(xué)定理推理模型GPT-f，可用于自動定理證明。

這一方法可完成測試集中56.5%的證明，超過當(dāng)時SOTA模型MetaGen-IL30%以上。

同年，微軟也發(fā)布了可以做出IMO試題的Lean，這意味著AI能做出沒見過的題目了。

去年，OpenAI給GPT-3加上驗證器后，做數(shù)學(xué)題效果明顯好于此前微調(diào)的辦法，可以達到小學(xué)生90%的水平。

今年1月，來自MIT+哈佛+哥倫比亞大學(xué)+滑鐵盧大學(xué)的一項聯(lián)合研究表明，他們提出的模型可以做高數(shù)了。

總之，科學(xué)家們正在努力讓AI這個偏科生變得文理雙全。