AI能證明數(shù)學(xué)數(shù)據(jù)庫(kù)中82%的問題，新SOTA已達(dá)成，基于Transformer

明敏 2022-05-26 14:02:59 來源：量子位

明敏 發(fā)自 凹非寺

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

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

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

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

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

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

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

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

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

還是Transformer

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

大致可以分為三步：

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

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

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

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

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

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

Metamath的主庫(kù)是set.mm，包含基于ZFC集合論的約38000個(gè)證明。

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

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

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

MCTS譯為蒙特卡洛樹搜索，常用于解決博弈樹問題，它因?yàn)锳lphaGo所被人熟知。

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

本項(xiàng)研究采用的思路類似于此。

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

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

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

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

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

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

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

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

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

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

實(shí)驗(yàn)結(jié)果

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

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

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

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

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

比如在如下這道題中，它并沒有用最簡(jiǎn)便的辦法解出題目，研究人員表示這是因?yàn)樽⑨屩谐霈F(xiàn)了錯(cuò)誤。

One More Thing

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

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

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

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

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

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

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

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

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

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

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

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

論文地址：
https://arxiv.org/abs/2205.11491