AI“雙子星”同日聯(lián)動：DeepMind加速編程自動化，OpenAI新方法解開2道國際奧數(shù)題

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

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

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

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

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

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

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