不得不說，科學家們最近都在癡迷給 AI 補數(shù)學課了。這不，臉書團隊也來湊熱鬧，提出了一種新模型，能完全自動化論證定理，并顯著優(yōu)于 SOTA。
要知道，隨著數(shù)學定理愈加復雜，之后再僅憑人力來論證定理只會變得更加困難。因此，用計算機論證數(shù)學定理已經(jīng)成為一個研究焦點。
此前 OpenAI 也提出過專攻這一方向的模型 GPT-f，它能論證 Metamath 中 56% 的問題。而這次提出的最新方法，能將這一數(shù)字提升到 82.6%。
與此同時，研究人員表示該方法使用的時間還更短，與 GPT-f 相比可以將計算消耗縮減到原本的十分之一。難道說這一次 AI 大戰(zhàn)數(shù)學，是要成功了？
還是 Transformer
本文提出的方法為一種基于 Transformer 的在線訓練程序。大致可以分為三步：
第一、在數(shù)學證明庫中預訓練；
第二、在有監(jiān)督數(shù)據(jù)集上微調(diào)策略模型；
第三、在線訓練策略模型和判斷模型。
具體來看是利用一種搜索算法，讓模型在已有的數(shù)學證明庫中學習，然后去推廣證明更多的問題。其中數(shù)學證明庫包括 3 種，分別是 Metamath、Lean 和自研的一種證明環(huán)境。這些證明庫簡單來說，就是把普通數(shù)學語言轉(zhuǎn)換成近似于編程語言的形式。
Metamath 的主庫是 set.mm，包含基于 ZFC 集合論的約 38000 個證明。Lean 更為人熟知的，是微軟那個可以參加 IMO 賽事的 AI 算法。Lean 庫就是為了教會同名算法所有的本科數(shù)學知識，并讓它學會證明這些定理。
這項研究的主要目標，是為了構(gòu)建一個證明器，讓它可以自動生成一系列合適的策略去論證問題。為此，研究人員提出了一個基于 MCTS 的非平衡超圖證明搜索算法。
MCTS 譯為蒙特卡洛樹搜索，常用于解決博弈樹問題，它因為 AlphaGo 所被人熟知。它的運行過程，就是通過在搜索空間中隨機抽樣來找尋有希望的動作，然后根據(jù)這個動作來擴展搜索樹。
本項研究采用的思路類似于此。搜索證明過程從目標 g 開始，向下搜索方法，逐步發(fā)展成一個超圖（Hypergraph）。當出現(xiàn)一個分支下出現(xiàn)空集時，就意味著找到了一個最優(yōu)證明。最后，在反向傳播過程中，記下超樹的節(jié)點值和總操作次數(shù)。
在這個環(huán)節(jié)中，研究人員假設了一個策略模型和一個判斷模型。策略模型允許判斷模型進行抽樣，判斷模型可以評估當前策略找到證明方法的能力。整個搜索算法，就以如上兩個模型作為參照。而這兩個模型都是 Transformer 模型，且權值共享。
接下來，就到了在線訓練的階段。這個過程中，控制器會將語句發(fā)送給異步 HTPS 驗證，并收集訓練和證明數(shù)據(jù)。然后驗證器會將訓練樣本發(fā)送給分布式訓練器，并定期同步其模型副本。
實驗結(jié)果
在測試環(huán)節(jié)，研究人員將 HTPS 與 GPT-f 進行了比較。后者是 OpenAI 此前提出的數(shù)學定理推理模型，同樣基于 Transformer。結(jié)果表明，在線訓練后的模型可以證明 Metamath 中 82% 的問題，遠超 GPT-f 此前 56.5% 的記錄。
在 Lean 庫中，這一模型可以證明其中 43% 的定理，比 SOTA 提高了 38%，以下是該模型證明出的 IMO 試題。
不過目前它還不是十全十美。比如在如下這道題中，它并沒有用最簡便的辦法解出題目，研究人員表示這是因為注釋中出現(xiàn)了錯誤。
One More Thing
用計算機論證數(shù)學問題，四色定理的證明便是最為人熟知的例子之一。四色定理是近代數(shù)學三大難題之一，它提出“任何一張地圖只用四種顏色就能使具有共同邊界的國家，著上不同的顏色”。
由于這一定理的論證需要大量計算，在它被提出后 100 年內(nèi)，都沒有人能完全論證。直到 1976 年，在美國伊利諾斯大學兩臺計算機上，經(jīng)過 1200 小時、100 億次判斷后，終于可以論證任何一張地圖都只需要 4 種顏色來標記，由此也轟動了整個數(shù)學界。
加之隨著數(shù)學問題愈加復雜，用人力來檢驗定理是否正確也變得更加困難。近來，AI 界也把目光逐步聚焦在數(shù)學問題上。
2020 年，OpenAI 推出數(shù)學定理推理模型 GPT-f，可用于自動定理證明。這一方法可完成測試集中 56.5% 的證明，超過當時 SOTA 模型 MetaGen-IL30% 以上。
同年，微軟也發(fā)布了可以做出 IMO 試題的 Lean，這意味著 AI 能做出沒見過的題目了。去年，OpenAI 給 GPT-3 加上驗證器后，做數(shù)學題效果明顯好于此前微調(diào)的辦法，可以達到小學生 90% 的水平。
今年 1 月，來自 MIT + 哈佛 + 哥倫比亞大學 + 滑鐵盧大學的一項聯(lián)合研究表明，他們提出的模型可以做高數(shù)了?？傊?，科學家們正在努力讓 AI 這個偏科生變得文理雙全。
論文地址：
https://arxiv.org/abs/2205.11491
廣告聲明：文內(nèi)含有的對外跳轉(zhuǎn)鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節(jié)省甄選時間，結(jié)果僅供參考，IT之家所有文章均包含本聲明。