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

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

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

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

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

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

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

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

　　01

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

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

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

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

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

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

　　02

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

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

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

　　每年，頂尖的大學前數(shù)學家們都要訓練，有時要訓練數(shù)千小時，以解決代數(shù)、組合學、幾何學和數(shù)論領域的六道極其困難的難題。菲爾茲獎是數(shù)學家的最高榮譽之一，許多獲獎者都曾代表他們的國家參加過國際數(shù)學奧林匹克比賽。

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

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

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

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

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

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

　　03

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

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

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

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

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

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

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

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

　　04

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

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

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

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

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

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

　　谷歌DeepMind的原文：

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

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

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