又放大招 ?OpenAI 推出 GPT-f 數學推理證明模型:推理結果首次被數學家接受

2020/10/11 19:42:12 來源:大數據文摘微信公眾號 作者:牛婉楊 責編:騎士

今年 6 月,OpenAI 發布一款強大的文本生成模型 GPT-3,不少網友迅速上手用了起來,有人用它寫食譜、寫歌詞,甚至有人用它寫博客,愣是以假亂真登上了新聞平臺技術板塊熱榜第一。

前不久,OpenAI 再次放出大招。這次,研究人員發布了一篇論文《Generative Language Modeling for Automated Theorem Proving》,推出了一款用于自動定理證明 (ATP) 的 GPT-f 模型。GPT-f 基于 Transformer 語言模型,可以為 Metamath 形式化語言提供自動證明器和證明助手。

論文地址:

https://arxiv.org/pdf/2009.03393.pdf

GPT-f 有什么特別之處?

論文一作 Stanislas Polu 在推特上進行了介紹,他們在實驗中發現,GPT-f 比現有自動定理證明器還要優秀,可完成測試集中 56.22% 的證明,而現有的 SOTA 模型 MetaGen-IL 也只能證明 21.16% 的定理。

此外,GPT-f 還發現了新的簡短證明,已有 23 個簡短證明被收入 Metamath 函式庫中。這是深度學習模型的定理生成證明首次被數學家接受。

那么大家對于 GPT-f 是怎么看的呢?

網友普遍保持中立,大佬認為沒有特別之處

文摘菌想在推特上看看網友們的討論,沒想到 AI 界的一些大佬也發表了自己的看法。

Robust.AI、Geometric Intelligence 兩家 AI 公司的創始人,研究人工智能領域多年的科學家 Gary Marcus 認為,“就像 GPT-3 不是研究真正人類語言的正確方向一樣……,GPT-f 并不是達到真正人類水平 (更不用說超越人了)的數學定理證明的正確研究方向?!?/p>

他還稱,人們一直在誤用 GPT 來解決它不適合解決的問題,同樣的問題也不斷出現。

美國通用人工智能會議主席、奇點大學顧問、人工智能軟件公司 Novamente LLC 公司董事長   Ben Goertzel 也在推特發表了自己的看法,他認為,GPT-f 又是一個在不理解的情況下指導定理證明的古怪實驗……

他還專門寫了一篇文章來談論對于 GPT-f 的看法,發表在了自己的博客上。

博客地址:

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

Ben 還在博客中寫道,“從 ATP 領域正在進行的工作的總體背景來看,在我看來,GPT-f 不像 GPT-2 或 GPT-3 那樣邁出了一大步——但可以肯定的是,它在 ATP 方面是有意義的進展,與這一領域其他專家正在進行的大量研究進展相符(然而,這些專家因為沒有像 OpenAI 那樣的公關預算而不被媒體報道)。GPT-f 還有一個與其他 GPT 類似的核心缺點——它在理解數學這方面并不比 GPT-2 或 GPT-3 理解語言的能力更強?!?/p>

那網友們怎么看呢?

現階段網友們普遍是一種吃瓜的態度,并沒有對 GPT-f 大肆夸耀。大部分只是轉發了相關推文并陳述了論文中 GPT-f 實驗的成果。

也有一部分網友在論壇中發表了自己的疑問。

比如網友 @Jason Rute 就問到:什么才是有效的證明步驟?Jason Rute 曾經是一名數學家,后來成為了數據科學家,他對深度學習很感興趣。

GPT-f 將同時返回一個定理和替換,然后它們必須與目標統一。如果替換不統一,那么我確定它被標記為無效。然而,如果這個定理不在先前證明的定理列表中呢?GPT-f 是做什么的?

1)試著證明這個定理;

2)認為這是一個無效的證明步驟,還是將輸出限制在已知的定理上?

(我想會是第一條,但我還是想驗證一下。)

論文一作 Stanislas Polu 也在論壇對此進行了回復,并表示這是個好問題。

· 如果統一失敗,內核會拒絕驗證步驟,甚至在驗證樹搜索中也不會考慮它(不會添加到樹或隊列中,也不會由值函數賦值)?!?nbsp;如果該定理在數據庫中沒有被報告,那么該定理也將被拒絕。這就是說,我們正在試驗讓模型證明這些猜想,如果它們被價值函數認為有趣的話。在這種情況下,我們只需將定理本身添加為子目標(帶有一個特殊的標記,以確保一旦找到證據,我們就重新檢查不同的變量(DVs 是一種元數學技術,可以在您的思維中抽象出來,如果您不知道它們是如何工作的,可以稍后再訪問)),然后子目標會相應地被賦值并添加到隊列中。

針對這個問題,Jason Rute 在論文作者回復后還追加了提問,詳細討論可以看這里:https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/GPT-f.20paper.html#210087032 Jason Rute 還說,“在許多方面 GPT-f 類似于之前出現的其他定理證明,HOList/DeepMath, CoqGym/ASTTactic, TacticToe 等等。所有這些的共同之處在于它們把定理證明當作樹搜索。長期以來,我們所知道的是,采用智能啟發式可以避免樹 (和圖)搜索中的組合爆炸。AlphaGo 及其后繼者告訴我們的是,這些啟發式完全可以從例子中學習,也可以從引導和強化學習中學習。GPT-f 在這方面沒有什么不同。(關于 GPT-f 使用的特定樹搜索算法,我不打算說得太多,因為我不認為他們的方法比其他類似的論文優化很多。)” 此外,文摘菌也翻了一下知乎,只有一個相關問題,而且該問題下只有一個回答。由此可見,國內網友可能還不太知道 GPT-f,也可能由于發布時間并不長,大家對于 GPT-f 還處在比較懵的狀態。

如果你對 GPT-f 有更好的了解或看法,歡迎在評論區分享~

GPT-f 由自動證明器和證明助手組成

GPT-f 是由兩部分組成的,分別是自動證明器和證明助手。 自動證明器是為了尋求更簡短的證明,研究人員從 Metamath 的 set.mm 庫中采樣命題證明,并對比 GPT-f 模型找到的解與真值的長度,同時還驗證了簡短證明不依賴于額外的公理。

證明搜索包括維護一個證明樹,其中從根目標開始探索每個目標的多種策略。 OpenAI 利用在線證明助手,來幫助模型產生交互式的證明架構。下圖展示了 GPT-f 證明助理的界面:

Metamath 是一種用于存檔,驗證和研究數學證明的語言和計算機程序。研究人員使用 Metamath 作為正式環境,使用類似于 GPT-2 和 GPT-3 的僅解碼器的轉換器來創建具有各種預訓練數據集和不同大小的模型。他們最大的模型具有 36 層和 774m 可訓練參數。

各種模型大小和預訓練數據集的性能 說了這么多,那什么是自動定理證明呢。 百度百科中是這樣描述的:自動定理證明是人工智能研究領域中的一個非常重要的課題,其任務是對數學中提出的定理或猜想尋找一種證明或反證的方法。因此,智能系統不僅需要具有根據假設進行演繹的能力,而且也需要一定的判定技巧。 研究人員發現,學習證明定理與學習玩棋盤游戲之間有相似之處,因為它們都提供了自動確定成功的方法,并生成新的數據。因此,AlphaZero 在圍棋領域的成功表明,自動定理證明可能是神經網絡推理研究的一個富有成效的領域。

相關文章

關鍵詞:OpenAI,數學

軟媒旗下網站: IT之家 辣品 - 超值導購,優惠券 IT圈(Win10/WP8.1/Win7論壇) 最會買 - 返利返現優惠券 6655網址之家 Win10之家 Win8之家 Win7之家 Vista之家

軟媒旗下軟件: 魔方 旗魚瀏覽器(極速內核) 云日歷 酷點桌面 閃游瀏覽器(IE內核) Win7優化大師 Win8優化大師 Win10優化大師 軟媒手機APP應用

贵州快3开奖号码走势