
首次證明了透過精巧的框架設計,AI有能力攻克需要深邃人類智慧的數學堡壘。

本文探討了當前大語言模型(LLM)在自動化定理證明(ATP)領域面臨的核心困境——強大的非形式化推理能力與孱弱的形式化證明能力之間的巨大鴻溝。為彌合這一鴻溝,我們提出了一種全新的“解耦推理與證明”框架。本研究由騰訊AI Lab完成,主要作者為梁振文和宋林峰。
論文題目:Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
論文地址:[2507.06804] Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
專案主頁及開源資料:https://tencent-imo.github.io/

01背景與動機:AI數學能力的巨大鴻溝
近年來,以大語言模型為代表的通用人工智慧在數學推理領域取得了長足進步。然而,當面對需要絕對邏輯嚴謹性的形式化數學證明時,AI的能力卻遭遇了瓶頸。這一現象揭示了當前AI數學研究中的一個核心矛盾,也是其“阿喀琉斯之踵”:
在“思考”與“證明”之間,存在一道難以逾越的鴻溝。
最近在頂尖數學競賽難題(如Putnam)上的大規模評測鮮明地印證了這一點:最強大的LLM(如Gemini 2.5 Pro)能夠以超過80%的準確率生成非形式化的解題思路,展現出驚人的數學直覺與推理能力。然而,當要求最先進的形式化證明器(Prover)將這些思路轉化為機器可驗證的嚴格證明時,成功率驟降至不足8%。

AI似乎成了一個“聰明的空想家”——它能想到解法,卻無法嚴格地證明它。現有SOTA證明器(如DeepSeek-Prover-v2)試圖透過在單一模型內融合“思考”(生成草稿)與“證明”(生成程式碼)來解決此問題。但我們的研究發現,這種“耦合”設計存在根本性缺陷:它強迫強大的“思考者”去遷就能力有限的“證明者”,從而扼殺了AI真正的數學潛能。這正是為何即便是最前沿的模型,也始終未能攻克任何一道2000年後的國際數學奧林匹克(IMO)難題。

02核心洞見:訓練正規化導致推理能力退化
為應對這一挑戰,目前最前沿的工作(如DeepSeek-Prover-v2, Kimina)普遍採用一種“一體化”或“耦合式”的方案,即在單個模型內部整合“思考草稿”與“形式化證明”兩個環節。它們試圖讓模型先生成高層思路,再據此產出形式化程式碼。
然而,我們的研究發現,這種看似直觀的設計存在一個根本性的缺陷:它讓模型“帶著鐐銬跳舞”。具體而言,這種耦合架構導致了兩個嚴重問題:
1.推理潛力被扼殺:模型的高層“思考”受到了其自身底層“證明”能力的嚴格束縛。為了確保後續能順利生成可透過驗證的程式碼,模型不敢提出那些真正具有創造性、但形式化難度較高的“奇招”,其所謂的“規劃”能力因此退化。
2.訓練正規化導致能力退化:這些模型普遍採用“可驗證獎勵的強化學習”(RLVR)進行訓練,即只根據最終程式碼是否編譯成功來給予獎勵。這種“成王敗寇”式的粗暴訊號,實際上在鼓勵模型“走捷徑”——放棄深度的、複雜的邏輯構建,轉而依賴ring, omega等自動化“戰術”(tactics)進行暴力嘗試。我們的實驗首次定量證明:這種特化訓練,會導致模型在通用數學推理(如MATH, AIME基準)上的效能顯著下降,即為了“證明”,犧牲了“推理”。
3.這些問題共同導致了現有方法無法真正利用LLM那高達80%的推理潛力,在面對國際數學奧林匹克(IMO)等真正需要“靈光一閃”的難題時,屢戰屢敗。


03解耦框架:讓“戰略家”與“精算師”各司其職
基於上述診斷,我們提出了一種全新的、基於“解耦 (Decoupling)”哲學的自動化定理證明框架。我們認為,與其強迫一個模型同時扮演好“戰略家”和“士兵”兩個角色,不如讓最優秀的人才各司其職。我們的框架由兩個獨立的、可靈活排程的核心模組構成:
1.“推理器”(The Reasoner):我們選用業界最強大的通用大模型(如GPT-4o, Gemini 1.5 Pro)作為推理器。它的唯一任務,就是不受任何形式化約束地進行最高水平的戰略思考,提出解決問題的核心思路,並將其凝練成一系列關鍵的子目標或引理(Lemmas)。這些引理是純粹的數學陳述,是連線高層智慧與底層邏輯的橋樑。
2.“證明器”(The Prover):我們選用最高效的形式化證明模型(如DeepSeek-Prover-v2)作為證明器。它的任務是接收推理器提出的引理,並像一個專注的工匠一樣,逐一驗證它們的正確性。
透過這種“戰略家出謀劃策,實幹家驗證執行”的分工,我們的框架徹底解放了推理器的思考潛力,同時又透過證明器的嚴格驗證保證了每一步的邏輯可靠性。


04里程碑式的實驗結果
我們在一系列極具挑戰性的、2000年後的IMO非幾何難題上驗證了我們框架的有效性。結果是突破性的:
我們的框架成功解決了5道此前所有開源自動化證明器均未能解決的IMO難題。包括:
lIMO 2000 Problem 2
lIMO 2005 Problem 3
lIMO 2011 Problem 3
lIMO 2019 Problem 1
lIMO 2020 Problem 2
這是AI在頂尖數學競賽難題上取得的一次里程碑式的突破,首次證明了透過精巧的框架設計,AI有能力攻克需要深邃人類智慧的數學堡壘。

05開源貢獻與總結
除了方法上的創新,我們深知推動整個社群發展的重要性。為此,我們向公眾開源了本次研究的全部成果:
我們為大量DeepSeek-Prover-V2 671B等模型無法獨立證明的IMO難題,提供了超過600條由我們的框架生成併成功驗證的高質量引理。我們相信,這個資料集將為後續工作解決更多IMO級別的難題提供一個堅實的基礎,無論是對於AI研究者,還是對於人類數學家,都可能帶來新的啟發。
本研究首次系統性地揭示並解決了AI在形式化數學證明中“思考”與“證明”能力失衡的核心矛盾。我們提出的“解耦”框架,不僅在實踐中取得了前所未有的成果,也為未來構建更強大、更具洞察力的人工智慧系統提供了一條全新的、充滿希望的路徑。
總結
本研究由騰訊AI Lab完成。我們不僅提出了一個全新的、有效的自動化定理證明框架,更重要的是,我們深刻揭示了當前領域發展的核心矛盾,併為如何彌合“非形式化推理”與“形式化證明”之間的鴻溝提供了一條清晰可行的道路。透過將“思考的藝術”與“驗證的科學”解耦,我們成功解決了5道頂尖IMO難題。

未經「AI科技評論」授權,嚴禁以任何方式在網頁、論壇、社群進行轉載!
公眾號轉載請先在「AI科技評論」後臺留言取得授權,轉載時需標註來源並插入本公眾號名片。
未經「AI科技評論」授權,嚴禁以任何方式在網頁、論壇、社群進行轉載!
公眾號轉載請先在「AI科技評論」後臺留言取得授權,轉載時需標註來源並插入本公眾號名片。