不得不說，科學(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é)證明庫中預(yù)訓(xùn)練；
第二、在有監(jiān)督數(shù)據(jù)集上微調(diào)策略模型；
第三、在線訓(xùn)練策略模型和判斷模型。
具體來看是利用一種搜索算法，讓模型在已有的數(shù)學(xué)證明庫中學(xué)習(xí)，然后去推廣證明更多的問題。其中數(shù)學(xué)證明庫包括 3 種，分別是 Metamath、Lean 和自研的一種證明環(huán)境。這些證明庫簡(jiǎn)單來說，就是把普通數(shù)學(xué)語言轉(zhuǎn)換成近似于編程語言的形式。
Metamath 的主庫是 set.mm，包含基于 ZFC 集合論的約 38000 個(gè)證明。Lean 更為人熟知的，是微軟那個(gè)可以參加 IMO 賽事的 AI 算法。Lean 庫就是為了教會(huì)同名算法所有的本科數(shù)學(xué)知識(shí)，并讓它學(xué)會(huì)證明這些定理。
這項(xiàng)研究的主要目標(biāo)，是為了構(gòu)建一個(gè)證明器，讓它可以自動(dòng)生成一系列合適的策略去論證問題。為此，研究人員提出了一個(gè)基于 MCTS 的非平衡超圖證明搜索算法。
MCTS 譯為蒙特卡洛樹搜索，常用于解決博弈樹問題，它因?yàn)?AlphaGo 所被人熟知。它的運(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 庫中，這一模型可以證明其中 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
廣告聲明：文內(nèi)含有的對(duì)外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時(shí)間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。