本文轉自雷鋒網，如需轉載請至雷鋒網官網申請授權。

最近，GPT家族又添了一位新成員—GPT-f

提到GPT家族，首先想到了必然是今年大火的GPT-3，這款基于Transformer架構的語言模型，在文本生成方面的能力，已經可以達到以假亂真，欺騙人類的地步。

前不久，就有人利用GPT-3冒充專業人士在Reddit上回帖，還多次被頂上“高贊”，直到一周后才有網友發現，原來這些內容并非人類撰寫。

與GPT-3類似，最新推出的這款GPT-f同樣是基于Transformer語言模型，但不同的是，它目標是解決自動定理證明（ATP）的問題。

GPT家族的創始公司OpenAI認為，Transformer架構已經在自然語言處理、計算機視覺和語音識別等方面取得了長足的進步，相信它在相對未開發的推理任務領域中也具有足夠的潛力。

而他們在GPT-f的最新研究論文中已經證明了這一點。

論文地址：https://arxiv.org/pdf/2009.03393.pdf

GPT-f：用語言模型解決數學問題

據了解，自動定理證明是人工智能研究領域中的一個非常重要的課題，其任務是對數學中提出的定理或猜想尋找一種證明或反證的方法。因此，自動證明系統不僅需要具有根據假設進行演繹的能力，而且也需要一定的判定技巧。

而Transformer語言模型恰好具備這樣的能力，同時其生成能力還能解決現有研究的一個主要局限，即原始數學項（term）的生成。

GPT-f 可以看做是Transformer語言模型在數學推理領域的拓展，而它通過自動定理證明驗證了語言模型在這一方面的可行性。

研究人員Greg Brockman在Twitter發文稱，

GPT-f 已經發現32個形式定理證明，包括現有定理更簡單的證明方式，以及尚未確定的證明。這些證明已經被收錄到Metamath數據庫中。

Github地址：

https://github.com/metamath/set.mm/pull/1547

https://github.com/metamath/set.mm/pull/1710

其中，Metamath數據庫是目前最具全面，也最具權威性的形式數學社區。Metamath是一種微小的語言，它可以用抽象數學表達定理，并附有可以由計算機程序驗證的證明。

此次GPT-f的自動定理證明被收錄，是形式數學社區首次采納深度學習系統提供的證明。

值得一提的是，該研究論文一作Stanislas Polu還表示，GPT在自動定理證明方面，達到了現有研究的最佳SOTA.

我們在實驗中發現，GPT-f比現有自動定理證明器還要優秀，可完成測試集中56.22%的證明，而現有的SOTA模型MetaGen-IL也只能證明21.16%的定理。

除此之外，論文中顯示，GPT-f在自動定理證明領域還取得了以下新的發現：

• 生成式預訓練可以顯著提高模型性能，而相比于對網頁上的通用文本進行預訓練，對數學數據進行預訓練會帶來更好的性能。

• 模型大小與性能表現呈正相關，即使所采用的Metamath數據集相對較小。

• 研究發現，語言模型生成的語句上迭代地訓練一個值函數可以提高證明程序的性能，由此提出了一個持續自我改進的策略：基于證明器生成的證明不斷訓練。

• 利用Metamath環境測試，GPT-f模型證明了Transformer架構在形式推理方面的可行性。

接下來，我們來詳細看一下GPT-f 的工作原理

基于自動證明器和證明助理的模型

論文中顯示，研究人員使用了類似 GPT-2 和 GPT-3 的純解碼器Transformer，最大的模型有 36 層、7.74 億個可訓練參數。

基于該語言模型，GPT-f為 Metamath 形式化語言提供了自動證明器和證明助理（Proof Assistant）兩個部分。

自動證明器的核心在于證明搜索過程。證明搜索包含維護一個證明樹，它是從根目標開始探索每個目標的多種策略。而目標由累積對數概率（Logprob）的優先級進行擴展。

該研究采用 Metamath 作為形式環境。Metamath 的主庫叫做 set.mm，包含基于 ZFC 集合論的約 38000 個證明。

需要注意的是，執行證明搜索需要與Metamath模型緊密耦合。在這里，研究人員用Python創建了一個Metamath內核，內核包含一個修改過的LR(0)解析器，用于檢查模型生成的術語是否符合Metamath語法，以及實現Metamath替換，并以此來表示證明樹的目標和策略對象。

總的來說，這個證明搜索過程和與它綁定的Metamath形式驗證器共同構成了GPT-f自動驗證器。

實驗結果表明，盡管訓練數據集的大小有限，但模型大小對GPT-f性能依然有正向影響。從下圖來看，模型越大，訓練和基準測試時使用的計算越多。

隨著在樣本數據上迭代次數的增加，模型性能也在不斷增加，如下圖，160m和700m（Webmath）參數模型在迭代學習值函數數據生成和重新訓練過程中的性能表現：

另外，需要說明的是，研究人員向Metamath數學庫提供了23個定理的簡化證明，這些證明全部是由GPT-f自動驗證器生成的。為了發現更簡短的證明方式，研究人員從set.mm庫中采樣命題證明，并對比GPT-f模型找到的解與真值的長度，由此也驗證了簡短證明不依賴于額外定理。

在GPT-f中，在線證明助理可以輔助模型進行交互式證明構建。論文中，研究人員用它形式化了200多個定理和練習，結果發現模型的性能表現大幅提升。

證明助理可以自動生成大多數Metamath證明所需的各種簡單技術驗證步驟，它通過將現有定理調整到用戶所需的搜索庫，并建議使用定理。

即使推薦的定理存在錯誤，GPT-f模型通常也會選擇正確的定理，而錯誤的定理通常很容易被人類修正。

證明助手也已經在Metamath社區中應用。研究人員表示，他們其目的是希望幫助社區提高效率的同時，通過自動收集用戶反饋，反過來幫助他們提高模型的準確性。

語言模型解決邏輯問題，真的靠譜嗎？

對于這項研究成果，Twitter上引起了不少網友和大佬們的關注討論。其中也有部分人對GPT-f在數學定理方面的應用表示了質疑。

如一位網友表示，不要高估GPT-f，神經網絡是很好的模式發現者，但它也只是一個模式發現者，而不是算法的發現者。

還有一位AI軟件公司CEO，美國通用人工智能會議主席Ben Goertzel怎直接發文稱，GPT-f 是一個在不理解的情況下指導定理證明的奇怪實驗。

在他看來，與GPT的核心缺點一樣，GPT-f在理解數學方面并不比GPT-2或GPT-3的能力更強。”另外，就像GPT-3不是實現真正人類語言能力的正確研究方向一樣，GPT-f也不是實現真正人類(更不用超過人類)的數學定理證明的正確研究方向。

Ben Goertzel還專門撰寫了一篇博客表達自己的觀點。

博客地址：https://multiverseaccordingtoben.blogspot.com/2020/09/gpt-f-one-more-funky-experiment-in.html

不過，他也表示，從總體背景來看，GPT-f 在ATP方面應用是有意義的進展，這項研究與該領域其他專家正在進行的大量研究進展相符。

事實上，基于 Transformer架構的GPT-3模型雖然在文本生成方面具有強大性能，但其始終未通過圖靈測試，而且它在簡單的數學推理方面存在明顯的缺陷。

對于同樣基于Transformer模型的GPT-f也難免陷入這樣的質疑，即語言模型是真正理解了數學定理之間的邏輯關系，還是只是這一模型只是簡單理解了語意？