里程碑！谷歌新的AI模型在國際奧數(shù)IMO方面達(dá)到銀牌水平

　　前一段時間，部分大模型連9.11和9.9誰大都分不清，而今，高級數(shù)學(xué)推理問題被破解了!

　　7月25日，谷歌DeepMind團隊發(fā)文宣布，推出基于強化學(xué)習(xí)的新型形式數(shù)學(xué)推理系統(tǒng) AlphaProof，以及幾何求解系統(tǒng)的改進(jìn)版本 AlphaGeometry 2。這兩個系統(tǒng)共同解決了今年國際數(shù)學(xué)奧林匹克(IMO) 六道題目中的四道，首次在競賽中取得與銀牌得主同等的成績。

　　谷歌DeepMind團隊認(rèn)為，具有高級數(shù)學(xué)推理能力的通用人工智能（AGI）有可能開辟科學(xué)技術(shù)的新領(lǐng)域。

　　“這是機器學(xué)習(xí)和人工智能領(lǐng)域的一大進(jìn)步，”參與該項目的谷歌 DeepMind 研究副總裁 Pushmeet Kohli 表示。“迄今為止，還沒有開發(fā)出能夠以如此高的成功率和如此普遍性解決問題的系統(tǒng)。”

　　作為 IMO 工作的一部分，DeepMind還試驗了一種基于Gemini和谷歌最新研究的自然語言推理系統(tǒng)，以實現(xiàn)高級問題解決技能。該系統(tǒng)不需要將問題翻譯成形式語言，并且可以與其他 AI 系統(tǒng)結(jié)合使用。DeepMind還在今年的 IMO 問題上測試了這種方法，結(jié)果顯示出巨大的潛力。

　　DeepMind的團隊正在繼續(xù)探索多種用于推進(jìn)數(shù)學(xué)推理的人工智能方法，并計劃很快發(fā)布有關(guān) AlphaProof 的更多技術(shù)細(xì)節(jié)。

　　DeepMind團隊提到：“很高興看到未來數(shù)學(xué)家們能夠利用人工智能工具探索假設(shè)，嘗試大膽的新方法來解決長期存在的問題，并快速完成耗時的證明步驟——而像Gemini這樣的人工智能系統(tǒng)在數(shù)學(xué)和更廣泛的推理方面的能力將變得更強。”

　　01

　　高級數(shù)學(xué)推理進(jìn)入新階段，教育將如何改變?

　　AI在數(shù)學(xué)推理方面的進(jìn)步讓許多人感到震撼，同時也引發(fā)了對教育的思考。

　　前美國奧數(shù)隊總教練羅博深教授認(rèn)為，“極強的學(xué)術(shù)技能將不再是一人獨有的硬核技術(shù)。而擁有能夠認(rèn)識未來世界的全局的洞察力和應(yīng)變力將變得至關(guān)重要。學(xué)會發(fā)現(xiàn)問題提出問題，學(xué)會整合和利用資源，理解那些在完成目標(biāo)的過程中遇到的一個個小問題，才是一個人能夠有策略地解決任何難題的關(guān)鍵。按照目前的發(fā)展趨勢，人類無法在速度和準(zhǔn)確性上擊敗計算機，但更加迫在眉睫的是，我們需要找到屬于自己的那條，旁人和人工智都能未曾踏入的河流。”

　　對于孩子教育的問題，他說：“現(xiàn)在，AI已經(jīng)能夠解決IMO問題，這意味著它們已經(jīng)學(xué)會了解決沒有見過的新問題，這幾乎是人類最有價值的技能之一，因此，現(xiàn)有的教育方法需要快速改變。不管人們是否愿意承認(rèn)，我們的教育結(jié)構(gòu)目前深受標(biāo)準(zhǔn)化考試影響，學(xué)生仍然在‘被迫’追求解題的熟練程度。但現(xiàn)在，每個人都需要學(xué)習(xí)如何解決他們以前從未見過的問題，以跟上AI的發(fā)展。

　　此外，技術(shù)越強大，我們就越需要努力保護(hù)人類文明和人性的光輝。我們需要建立一個人們愿意共同友好合作，相互支持的，讓人類感到安全和進(jìn)步的社群，而不是成為一個個為了競爭在內(nèi)卷中彼此爭斗打壓的個體。分裂則衰。對我來說，這與建立人類智能密切相關(guān)，如果我們培養(yǎng)一個尋求打敗他人的‘人才’而不是幫助他人的人才可能是有害的。”

　　劍橋大學(xué)專門研究數(shù)學(xué)和人工智能研究員凱蒂·柯林斯 (Katie Collins) 表示：“創(chuàng)建能夠解決更具挑戰(zhàn)性的數(shù)學(xué)問題的人工智能系統(tǒng)可以為激動人心的人機合作鋪平道路，幫助數(shù)學(xué)家解決和發(fā)明新類型的問題。這反過來可以幫助我們更多地了解人類如何解決數(shù)學(xué)問題。”

　　02

　　模型達(dá)到了國際奧數(shù)IMO銀牌水平

　　人工智能模型可以輕松生成論文和其他類型的文本。然而，它們在解決數(shù)學(xué)問題方面卻遠(yuǎn)遠(yuǎn)不夠，因為數(shù)學(xué)問題往往需要邏輯推理，而這超出了大多數(shù)當(dāng)前人工智能系統(tǒng)的能力。而谷歌DeepMind的新模型終于突破了高難度的數(shù)學(xué)問題。

　　眾所周知，國際數(shù)學(xué)奧林匹克競賽是歷史最悠久、規(guī)模最大、最負(fù)盛名的青年數(shù)學(xué)競賽，自 1959 年起每年舉辦。

　　每年，頂尖的大學(xué)前數(shù)學(xué)家們都要訓(xùn)練，有時要訓(xùn)練數(shù)千小時，以解決代數(shù)、組合學(xué)、幾何學(xué)和數(shù)論領(lǐng)域的六道極其困難的難題。菲爾茲獎是數(shù)學(xué)家的最高榮譽之一，許多獲獎?wù)叨荚硭麄兊膰覅⒓舆^國際數(shù)學(xué)奧林匹克比賽。

　　近年來，一年一度的國際數(shù)學(xué)奧林匹克競賽也被廣泛認(rèn)為是機器學(xué)習(xí)領(lǐng)域的一大挑戰(zhàn)，也是衡量人工智能系統(tǒng)高級數(shù)學(xué)推理能力的理想基準(zhǔn)。

　　今年，DeepMind將聯(lián)合人工智能系統(tǒng)應(yīng)用于 IMO 主辦方提供的競賽問題。DeepMind的解決方案由著名數(shù)學(xué)家、IMO 金牌得主和菲爾茲獎得主蒂莫西·高爾斯爵士教授和兩屆 IMO 金牌得主、IMO 2024 問題選擇委員會主席約瑟夫·邁爾斯博士根據(jù) IMO 的評分規(guī)則進(jìn)行評分。

　　DeepMind采用的方式是：首先，問題被手動翻譯成正式的數(shù)學(xué)語言，以便模型理解。在正式比賽中，學(xué)生分兩節(jié)提交答案，每節(jié) 4.5 小時。而DeepMind的模型在幾分鐘內(nèi)解決了一個問題，而解決其他問題則需要三天時間。

　　AlphaProof 通過確定答案并證明其正確性，解決了兩道代數(shù)題和一道數(shù)論題。其中包括比賽中最難的一道題，今年的 IMO 比賽中只有五名選手解決了這道題。AlphaGeometry 2 解決了幾何問題，而兩道組合問題仍未解決。

　　六道題目每道可得 7 分，總分最高為 42 分。DeepMind的模型最終得分為 28 分，每道題目都獲得滿分 ，相當(dāng)于銀牌類別的最高分。今年，金牌門檻為 29 分，在正式比賽中，609 名參賽者中有 58 人達(dá)到了金牌門檻。

(圖表顯示了谷歌AI 模型在 IMO 2024 中相對于人類競爭對手的表現(xiàn)，其獲得了總分 42 分中的 28 分，達(dá)到與比賽中銀牌得主相同的水平。)

　　03

　　AlphaProof：一種形式化的推理方法

　　AlphaProof 是一個自我訓(xùn)練的系統(tǒng)，用于用形式語言Lean來證明數(shù)學(xué)陳述。它將預(yù)先訓(xùn)練好的語言模型與AlphaZero強化學(xué)習(xí)算法結(jié)合在一起，后者之前曾自學(xué)過如何掌握國際象棋、將棋和圍棋等益智游戲。

　　形式語言的關(guān)鍵優(yōu)勢在于，涉及數(shù)學(xué)推理的證明可以得到形式化驗證，以確保其正確性。然而，它們在機器學(xué)習(xí)中的應(yīng)用此前一直受到人工編寫數(shù)據(jù)量非常少的限制。

(AlphaProof研發(fā)團隊部分成員)

　　相比之下，基于自然語言的方法盡管能夠訪問數(shù)量級更多的數(shù)據(jù)，卻可能產(chǎn)生看似合理但實際上不正確的中間推理步驟和解決方案。DeepMind通過微調(diào)Gemini模型來自動將自然語言問題陳述轉(zhuǎn)換為形式陳述，從而在這兩個互補領(lǐng)域之間建立了一座橋梁，創(chuàng)建了一個包含各種難度的形式化問題的大型問題庫。

　　當(dāng)遇到問題時，AlphaProof 會生成解決方案候選，然后通過搜索 Lean 中可能的證明步驟來證明或反駁這些候選。每個找到并驗證的證明都會用于強化 AlphaProof 的語言模型，從而提高其解決后續(xù)更具挑戰(zhàn)性的問題的能力。

　　在比賽開始前的幾周內(nèi)，DeepMind通過證明或反證數(shù)百萬道題目來訓(xùn)練 AlphaProof，題目涉及各種難度和數(shù)學(xué)主題。比賽期間也應(yīng)用了訓(xùn)練循環(huán)，不斷強化對競賽題目自生成變體的證明，直到找到完整的解決方案。

(AlphaProof 強化學(xué)習(xí)訓(xùn)練循環(huán)的流程圖：形式化網(wǎng)絡(luò)將大約一百萬個非正式數(shù)學(xué)問題翻譯成正式數(shù)學(xué)語言。然后，求解器網(wǎng)絡(luò)搜索問題的證明或反證，通過 AlphaZero 算法逐步訓(xùn)練自身以解決更具挑戰(zhàn)性的問題。)

　　04

　　AlphaGeometry 2：解決更具挑戰(zhàn)性的幾何問題

　　AlphaGeometry 2 是AlphaGeometry的一個顯著改進(jìn)版本。它是一個神經(jīng)符號混合系統(tǒng)，其中的語言模型基于Gemini，并使用比其前身多一個數(shù)量級的合成數(shù)據(jù)從頭開始訓(xùn)練。這有助于該模型解決更具挑戰(zhàn)性的幾何問題，包括有關(guān)物體運動和角度、比率或距離等方程式的問題。

　　AlphaGeometry 2 采用的符號引擎比其前代產(chǎn)品快兩個數(shù)量級。當(dāng)遇到新問題時，會使用一種新穎的知識共享機制，來實現(xiàn)不同搜索樹的高級組合，以解決更復(fù)雜的問題。

　　由于AlphaGeometry 2 比前代系統(tǒng)接受了更多合成數(shù)據(jù)的訓(xùn)練，因此能夠解決更具挑戰(zhàn)性的幾何問題。

　　在今年的比賽之前，AlphaGeometry 2 可以解決過去 25 年所有 IMO 幾何問題中的 83%，而其前身的解決率僅為 53%。在 IMO 2024 中，AlphaGeometry 2在獲得形式化后 19 秒內(nèi)就解決了問題 4。

(問題 4 ，要求證明 ∠KIL 與 ∠XPY 之和等于 180°。AlphaGeometry 2 建議構(gòu)造 E，即直線 BI 上的一個點，以便 ∠AEB = 90°。點 E 有助于確定 AB 的中點 L，從而創(chuàng)建證明結(jié)論所需的多對相似三角形，例如 ABE ~ YBI 和 ALE ~ IPC。)

　　谷歌DeepMind的原文：

　　https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

　　谷歌數(shù)學(xué)模型解答第四題的全過程：

　　https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html