本文轉(zhuǎn)自雷鋒網(wǎng)，如需轉(zhuǎn)載請至雷鋒網(wǎng)官網(wǎng)申請授權(quán)。

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

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

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

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

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

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

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

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

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

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

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

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

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

Github地址：

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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