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

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

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

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

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

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

而他們?cè)贕PT-f的最新研究論文中已經(jīng)證明了這一點(diǎn)。

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

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

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

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

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

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

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

Github地址：

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

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

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

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

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

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

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

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

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

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

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

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

基于自動(dòng)證明器和證明助理的模型

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

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

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

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

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

總的來(lái)說(shuō)，這個(gè)證明搜索過(guò)程和與它綁定的Metamath形式驗(yàn)證器共同構(gòu)成了GPT-f自動(dòng)驗(yàn)證器。

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

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

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

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

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

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

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

語(yǔ)言模型解決邏輯問(wèn)題，真的靠譜嗎？

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

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

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

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

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

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

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

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

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