世界本來(lái)已經(jīng)很卷，有了 AI 加入之后，卷上加卷……

>>>>

太卷了！

在國(guó)內(nèi)歡度春節(jié)之時(shí)，DeepMind 與 OpenAI 兩個(gè)知名 AI 研究機(jī)構(gòu)分別發(fā)布重要研究成果：DeepMind 發(fā)布了基于 Transformer 模型的 AlphaCode，可以編寫(xiě)與人類(lèi)相媲美的計(jì)算機(jī)程序；同時(shí)，OpenAI 開(kāi)發(fā)的神經(jīng)定理證明器成功解出了兩道國(guó)際奧數(shù)題。

有沒(méi)有覺(jué)得 AI 攻克的這兩個(gè)領(lǐng)域很熟悉？沒(méi)錯(cuò)，就在 2021 年，OpenAI 發(fā)布了 AI 代碼補(bǔ)全工具 GitHub Copilot ，并公布了背后的技術(shù) CodeX。同樣，在去年下半年，DeepMind 也公布了他們解決數(shù)學(xué)難題的 AI 研究成果，并登上了 Nature。

雖然兩家研究機(jī)構(gòu)的新成果為 AI 解決老問(wèn)題提供了新思路，但也不得不讓網(wǎng)友感嘆，AI 領(lǐng)域太卷了！

來(lái)源：網(wǎng)友微博截圖

擊敗 46% 參賽者的 AlphaCode

在最近的一篇論文中，DeepMind 的研究者介紹了 AlphaCode。AlphaCode 使用基于 Transformer 的語(yǔ)言模型實(shí)現(xiàn)大規(guī)模的代碼生成，并且將其編寫(xiě)為程序。

論文連接：https://storage.googleapis.com/deepmind-media/AlphaCode/competition_level_code_generation_with_alphacode.pdf

研究者將 AlphaCode 放在 Codeforces 挑戰(zhàn)中進(jìn)行了測(cè)試，Codeforces 是一個(gè)具有競(jìng)爭(zhēng)力的編程平臺(tái)，它類(lèi)似于國(guó)際象棋中使用的 Elo 評(píng)級(jí)系統(tǒng)，每周分享編程挑戰(zhàn)和問(wèn)題排名。不同于編程人員在打造商業(yè)應(yīng)用程序時(shí)可能面臨的任務(wù)，Codeforces 的挑戰(zhàn)更加獨(dú)立，需要對(duì)計(jì)算機(jī)科學(xué)中的算法和理論概念有更廣泛的了解，一般是結(jié)合邏輯、數(shù)學(xué)和編碼專(zhuān)業(yè)知識(shí)的非常專(zhuān)業(yè)的難題。

AlphaCode 針對(duì) Codeforces 網(wǎng)站上 5000 名用戶解決的 10 項(xiàng)挑戰(zhàn)進(jìn)行了測(cè)試，總體排名位于前 54.3%，也就是說(shuō)它擊敗了 46% 的參賽者 。DeepMind 估計(jì)，AlphaCode 系統(tǒng)的 Codeforces Elo 為 1238，使其過(guò)去六個(gè)月內(nèi)在該網(wǎng)站上競(jìng)爭(zhēng)的用戶中排名前 28%。

舉個(gè)例子，在測(cè)試 AlphaCode 的一項(xiàng)挑戰(zhàn)中，試題要求參賽者找到一種方法，使用一組有限的輸入將一個(gè)隨機(jī)、重復(fù)的 s 和 t 字母字符串轉(zhuǎn)換為另一個(gè)相同字母的字符串。例如，競(jìng)爭(zhēng)對(duì)手不能只輸入新字母，而必須使用「backspace」命令刪除原始字符串中的幾個(gè)字母。對(duì)于 AlphaCode 來(lái)說(shuō)，這只是中等難度的挑戰(zhàn)：

其中十個(gè)挑戰(zhàn)以與人類(lèi)完全相同的格式輸入 AlphaCode。然后，AlphaCode 生成大量可能的答案，并通過(guò)運(yùn)行代碼和檢查輸出來(lái)篩選這些答案，就像人類(lèi)競(jìng)爭(zhēng)對(duì)手一樣。AlphaCode 論文的聯(lián)合負(fù)責(zé)人 Yujia Li 和 David Choi 表示：「整個(gè)過(guò)程是自動(dòng)的，無(wú)需人工選擇最佳樣本?！?/p>

要想在 Codeforces 的挑戰(zhàn)中脫穎而出，原本不是一件容易的事。AlphaCode 項(xiàng)目開(kāi)展于兩年多前，隨著大規(guī)模 Transformer 模型的進(jìn)步與大規(guī)模采樣、濾波技術(shù)的結(jié)合，DeepMind 的研究者已經(jīng)在 AI 能夠解決的問(wèn)題數(shù)量上取得了重大進(jìn)展。

受到疫情的影響，項(xiàng)目的大部分工作都是在家完成的。

研究者在選定的公共 GitHub 代碼上預(yù)訓(xùn)練該模型，并在相對(duì)較小的競(jìng)賽編程數(shù)據(jù)集上對(duì)其進(jìn)行微調(diào)。在評(píng)估期間，研究者為每個(gè)問(wèn)題創(chuàng)建了大量的 C++ 和 Python 程序，且數(shù)量級(jí)比以前的工作要大。然后對(duì)這些解決方案進(jìn)行篩選、聚類(lèi)和重新排序，將這些解決方案分配到一個(gè)由 10 個(gè)候選程序組成的小集合中，并提交給外部評(píng)估。這個(gè)自動(dòng)化系統(tǒng)取代了競(jìng)爭(zhēng)對(duì)手的調(diào)試、編譯、通過(guò)測(cè)試和最終提交的反復(fù)試驗(yàn)過(guò)程。

總體來(lái)說(shuō)，AlphaCode 的排名在競(jìng)爭(zhēng)對(duì)手中大致相當(dāng)于中位數(shù)。雖然遠(yuǎn)遠(yuǎn)沒(méi)能贏得比賽，但這個(gè)結(jié)果代表了人工智能解決問(wèn)題能力的實(shí)質(zhì)性飛躍。這一進(jìn)步證明了深度學(xué)習(xí)模型在需要批判性思維的任務(wù)中的潛力。DeepMind 指出，AlphaCode 目前的技能組合目前僅適用于競(jìng)賽性質(zhì)的編程領(lǐng)域，但它的能力為創(chuàng)建未來(lái)工具打開(kāi)了新的大門(mén)，這些工具使編程變得更加容易，并且有朝一日完全自動(dòng)化。

許多其他公司正在開(kāi)發(fā)類(lèi)似的應(yīng)用程序。對(duì)于終端的用戶來(lái)說(shuō)，這些系統(tǒng)就像 Gmail 的 Smart Compose 功能一樣工作，提供一些關(guān)于你正在編寫(xiě)的任何內(nèi)容的建議。

近年來(lái)，AI 編程系統(tǒng)的開(kāi)發(fā)取得了很大進(jìn)展，但這些系統(tǒng)還遠(yuǎn)未準(zhǔn)備好接管人類(lèi)程序員的工作。他們生成的代碼通常有問(wèn)題，而且由于系統(tǒng)通常是在公共代碼庫(kù)上進(jìn)行訓(xùn)練的，所以有時(shí)會(huì)復(fù)制受版權(quán)保護(hù)的材料。

在一項(xiàng)關(guān)于 GitHub Copilot AI 編程工具的研究中，研究人員發(fā)現(xiàn)其輸出的代碼約有 40% 包含安全漏洞。安全分析師甚至建議，不良行為者可以故意編寫(xiě)代碼并與隱藏的后門(mén)（backdoor）在線共享代碼，然后這些代碼可能被用來(lái)訓(xùn)練 AI 程序，將這些錯(cuò)誤插入到未來(lái)的程序中。

像這樣的挑戰(zhàn)意味著 AI 編程系統(tǒng)可能會(huì)慢慢融入程序員的工作中——換句話說(shuō)，他們要進(jìn)行學(xué)徒訓(xùn)練，從助理開(kāi)始做起，在被信任能夠自主執(zhí)行工作之前，AI 給出的建議都要受到懷疑。

目前，DeepMind 已在 GitHub 上發(fā)布了競(jìng)賽級(jí)編程問(wèn)題和解決方案的數(shù)據(jù)集，其中也包括廣泛的測(cè)試的數(shù)據(jù)，以確保通過(guò)這些測(cè)試的程序是正確的，這是目前數(shù)據(jù)集所缺乏的一個(gè)關(guān)鍵特性。DeepMind 希望這個(gè)基準(zhǔn)能夠推動(dòng)在解決問(wèn)題和代碼生成方面的進(jìn)一步創(chuàng)新。

GitHub 項(xiàng)目地址：https://github.com/deepmind/code_contests

挑戰(zhàn)奧數(shù)題的神經(jīng)定理證明器

在學(xué)科競(jìng)賽領(lǐng)域，國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）是非常有名的一個(gè)，我們熟悉的很多數(shù)學(xué)大神（如韋東奕）都在這一競(jìng)賽中取得了驕人的成績(jī)。

2021 年，這項(xiàng)比賽迎來(lái)了一個(gè)微小的變化：微軟研發(fā)多年的數(shù)學(xué) AI——Lean 也加入了競(jìng)爭(zhēng)，和人類(lèi)選手一決高下。據(jù)悉，Lean 是微軟研究院在 2013 年推出的計(jì)算機(jī)定理證明器：數(shù)學(xué)家可以把數(shù)學(xué)公式轉(zhuǎn)換成代碼，再輸入到 Lean 中，讓程序來(lái)驗(yàn)證定理是否正確。

由于 Lean 劍指金牌，研究人員一直在對(duì)其進(jìn)行不停的打磨，其中也包括被微軟收購(gòu)了的 OpenAI。剛剛，OpenAI 發(fā)文表示，他們已經(jīng)為 Lean 創(chuàng)建了一個(gè)神經(jīng)定理證明器，用于解決各種具有挑戰(zhàn)性的高中奧林匹克問(wèn)題，包括兩個(gè)改編自 IMO 的問(wèn)題和來(lái)自 AMC12、AIME 競(jìng)賽的若干問(wèn)題。

該證明器使用一個(gè)語(yǔ)言模型來(lái)尋找形式化命題（formal statement）的證明。每次發(fā)現(xiàn)一個(gè)新的證明，研究者就把它作為新的訓(xùn)練數(shù)據(jù)，這改善了神經(jīng)網(wǎng)絡(luò)，使它能夠在迭代中找到越來(lái)越難的命題的解決方案。

該證明器在 miniF2F 基準(zhǔn)測(cè)試中實(shí)現(xiàn)了 SOTA（41.2% vs 29.3%）水平，miniF2F 包含一組具有挑戰(zhàn)性的高中奧林匹克問(wèn)題。

研究者將他們的方法稱(chēng)為 statement curriculum learning，該方法包括手動(dòng)收集的一組不同難度級(jí)別的命題（無(wú)需證明），其中最難的命題類(lèi)似于目標(biāo)基準(zhǔn)。最初，他們的神經(jīng)證明器很弱，只能證明其中的幾個(gè)。因此，他們迭代地搜索新的證明，并在新發(fā)現(xiàn)的證明上重新訓(xùn)練他們的神經(jīng)網(wǎng)絡(luò)。經(jīng)過(guò) 8 次迭代，他們的證明器在 miniF2F 上取得了出色的成績(jī)。

形式化數(shù)學(xué)（formal mathematics）是一個(gè)令人興奮的研究領(lǐng)域，因?yàn)?#xff1a;1）它很豐富，可以讓你證明需要推理、創(chuàng)造力和洞察力的任意定理；2）它與游戲相似，也有一種自動(dòng)化的方法來(lái)確定一個(gè)證明是否成立（即由形式系統(tǒng)驗(yàn)證）。如下圖中的例子所示，證明一個(gè)形式化的命題需要生成一系列的證明步驟，每個(gè)證明步驟都包含對(duì)策略（ tactic）的調(diào)用。

形式化系統(tǒng)接受的 artifact 是低級(jí)的（就像匯編代碼），人類(lèi)很難產(chǎn)生。策略是從更高層次的指令生成這種 artifact 的搜索過(guò)程，以輔助形式化。

這些策略以數(shù)學(xué)術(shù)語(yǔ)作為參數(shù)，每次策略調(diào)用都會(huì)將當(dāng)前要證明的命題轉(zhuǎn)換為更容易證明的命題，直到?jīng)]有任何東西需要證明。

研究者觀察到，生成策略參數(shù)所需的原始數(shù)學(xué)術(shù)語(yǔ)的能力出現(xiàn)在了他們的訓(xùn)練過(guò)程中，這是離開(kāi)神經(jīng)語(yǔ)言模型所無(wú)法完成的。下面的證明就是它的一個(gè)例子：證明步驟「use n + 1」（完全由模型生成）提出使用「n + 1」作為解決方案，剩下的形式證明依賴(lài)于「ring _ exp」策略來(lái)驗(yàn)證它確實(shí)有效。

研究者還觀察到，他們的模型和搜索過(guò)程能夠產(chǎn)生鏈接多個(gè)重要推理步驟的證明。在下面的證明中，模型首先使用了引出存在性命題（existential statement） (? (x : ?), f x ≠ a * x + b) 的換質(zhì)換位律（contraposition）。然后，它使用 use (0 : ?) 為它生成一個(gè) witness，并通過(guò)利用 norm _ num 策略來(lái)完成證明。

該模型經(jīng)過(guò) statement curriculum learning 的訓(xùn)練，能夠解決培訓(xùn)教材以及 AMC12 和 AIME 中的各種問(wèn)題，以及改編自 IMO 的兩個(gè)問(wèn)題。下面是三個(gè)有關(guān)的例子。

形式數(shù)學(xué)涉及兩個(gè)主要的挑戰(zhàn)，使得單純的強(qiáng)化學(xué)習(xí)應(yīng)用不太可能成功：

1. 無(wú)限的動(dòng)作空間：形式數(shù)學(xué)不僅有超大的搜索空間（比如像圍棋），還有無(wú)限的動(dòng)作空間。在搜索證明的每個(gè)步驟，模型的選擇范圍不是一組行為良好的有限動(dòng)作，而是一組復(fù)雜且無(wú)限的策略，涉及必須生成的外生數(shù)學(xué)術(shù)語(yǔ)（例如，生成用作 witness 的數(shù)學(xué)命題)。

2. 缺乏自博弈（self-play）：與兩人游戲相反，證明器不是與對(duì)手對(duì)抗，而是與一系列需要證明的命題對(duì)抗。當(dāng)面對(duì)一個(gè)過(guò)于困難的命題時(shí)，沒(méi)有明顯的重構(gòu)可以讓證明器首先生成更容易處理的中間語(yǔ)句。這種不對(duì)稱(chēng)性阻止了在雙人游戲中獲得成功的自博弈算法的簡(jiǎn)單應(yīng)用。

在這項(xiàng)工作中，研究者通過(guò)從一個(gè)語(yǔ)言模型中采樣動(dòng)作來(lái)解決無(wú)限動(dòng)作空間問(wèn)題。語(yǔ)言模型能夠生成策略調(diào)用以及通常需要作為參數(shù)的原始數(shù)學(xué)術(shù)語(yǔ)。對(duì)于自博弈的缺乏，他們觀察到，自博弈在兩人游戲中的關(guān)鍵作用是提供一個(gè)無(wú)監(jiān)督的課程（curriculum）。因此，他們建議用一套不同難度的輔助問(wèn)題命題（不需要證明）來(lái)代替這種無(wú)監(jiān)督的課程。他們的實(shí)驗(yàn)結(jié)果表明，當(dāng)這些輔助問(wèn)題的難度變化足夠大時(shí)，他們的訓(xùn)練程序就能夠解決一系列越來(lái)越難的問(wèn)題，最終推廣到他們所關(guān)心的問(wèn)題集。

雖然這些結(jié)果非常令人興奮，因?yàn)樗鼈冏C明了深度學(xué)習(xí)模型在與形式系統(tǒng)交互時(shí)能夠進(jìn)行重要的數(shù)學(xué)推理，但在競(jìng)賽中，該證明器離最佳學(xué)生表現(xiàn)還差得很遠(yuǎn)。研究者表示，他們希望自己的工作將推動(dòng)這一領(lǐng)域的研究，特別是針對(duì) IMO 的研究，并希望他們提出的 statement curriculum learning 方法能夠加快自動(dòng)推理的研究進(jìn)展。

小結(jié)

兩家機(jī)構(gòu)最新的研究成果已經(jīng)介紹完畢，網(wǎng)上已經(jīng)零零散散地出現(xiàn)了關(guān)于效果的評(píng)價(jià)：

如有 AI 研究科學(xué)家發(fā)系列長(zhǎng)推表示，AlphaCode 達(dá)到人類(lèi)水平還需要幾年時(shí)間，它在 codeforce 上的排名是有限制的，如許多參與者是高中生或大學(xué)生；還有就是 AlphaCode 生成的絕大多數(shù)程序都是錯(cuò)誤的，正是使用示例測(cè)試進(jìn)行過(guò)濾才使得 AlphaCode 實(shí)際解決了某些問(wèn)題。

也有研究人員表示，這像是 AlphaStar 大力出奇跡的結(jié)果。

國(guó)內(nèi)的 AI 從業(yè)者們可以趁假期研究下這兩項(xiàng)研究，發(fā)表自己的看法。

參考鏈接：https://openai.com/blog/formal-math/?continueFlag=6cc759bbfb87d518f6d6948bcf276707

https://deepmind.com/blog/article/Competitive-programming-with-AlphaCode?continueFlag=b34ed7683541bab09a68d7ab1d608057

—版權(quán)聲明—

來(lái)源：機(jī)器之心，編輯：nhyilin

僅用于學(xué)術(shù)分享，版權(quán)屬于原作者。

若有侵權(quán)，請(qǐng)聯(lián)系微信號(hào):Eternalhui或nhyilin刪除或修改！

—THE END—

文章推薦

?藝術(shù)中蘊(yùn)含的數(shù)學(xué)原理

?物理學(xué)四大神獸，除了“薛定諤的貓”, 你還知道哪幾個(gè)？

?平凡而又神奇的貝葉斯方法

?怎樣用數(shù)學(xué)找到一顆丟失的氫彈？

?【物理方程】物理學(xué)中最難的方程之一，你知道多少？

?法國(guó)數(shù)學(xué)長(zhǎng)盛不衰的歷史淵源

總結(jié)

以上是生活随笔為你收集整理的卷起来了！DeepMind发布媲美普通程序员的AlphaCode，同日OpenAI神经数学证明器拿下奥数题...的全部?jī)?nèi)容，希望文章能夠幫你解決所遇到的問(wèn)題。

如果覺(jué)得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。