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

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

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

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

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

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

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

1

GPT-f：用語言模型解決數(shù)學問題

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

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

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

研究人員Greg Brockman在Twitter發(fā)文稱，

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

Github地址：

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

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

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

此次GPT-f的自動定理證明被收錄，是形式數(shù)學社區(qū)首次采納深度學習系統(tǒng)提供的證明。

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

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

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

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

• 模型大小與性能表現(xiàn)呈正相關，即使所采用的Metamath數(shù)據(jù)集相對較小。

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

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

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

2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3

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

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

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

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

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

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

博客地址：

https://multiverseaccordingtoben.blogspot.com/2020/09/gpt-f-one-more-funky-experiment-in.html

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

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

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

總結

以上是生活随笔為你收集整理的GPT家族又壮大了！OpenAI首次推出数学定理推理模型GPT-f的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。