2022 年開(kāi)年不久，全球人工智能領(lǐng)域兩大明星公司不約而同在今天宣布了重要進(jìn)展：OpenAI 稱(chēng)自己構(gòu)建了一個(gè)神經(jīng)定理證明器，該證明器學(xué)會(huì)了解決各種具有挑戰(zhàn)性的高中數(shù)學(xué)問(wèn)題，包括 AMC12 和 AIME 比賽的問(wèn)題，以及改編自 IMO 的兩個(gè)問(wèn)題。 DeepMind 則表示，由其開(kāi)發(fā)的名為 AlphaCode 的人工智能系統(tǒng)，該系統(tǒng)的“編程能力能與一般人類(lèi)程序員相競(jìng)爭(zhēng)”。DeepMind 說(shuō)，該系統(tǒng)的結(jié)果是朝著自主編程邁出的重要一步，盡管現(xiàn)在為止 AlphaCode 的能力不一定能代替普通程序員完成日常編程任務(wù)。 本文將分別介紹這兩項(xiàng)成果。
OpenAI：AI 進(jìn)軍數(shù)學(xué)

根據(jù) OpenAI 的介紹，他們的證明器使用語(yǔ)言模型來(lái)尋找形式陳述的證明。每次找到一個(gè)新的證明時(shí)，OpenAI 都會(huì)將其用作新的訓(xùn)練數(shù)據(jù)，用來(lái)改進(jìn)神經(jīng)網(wǎng)絡(luò)，并使其能夠通過(guò)迭代進(jìn)而找到解決更難更復(fù)雜陳述的方案。

OpenAI 在 miniF2F 基準(zhǔn)——一個(gè)具有挑戰(zhàn)性的高中奧林匹克問(wèn)題集合，測(cè)試中取得了目前的最先進(jìn)的水平（41.2% vs 29.3%）。 OpenAI 的方法稱(chēng)之為陳述課程學(xué)習(xí)（statement curriculum learning），包括手動(dòng)收集一組不同難度級(jí)別的陳述（沒(méi)有證據(jù)），其中最難的陳述與OpenAI的目標(biāo)基準(zhǔn)相似。最初，OpenAI 的神經(jīng)證明器能力很弱，只能證明其中的幾個(gè)。 OpenAI 反復(fù)搜索新的證明，并在新發(fā)現(xiàn)的證明上重新訓(xùn)練 OpenAI 的神經(jīng)網(wǎng)絡(luò)，經(jīng)過(guò) 8 次迭代，最終 OpenAI 的證明器在 miniF2F 上測(cè)試時(shí)表現(xiàn)得非常出色。 形式數(shù)學(xué)是一個(gè)令人興奮的研究領(lǐng)域，首先因?yàn)樗哂胸S富性，讓你可以證明需要推理、創(chuàng)造力和洞察力的任意定理；其次因?yàn)樗c游戲的相似性——人工智能在游戲領(lǐng)域取得了驚人的成功——因?yàn)樗靡环N自動(dòng)化的方式來(lái)確定證明是否成功（即，由形式系統(tǒng)驗(yàn)證）。  如下面的簡(jiǎn)單示例所示，證明形式陳述需要生成一系列證明步驟，每個(gè)證明步驟都包含對(duì)策略的調(diào)用。這些策略以數(shù)學(xué)術(shù)語(yǔ)作為論據(jù)，每個(gè)策略調(diào)用都會(huì)將當(dāng)前要證明的陳述轉(zhuǎn)換為更容易證明的陳述，直到?jīng)]有任何東西可以證明。
圖1 問(wèn)題1
通過(guò)觀察發(fā)現(xiàn)，在 OpenAI 的訓(xùn)練過(guò)程中出現(xiàn)了一種能力，即生成作為戰(zhàn)術(shù)參數(shù)所需的原始數(shù)學(xué)術(shù)語(yǔ)。如果沒(méi)有神經(jīng)語(yǔ)言模型，這是無(wú)法完成的。下面的證明就是一個(gè)例子：證明步驟提出使用 n+1 作為解決方案（這完全由 OpenAI 的模型生成），其余的正式證明依靠 ring_exp 策略來(lái)驗(yàn)證它確實(shí)是有效的。
圖2 問(wèn)題2
OpenAI 還觀察到，OpenAI 的模型和搜索程序能夠生成鏈接多個(gè)非平凡推理步驟的證明。在下面的證明中，模型首先使用存在性陳述的對(duì)立。然后使用為它生成一個(gè)見(jiàn)證，并通過(guò)利用 norm_num 策略完成證明。
圖3 問(wèn)題3
OpenAI 的模型經(jīng)過(guò)陳述課程學(xué)習(xí)訓(xùn)練，能夠解決培訓(xùn)教科書(shū)和 AMC12 和 AIME 比賽中的各種問(wèn)題，以及改編自 IMO 的 2 個(gè)問(wèn)題。下面 OpenAI 展示此類(lèi)生成證明的三個(gè)示例。
圖4 問(wèn)題4
圖5 問(wèn)題5
圖6 問(wèn)題6

形式數(shù)學(xué)涉及兩個(gè)主要挑戰(zhàn)，這使得強(qiáng)化學(xué)習(xí)的應(yīng)用不太可能成功。
1）無(wú)限的動(dòng)作空間：形式數(shù)學(xué)不僅有一個(gè)非常大的搜索空間（例如圍棋），它還有一個(gè)無(wú)限的動(dòng)作空間。在證明搜索的每一步，模型不是從行為良好的有限動(dòng)作集中進(jìn)行選擇，而是必須從一組復(fù)雜且無(wú)限的策略中進(jìn)行選擇，其中涉及必須生成的外生數(shù)學(xué)術(shù)語(yǔ)（例如，生成用作見(jiàn)證的數(shù)學(xué)語(yǔ)句，諸如“存在一個(gè) xx st ...”之類(lèi)的步驟中使用的對(duì)象“，或作為剪切，證明中間引理引入和鏈接）。
2）缺乏自我博弈：與二人博弈相反，證明器不是與對(duì)手比賽，而是與一組要證明的陳述進(jìn)行比賽。當(dāng)面對(duì)一個(gè)太難的陳述時(shí)，沒(méi)有明顯的重構(gòu)可以讓證明器生成中間更容易首先解決的陳述。這種不對(duì)稱(chēng)性阻止了在二人博弈中成功的自我博弈算法的應(yīng)用。
在 OpenAI 的工作中，通過(guò)在搜索證明時(shí)，從語(yǔ)言模型中采樣動(dòng)作來(lái)解決無(wú)限動(dòng)作空間問(wèn)題。語(yǔ)言模型能夠生成策略調(diào)用以及通常需要作為參數(shù)的原始數(shù)學(xué)術(shù)語(yǔ)。
其次，OpenAI 觀察到自我博弈在二人博弈中的關(guān)鍵作用是提供無(wú)監(jiān)督的課程，以此作為解決缺乏自我博弈的基礎(chǔ)，OpenAI 的方法建議用一組不同難度的輔助問(wèn)題陳述（不需要證明）來(lái)代替這種無(wú)監(jiān)督的課程。OpenAI 的經(jīng)驗(yàn)表明，當(dāng)這些輔助問(wèn)題的難度足夠多時(shí)，OpenAI 的訓(xùn)練程序能夠解決越來(lái)越難的問(wèn)題的課程，最終推廣到 OpenAI 關(guān)心的問(wèn)題集。
雖然這些結(jié)果非常令人興奮，它們證明了深度學(xué)習(xí)模型在與正式系統(tǒng)交互時(shí)能夠進(jìn)行非凡的數(shù)學(xué)推理，但與這些比賽中最好的學(xué)生的表現(xiàn)相比，OpenAI 的方法還差得很遠(yuǎn)。 未來(lái)，OpenAI 希望，自己的工作能夠激發(fā)該領(lǐng)域的研究，特別是針對(duì) IMO 大挑戰(zhàn)，與此同時(shí)，OpenAI 提出的陳述式課程學(xué)習(xí)方法，或?qū)⒂兄诩铀僮詣?dòng)化推理的總體進(jìn)展。
DeepMind：寫(xiě)代碼自動(dòng)化更進(jìn)一步
DeepMind 創(chuàng)建了一個(gè)名為 AlphaCode 的人工智能系統(tǒng)，該系統(tǒng)的“編程能力能與一般人類(lèi)程序員相競(jìng)爭(zhēng)”。

開(kāi)發(fā)團(tuán)隊(duì)針對(duì)人類(lèi)競(jìng)賽中使用的編程挑戰(zhàn)題目測(cè)試了該人工智能系統(tǒng)，發(fā)現(xiàn)其程序達(dá)到了“預(yù)期的排名”，使其在人類(lèi)程序員中排名前 54%。DeepMind 說(shuō)，該系統(tǒng)的結(jié)果是朝著自主編程邁出的重要一步，盡管現(xiàn)在為止 AlphaCode 的能力不一定能代替普通程序員完成日常編程任務(wù)。 DeepMind 的首席研究科學(xué)家 OriolVinyals 通過(guò)電子郵件告訴 The Verge，研究仍處于早期階段，但結(jié)果使公司更接近于創(chuàng)建一個(gè)靈活的、解決問(wèn)題的人工智能——一個(gè)可以自主應(yīng)對(duì)目前僅屬于人類(lèi)領(lǐng)域的編碼挑戰(zhàn)的程序。Vinyals 說(shuō)：“從長(zhǎng)遠(yuǎn)來(lái)看，我們對(duì)【AlphaCode】幫助程序員和非程序員編寫(xiě)代碼、提高生產(chǎn)力或者創(chuàng)建新的軟件制作方法的潛力感到興奮?！?/span> AlphaCode 根據(jù) Codeforces 策劃的挑戰(zhàn)進(jìn)行了測(cè)試，Codeforces 是一個(gè)競(jìng)爭(zhēng)性的編碼平臺(tái)，每周共享問(wèn)題，并為編碼人員發(fā)布類(lèi)似于國(guó)際象棋中使用的 Elo 評(píng)級(jí)系統(tǒng)的排名。這些挑戰(zhàn)不同于編碼器在制作（例如商業(yè)應(yīng)用程序）時(shí)可能面臨的任務(wù)類(lèi)型。它們更自成一體，需要更廣泛地了解計(jì)算機(jī)科學(xué)的算法和理論概念。把它們想象成結(jié)合了邏輯、數(shù)學(xué)和編碼專(zhuān)業(yè)知識(shí)的非常專(zhuān)業(yè)的謎題。 在 AlphaCode 測(cè)試的一個(gè)示例挑戰(zhàn)中，要求競(jìng)爭(zhēng)對(duì)手找到一種方法，使用有限的輸入集將一串隨機(jī)、重復(fù)的s和t字母轉(zhuǎn)換為另一串相同的字母。例如，競(jìng)爭(zhēng)對(duì)手不能只鍵入新字母，而是必須使用刪除原始字符串中幾個(gè)字母的“退格”命令。您可以閱讀以下挑戰(zhàn)的完整描述：

其中 10 個(gè)挑戰(zhàn)以與人類(lèi)完全相同的格式輸入 AlphaCode。然后，AlphaCode 生成大量可能的答案，并像人類(lèi)競(jìng)爭(zhēng)對(duì)手一樣通過(guò)運(yùn)行代碼和檢查輸出來(lái)篩選這些答案?！罢麄€(gè)過(guò)程是自動(dòng)的，無(wú)需人工選擇最佳樣本，”AlphaCode 論文的聯(lián)合負(fù)責(zé)人 Yujia Li 和 David Choi 通過(guò)電子郵件告訴 The Verge。 AlphaCode 針對(duì) Codeforces 網(wǎng)站上 5,000 名用戶解決的 10 項(xiàng)挑戰(zhàn)進(jìn)行了測(cè)試。平均而言，它的排名在前 54.3%，DeepMind 估計(jì)這使該系統(tǒng)的 Codeforces Elo 為 1238，這使其在過(guò)去六個(gè)月中在該網(wǎng)站上競(jìng)爭(zhēng)的用戶中排名前 28%。 “我可以肯定地說(shuō) AlphaCode 的結(jié)果超出了我的預(yù)期，”Codeforces 創(chuàng)始人 Mike Mirzayanov 在 DeepMind 發(fā)布的一份聲明中這樣說(shuō)?！拔页謶岩蓱B(tài)度，因?yàn)榧词乖诤?jiǎn)單的競(jìng)爭(zhēng)問(wèn)題中，通常不僅需要實(shí)現(xiàn)算法，更需要（這是最困難的部分）發(fā)明它。AlphaCode 成功地達(dá)到了一個(gè)有前途的、新競(jìng)爭(zhēng)對(duì)手的水平?！?/span>

DeepMind 指出，AlphaCode 目前的技能僅適用于競(jìng)爭(zhēng)性編程領(lǐng)域，但它的能力為創(chuàng)建未來(lái)工具打開(kāi)了新大門(mén)，這些工具使編程更易于進(jìn)行，并且有朝一日完全自動(dòng)化。 許多其他公司正在開(kāi)發(fā)類(lèi)似的應(yīng)用程序。例如，微軟和 AI 實(shí)驗(yàn)室 OpenAI 已將后者的語(yǔ)言生成程序 GPT-3 改編為輸出代碼字符串的自動(dòng)完成程序。（與 GPT-3 一樣，AlphaCode 也基于稱(chēng)為 transformer 的 AI 架構(gòu)，它特別擅長(zhǎng)解析自然語(yǔ)言和代碼這類(lèi)順序文本）。對(duì)于終端用戶來(lái)說(shuō)，這些系統(tǒng)就像 Gmail 的 Smart Compose 功能一樣工作：為完成您正在編寫(xiě)的任何內(nèi)容出謀劃策。 近年來(lái)，人工智能編程系統(tǒng)的開(kāi)發(fā)取得了很大進(jìn)展，但這些系統(tǒng)還遠(yuǎn)未準(zhǔn)備好接管人類(lèi)程序員的工作。他們產(chǎn)出的代碼通常有些問(wèn)題，而且由于系統(tǒng)通常是在公共代碼庫(kù)上進(jìn)行訓(xùn)練的，因此他們有時(shí)會(huì)“復(fù)制”受版權(quán)保護(hù)的材料。 在一項(xiàng)由代碼存儲(chǔ)庫(kù) GitHub 開(kāi)發(fā)的名為 Copilot 的 AI 編程工具的研究中，研究人員發(fā)現(xiàn)其輸出代碼的大約 40% 包含安全漏洞。安全分析師甚至建議，不良行為者可以故意編寫(xiě)代碼并與隱藏的在線后門(mén)共享代碼，然后這些代碼可能被用來(lái)訓(xùn)練人工智能程序，將這些錯(cuò)誤插入到未來(lái)的程序中。 像這樣的挑戰(zhàn)意味著人工智能編程系統(tǒng)可能會(huì)慢慢融入程序員的工作中——從助手開(kāi)始，他們的建議在能夠被信任之前都將受到懷疑。換句話說(shuō)：他們要香徒弟跟師傅一樣接受專(zhuān)業(yè)程序員的訓(xùn)練。目前為止，這些 AI 編程系統(tǒng)正在飛快地學(xué)習(xí)。