對于 AI 來說，奧數(shù)不再是問題了。

本周四，谷歌 DeepMind 的人工智能完成了一項壯舉：用 AI 做出了今年國際數(shù)學(xué)奧林匹克競賽 IMO 的真題，并且距拿金牌僅一步之遙。

上周剛剛結(jié)束的 IMO 競賽共有六道賽題，涉及代數(shù)、組合學(xué)、幾何和數(shù)論。谷歌提出的混合 AI 系統(tǒng)做對了四道，獲得 28 分，達(dá)到了銀牌水平。

本月初，UCLA 終身教授陶哲軒剛剛宣傳了百萬美元獎金的 AI 數(shù)學(xué)奧林匹克競賽（AIMO 進(jìn)步獎），沒想到 7 月還沒過，AI 的做題水平就進(jìn)步到了這種水平。

IMO 上同步做題，做對了最難題

IMO 是歷史最悠久、規(guī)模最大、最負(fù)盛名的青年數(shù)學(xué)家競賽，自 1959 年以來每年舉辦一次。近來，IMO 競賽也被廣泛認(rèn)為是機(jī)器學(xué)習(xí)領(lǐng)域的一項重大挑戰(zhàn)，成為衡量人工智能系統(tǒng)高級數(shù)學(xué)推理能力的理想基準(zhǔn)。

在今年的 IMO 競賽上，由 DeepMind 團(tuán)隊研發(fā)的 AlphaProof 和 AlphaGeometry 2 共同實(shí)現(xiàn)了里程碑式的突破。

其中，AlphaProof 是一種用于形式化數(shù)學(xué)推理的強(qiáng)化學(xué)習(xí)系統(tǒng)，而 AlphaGeometry 2 是 DeepMind 幾何求解系統(tǒng) AlphaGeometry 的改進(jìn)版本。

這一突破表明具有先進(jìn)數(shù)學(xué)推理能力的通用人工智能 (AGI) 有潛力開啟科學(xué)技術(shù)新領(lǐng)域。

那么，DeepMind 的 AI 系統(tǒng)是如何參加 IMO 競賽的？

簡單來說，首先這些數(shù)學(xué)問題被手動翻譯成形式化的數(shù)學(xué)語言，以便 AI 系統(tǒng)理解。在正式比賽中，人類參賽選手分兩節(jié)（兩天）提交答案，每節(jié)限時 4.5 小時。AlphaProof+AlphaGeometry 2 組合成的 AI 系統(tǒng)在幾分鐘內(nèi)就解決了一個問題，但花了三天時間來解決其他問題。雖然如果嚴(yán)格按照規(guī)則來說的話，DeepMind 的系統(tǒng)超時了。有人推測，這里面可能涉及大量的暴力破解。

谷歌表示，AlphaProof 通過確定答案并證明其正確性解決了兩道代數(shù)問題和一道數(shù)論問題。其中包括本次競賽中最難的問題，在今年的 IMO 上只有五名參賽者解決了。而 AlphaGeometry 2 證明了一道幾何問題。

AI 給出的解：https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

IMO 金牌得主、菲爾茲獎得主 Timothy Gowers 和兩屆 IMO 金牌得主、IMO 2024 問題選擇委員會主席 Joseph Myers 博士根據(jù) IMO 評分規(guī)則，對該組合系統(tǒng)給出的解決方案進(jìn)行了評分。

六個問題中的每一個問題滿分 7 分，總分最高 42 分。DeepMind 的系統(tǒng)最終得分為 28 分，意味著解決的 4 個問題都獲得了滿分——相當(dāng)于銀牌類別的最高分。今年的金牌門檻為 29 分，正式比賽的 609 名選手中有 58 人獲得了金牌。

該圖顯示了谷歌 DeepMind 的人工智能系統(tǒng)在 IMO 2024 上相對于人類競爭對手的表現(xiàn)。在總分為 42 分的情況下，該系統(tǒng)獲得了 28 分，達(dá)到了與比賽銀牌獲得者相同的水平。另外，今年 29 分是能拿金牌的。

AlphaProof：一種形式化推理方法

在谷歌使用的混合 AI 系統(tǒng)中，AlphaProof 是一個以形式語言 Lean 來證明數(shù)學(xué)陳述的自訓(xùn)練系統(tǒng)。它結(jié)合了預(yù)訓(xùn)練語言模型與 AlphaZero 強(qiáng)化學(xué)習(xí)算法。

其中，形式語言為形式化地驗(yàn)證數(shù)學(xué)推理證明的正確性，提供了重要優(yōu)勢。在此之前，這在機(jī)器學(xué)習(xí)中的使用一直受限，因?yàn)槿斯ぞ帉憯?shù)據(jù)數(shù)量非常有限。

相比之下，基于自然語言的方法盡管可以訪問更多量級的數(shù)據(jù)，但會產(chǎn)生看似合理而不正確的中間推理步驟與解法。

谷歌 DeepMind 通過微調(diào) Gemini 模型自動將自然語言問題陳述翻譯為形式陳述，在這兩個互補(bǔ)領(lǐng)域之間建立了一座橋梁，從而創(chuàng)建了一個包含不同難度形式問題的大型庫。

給到數(shù)學(xué)問題，AlphaProof 會生成候選解題方案，然后通過搜索 Lean 中可能的證明步驟來證明它們。找到并驗(yàn)證的每個證明方案，都用來強(qiáng)化 AlphaProof 的語言模型，增強(qiáng)其解決后續(xù)更具挑戰(zhàn)性問題的能力。

為訓(xùn)練 AlphaProof，谷歌 DeepMind 在 IMO 比賽前幾周內(nèi)證明或反證明了涵蓋廣泛難度與主題的數(shù)百萬個數(shù)學(xué)問題。比賽期間還應(yīng)用了訓(xùn)練 loop，以強(qiáng)化自生成競賽題變體的證明，直到找到完整的解決方案。

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

更具競爭力的 AlphaGeometry 2

AlphaGeometry 2 是今年登上《自然》雜志的數(shù)學(xué) AI AlphaGeometry 的重大改進(jìn)版本。它是一個神經(jīng) - 符號混合系統(tǒng)，其中的語言模型基于 Gemini，并在比其前身多一個數(shù)量級的合成數(shù)據(jù)上從頭開始訓(xùn)練。這有助于該模型解決更具挑戰(zhàn)性的幾何問題，包括有關(guān)物體運(yùn)動以及角度、比例或距離方程的問題。

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

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

問題 4 的示例，要求證明∠KIL 與∠XPY 的和等于 180°。AlphaGeometry 2 提議在直線 BI 上構(gòu)造點(diǎn) E，使得∠AEB = 90°。點(diǎn) E 有助于賦予線段 AB 中點(diǎn) L 以意義，從而創(chuàng)建許多對相似三角形，如 ABE ~ YBI 和 ALE ~ IPC，以證明結(jié)論。

谷歌 DeepMind 還報告說，作為 IMO 工作的一部分，研究人員還試驗(yàn)了一種基于 Gemini 和一種最新的自然語言推理系統(tǒng)，希望實(shí)現(xiàn)高級的問題解決能力。該系統(tǒng)不需要將問題翻譯成正式語言，并且可以與其他 AI 系統(tǒng)相結(jié)合。在今年的 IMO 賽題的測試中「顯示出了巨大的潛力」。

谷歌正在繼續(xù)探索推進(jìn)數(shù)學(xué)推理的 AI 方法，并計劃很快發(fā)布有關(guān) AlphaProof 的更多技術(shù)細(xì)節(jié)。

我們對未來充滿期待，數(shù)學(xué)家們將使用 AI 工具探索假設(shè)，嘗試大膽的新方法來解決長期存在的問題，并快速完成耗時的證明元素——而像 Gemini 這樣的 AI 系統(tǒng)將在數(shù)學(xué)和更廣泛的推理方面變得更加強(qiáng)大。

研究團(tuán)隊

谷歌表示，新研究得到了國際數(shù)學(xué)奧林匹克組織的支持，此外：

AlphaProof 的開發(fā)由 Thomas Hubert、Rishi Mehta 和 Laurent Sartran 領(lǐng)導(dǎo)；主要貢獻(xiàn)者包括 Hussain Masoom、Aja Huang、Miklós Z. Horváth、Tom Zahavy、Vivek Veeriah、Eric Wieser、Jessica Yung、Lei Yu、Yannick Schroecker、Julian Schrittwieser、Ottavia Bertolli、Borja Ibarz、Edward Lockhart、Edward Hughes、Mark Rowland 和 Grace Margand。

其中，Aja Huang、Julian Schrittwieser、Yannick Schroecker 等成員也是 8 年前（2016 年）AlphaGo 論文的核心成員。8 年前，他們基于強(qiáng)化學(xué)習(xí)打造的 AlphaGo 聲名大噪。8 年后，強(qiáng)化學(xué)習(xí)在 AlphaProof 中再次大放異彩。有人在朋友圈感嘆說：RL is so back！

AlphaGeometry 2 和自然語言推理工作由 Thang Luong 領(lǐng)導(dǎo)。AlphaGeometry 2 的開發(fā)由 Trieu Trinh 和 Yuri Chervonyi 領(lǐng)導(dǎo)，Mirek Ol?ák、Xiaomeng Yang、Hoang Nguyen、Junehyuk Jung、Dawsen Hwang 和 Marcelo Menegali 做出了重要貢獻(xiàn)。

此外，David Silver、Quoc Le、哈薩比斯和 Pushmeet Kohli 負(fù)責(zé)協(xié)調(diào)和管理整個項目。