首次證明了透過精巧的框架設計，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）。這些引理是純粹的數學陳述，是連線高層智慧與底層邏輯的橋樑。