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

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

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

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

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

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

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

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

　　01

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

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

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

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

　　此外，技術(shù)越強(qiáng)大，我們就越需要努力保護(hù)人類(lèi)文明和人性的光輝。我們需要建立一個(gè)人們?cè)敢夤餐押煤献鳎嗷ブС值?，讓人?lèi)感到安全和進(jìn)步的社群，而不是成為一個(gè)個(gè)為了競(jìng)爭(zhēng)在內(nèi)卷中彼此爭(zhēng)斗打壓的個(gè)體。分裂則衰。對(duì)我來(lái)說(shuō)，這與建立人類(lèi)智能密切相關(guān)，如果我們培養(yǎng)一個(gè)尋求打敗他人的‘人才’而不是幫助他人的人才可能是有害的。”

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

　　02

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

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

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

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

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

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

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

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

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

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

　　03

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

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

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

(AlphaProof研發(fā)團(tuán)隊(duì)部分成員)

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

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

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

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

　　04

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

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

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

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

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

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

　　谷歌DeepMind的原文：

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

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

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