作者 | 八寶粥
出品 | CSDN(ID:CSDNnews)
OpenAI 大招頻出，染指數學江湖
日前，OpenAI 研究者Stanislas Polu和Ilya Sutskever在社交媒體發布消息，宣布在預印本發布文章，展示了一個基於Transformer 的自動定理證明模型。文章表示，團隊在 Metamath 庫上取得了新的進展，通過將深度學習和形式系統相結合能帶來更好的效果。
論文兩位作者在社交網絡分享發布新模型的喜悅
團隊表示，GPT-f 可以自動證明 Metamath 當中23個定理。橫向對比上，GPT-f 最佳模型實現 Metamath 56.22% 的保留測試集，而目前最先進的 MetaGen-IL 只有 21.16% 的證明能力。
文章還給出了數據集 set.mm 和證明助手的一個 demo：
「自動定理證明」對於飽受數學困擾的同學來說簡直就是大殺器，比擬「步步高點讀機」，筆者不禁想到自己中學數學做題時自信地刷刷寫下「證明」二字和面對高等數學撓頭時候的「這也能證？」，「要是機器能幫我證明就好了」。
實際上，在數學界，確實有很多問題需要機器來幫忙。但是 GPT-f 真的是數學界的 AlphaGo 嗎？數學家也要望機器興嘆了嗎？似乎也並不是這樣。
數學天才也需要機器
前段時間獲得諾貝爾物理學獎的科學家羅傑·彭羅斯，他在數學方面有一個很有趣的貢獻，就是彭羅斯密鋪，1976年，他提出採用兩種不同的菱形進行密鋪，實現對平面的全覆蓋。而放眼三維，早在十七世紀，德國天文學家克卜勒就對三維歐式空間當中容納球的方式進行研究，發現三維球堆積的最大密度為：
而這個定理直到 1998 年由機器來輔助證明的。就是那種你明明知道卻證不出來的感覺。直到 2014年才由黑爾斯的 FlysPeck 項目完成了形式化證明。
說到推理，就肯定會提到計算機界的鼻祖圖靈大佬。二戰期間，德軍採用恩格瑪機器加密，給盟軍的情報獲取造成了極大的打擊。為了破解密碼，盟軍招募大量人力組建團隊，對密碼機進行研究，後發明「圖靈炸彈（Turing Bombe）」，雖然對恩格瑪的破解是波蘭人，但是毫無疑問圖靈是恩格瑪破解的最大功臣。此後「圖靈炸彈」在布萊切利繼續發揮作用，給密碼破譯工作加速。圖靈以他的名字命名的抽象計算模型——圖靈機也是通過機器來模擬人類計算的過程。後來成為計算機歷史上具有濃墨重彩的一頁。
機器輔助證明已經成為了單獨的數學研究方向，而人工智慧更多地研究的是讓機器自主去發現和探索數學定理。就好比 AlphaGo 或者 AutoML 一樣，機器可以自己去探索和研究。人們期待計算機能給人帶來更多驚喜。GPT 這種驚人能力讓人想到了當年的印度天才拉馬努金，他從來沒有經歷專業的數學訓練。憑藉自己的天賦，用自己的符號和方式證明了很多已經存在的定理。著名的數學家哈代發現了他的天賦，將其帶往英國，後發現了拉馬努金猜想、整數分割和θ函數等著名的數學定理。如果機器真的都能變成一個個拉馬努金，那麼不久的將來在數學甚至信息學界就會發生翻天覆地的變化。
保持慎重,保持樂觀
對於 GPT 模型，很多人並不樂觀，像此前一直對 GPT 開炮的 Gary Marcus, 在社交媒體上一直置頂自己在《MIT 科技評論》上面批判 GPT 的文章，文中批評了 GPT 在面對數學等基礎學科上的無知和無能，稱其根本一文不值，只是一個了解上下文的機器而已。此次更是快速反應, 稱 GPT-f 也一樣達不到人類的水平，更不用說打敗人類了。
Robust.AI聯合創始人一直都不喜歡GPT，此次依然直接吐槽
這裡我們也表示樂觀，如果 GPT-f 真的能夠實現更大的突破，那麼不管是數學界還是在 AI 界，都是拉馬努金在世一樣的好事，畢竟這位印度天才如果不是在異國他鄉身體虛弱，說不定還能創造更多的數學奇蹟。如果 GPT-f 不能跟真人一樣, 說不定還會有 GPT-G, GPT-X, GPT-Y 呢～
注: Metamath是用來發展嚴格形式化數學定義及證明的一款語言，亦指用來驗證該語言的證明驗證器，以及存有邏輯、集合論、數論、群論、代數、數學分析、拓撲學、希爾伯特空間及量子邏輯等領域中數萬條已證明定理且仍不斷在增加中的資料庫。(來源: 維基百科)
論文連結:https://arxiv.org/abs/2009.03393