不得不說，科學家們最近都在癡迷給AI補數學課了。

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

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

因此，用計算機論證數學定理已經成為一個研究焦點。

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

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

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

難道說這一次AI大戰數學，是要成功了?

還是Transformer

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

大致可以分為三步：

第一、在數學證明庫中預訓練;

第二、在有監督數據集上微調策略模型;

第三、在線訓練策略模型和判斷模型。

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

其中數學證明庫包括3種，分別是Metamath、Lean和自研的一種證明環境。

這些證明庫簡單來說，就是把普通數學語言轉換成近似于編程語言的形式。

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

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

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

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

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

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

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

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

當出現一個分支下出現空集時，就意味著找到了一個最優證明。

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

在這個環節中，研究人員假設了一個策略模型和一個判斷模型。

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

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

而這兩個模型都是Transformer模型，且權值共享。

接下來，就到了在線訓練的階段。

這個過程中，控制器會將語句發送給異步HTPS驗證，并收集訓練和證明數據。

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

實驗結果

在測試環節，研究人員將HTPS與GPT-f進行了比較。

后者是OpenAI此前提出的數學定理推理模型，同樣基于Transformer。

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

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

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

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

One More Thing

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

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

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

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

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

近來，AI界也把目光逐步聚焦在數學問題上。

2020年，OpenAI推出數學定理推理模型GPT-f，可用于自動定理證明。

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

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

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

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

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