每年夏天，來自全球的青年數學天才匯聚一堂，參加被譽為「數學世界杯」的國際數學奧林匹克競賽（IMO）。

比賽6道題分兩天完成，每題滿分7分，總分42分，難度極高，往往只有不到1%的參賽者能全對所有題目。

橫軸為分數（7分滿），縱軸為人數

近年來，IMO也被視為AI領域的終極挑戰之一，是測試AI高級數學推理能力的理想舞臺。

2024年，谷歌DeepMind團隊讓一位特殊的「選手」參與了IMO角逐——一個名為AlphaProof的AI系統。

它取得了28分的高分，僅以1分之差無緣金牌，達到了銀牌水平。

這是有史以來AI系統首次在IMO這樣的頂級賽事中獲得相當于獎牌的成績，標志著機器在數學難題上的攻關能力邁上新臺階。

AlphaProof：數學解題AI高手登場

AlphaProof是DeepMind最新研發的「數學解題AI」系統，專門為證明復雜數學命題而設計。

簡單來說，如果把數學題視作需要攻克的「迷宮」，AlphaProof就是一個自學成才的AI解題高手。

不同于我們常見的ChatGPT這類純粹用自然語言「思考」的模型，AlphaProof走了一條獨特的道路：它在計算機可驗證的形式化語言中進行推理，從而確保每一步推導都嚴格正確，不會出現憑空捏造的「靈光一閃」卻實則謬誤的步驟。

AlphaProof使用了數學領域流行的形式化證明語言Lean來書寫證明。

Lean語言示例

Lean的語法接近數學和編程語言的結合體，允許AI輸出的每一步推理都被自動檢查驗證，避免了常規語言模型可能出現的謬誤。

AlphaProof給出的答案不是靠人類評審的文字解釋，而是一份計算機逐行檢驗通過的嚴謹證明。

這種將AI思維「硬化」成機械可核查形式的方式，讓AlphaProof在解答再難的題目時也沒有半點僥幸成分。

技術秘訣：大模型牽手強化學習

AlphaProof成功的核心秘訣在于將預訓練大語言模型的「聰明直覺」和AlphaZero強化學習算法的「勤學苦練」巧妙結合。

語言模型擅長從海量數據中學習人類解題的經驗和模式；

而強化學習則讓AI通過不斷嘗試錯誤，不斷改進策略，正如小孩反復練習最終學會騎自行車。

DeepMind團隊先利用大模型為AlphaProof打下「學識」基礎，然后讓它在模擬的數學環境中反復練習，自己發現解題策略。

研究者首先收集了近一百萬道數學題（涵蓋不同領域和難度），利用谷歌最新的Gemini將這些自然語言描述的題目自動翻譯成形式化的Lean代碼表述。

這一過程相當于為AlphaProof打造了一個規?？涨暗念}庫——團隊共獲得了約8000萬條形式化的數學命題，可以讓AI來練習證明。

有了這個「題?！购?，AlphaProof先經過監督學習微調，掌握基本的Lean語言證明技巧。

接著，它進入強化學習階段：像AlphaGo下棋自我對弈一樣，AlphaProof在Lean證明環境中與自己切磋。

每當AlphaProof找到一道題的正確證明并通過驗證，就用這一成功案例來立即強化自身的模型參數，使它下次能更有效地解決更有難度的新問題。

這種邊練邊學的訓練循環持續進行，AlphaProof在數以百萬計的問題證明中不斷進步，逐漸掌握高難度問題所需的關鍵技能。

AlphaProof在搜索證明的時候并非毫無頭緒地「暴力窮舉」。

它采用了類似于棋類AI中蒙特卡羅樹搜索的策略，會智能地將復雜問題拆解成若干子目標各個擊破，并靈活調整搜索方向。

在某些情況下，AlphaProof能在看似無限的可能推導中邁出恰到好處的一步，展現出仿佛人類數學家般的「靈光一閃」。

這既歸功于大模型提供的直覺指導，也離不開強化學習反復探索帶來的全面搜索能力——兩者結合，使得AlphaProof比以往的任何AI系統都更善于在復雜的數學迷宮中找到出路。

奧賽奪銀：AI解題里程碑

DeepMind的AlphaProof與AlphaGeometry 2聯手在2024年IMO的6道競賽題中解出了4道，獲得了28分（滿分42分），達到了銀牌選手的成績。

這一得分距離當年金牌線僅差一分（29分），幾乎觸及金牌門檻。

在解出的題目中，AlphaProof單獨解決了其中3題（包括2道代數題和1道數論題），其中就包括了整場比賽最難的第6題——該題在600多名頂尖學生中也只有5人滿分解決。

剩余的一道幾何題則由專攻幾何的AlphaGeometry 2模型完成，而兩道組合數學題由于難以形式化和搜索爆炸等原因未能攻克。

最終，這套AI系統拿下4題滿分（其余2題為0分），分數正好處于銀牌段的頂端。

要知道，在人類選手中也只有不到10%的人能拿到金牌，今年共有58名選手得分不低于29分。

AlphaProof取得的銀牌水平成績，足以比肩一位受過多年訓練的國際頂尖高中生天才選手。

這一成果令許多專家感到震撼：著名數學家、菲爾茲獎得主高爾斯評價說，AlphaProof給出的某些巧妙構造「遠超出我以為AI目前能夠做到的水平」。

AlphaProof在IMO上的表現具有里程碑意義。

這是AI首次在如此高難度的數學競賽中達到人類獎牌選手的水準，表明AI的數學推理能力實現了重大飛躍。

過去，大模型即便掌握了海量教材和定理，也常常難以完整解決奧賽級別的挑戰，更不用說給出嚴格證明。

而AlphaProof通過形式化證明和強化學習，真正讓AI具備了解決開放性數學難題的實力。

它成功證明了IMO中最困難題目的事實也讓人看到了希望：或許將來AI有潛力輔助人類攻克懸而未決的數學猜想。

局限與未來

AI數學家的進階之路

盡管AlphaProof令人眼前一亮，但目前它仍有不少局限。

其一，解題效率是個問題。

人類選手必須在4.5小時內完成3題，而AlphaProof雖然最后找出了3題的解法，卻耗費了將近3天時間。

這表明當前AI證明方法在搜索速度和計算資源上還有很大提升空間。

其二，AlphaProof并非萬能，它未能解決的兩道組合數學題恰恰反映了某些類型的問題對AI而言依然棘手。

這類題目往往涉及高度非結構化的創新思維，超出了AlphaProof主要從訓練中「見過」的范疇。

因此，如何讓AI擁有更強的通用性和適應性，去應對未曾遇見的新穎難題，是下一步的重要挑戰。

其三，目前AlphaProof需要人工先將題目翻譯成Lean的形式化表達，它自己并不理解自然語言問題。

這意味著它無法自主讀題，也無法像人類數學家那樣提出新的問題或判斷哪些問題值得研究。

正如倫敦數學科學研究所的何楊輝所指出的，AlphaProof可以作為協助數學家證明的有力工具，但它還不能替代人類去發現和選擇研究課題。

何楊輝

面對這些局限，DeepMind團隊表示他們將繼續探索多種途徑來提升AI的數學推理能力。

未來的研發方向之一是讓AI擺脫對人工翻譯的依賴，直接閱讀理解自然語言表述的數學題，并給出形式化證明。

同時，針對不同類別的數學問題（如組合數學或幾何），可能需要引入更專業的策略，比如融合符號計算、知識庫或分領域訓練的模型，從而全面提高AI的解題覆蓋面。

還有研究者設想，將來數學家可以與這樣的AI證明助手協同工作：

AI快速驗證人類猜想和小引理，甚至嘗試大膽的思路攻克長期懸而未決的難題；

人類則專注于提出有意義的問題和整體證明構想。

可以預見，隨著AlphaProof這類系統的不斷完善，我們正迎來人機攜手探尋數學前沿的新紀元。

AlphaProof展現出的形式化推理能力對AI安全和可靠性也有啟發意義。

它輸出的每一步推理都可追溯、驗證，這種「嚴謹求證」的風格或許可用于改進未來的大模型，讓它們在回答開放性問題時減少荒誕的臆測。

當AI變得越來越強大，我們更希望它是一個踏實嚴謹的「數學家」。

經過此次奧賽洗禮，AlphaProof讓我們看到了AI在純粹理性領域逼近人類頂尖水平的曙光。

當然，人類頂尖數學家的創造力和洞察力依然不可替代——至少在提出問題和宏觀思路上，AI還有很長的路要走。

但毫無疑問，AI正在成為人類探索數學未知的一雙有力之手。

無論人類或AI，攀登真理高峰的道路上，永遠需要勇氣、耐心與對未知的敬畏。