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

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

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

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

IMO 上同步做題，做對(duì)了最難題

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

在今年的 IMO 競(jìng)賽上，由 DeepMind 團(tuán)隊(duì)研發(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 競(jìng)賽的？

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

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

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

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

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

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

AlphaProof：一種形式化推理方法

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

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

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

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

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

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

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

更具競(jìng)爭(zhēng)力的 AlphaGeometry 2

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

AlphaGeometry 2 采用的符號(hào)引擎比上一代產(chǎn)品快兩個(gè)數(shù)量級(jí)。當(dāng)遇到新問題時(shí)，新穎的知識(shí)共享機(jī)制可實(shí)現(xiàn)不同搜索樹的高級(jí)組合，以解決更復(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)建許多對(duì)相似三角形，如 ABE ~ YBI 和 ALE ~ IPC，以證明結(jié)論。

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

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

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

研究團(tuán)隊(duì)

谷歌表示，新研究得到了國際數(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)和管理整個(gè)項(xiàng)目。