首次證明了通過精巧的框架設(shè)計(jì)，AI有能力攻克需要深邃人類智慧的數(shù)學(xué)堡壘。

本文探討了當(dāng)前大語(yǔ)言模型（LLM）在自動(dòng)化定理證明（ATP）領(lǐng)域面臨的核心困境——強(qiáng)大的非形式化推理能力與孱弱的形式化證明能力之間的巨大鴻溝。為彌合這一鴻溝，我們提出了一種全新的“解耦推理與證明”框架。本研究由騰訊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

項(xiàng)目主頁(yè)及開源數(shù)據(jù)：https://tencent-imo.github.io/

01
背景與動(dòng)機(jī)：AI數(shù)學(xué)能力的巨大鴻溝

近年來，以大語(yǔ)言模型為代表的通用人工智能在數(shù)學(xué)推理領(lǐng)域取得了長(zhǎng)足進(jìn)步。然而，當(dāng)面對(duì)需要絕對(duì)邏輯嚴(yán)謹(jǐn)性的形式化數(shù)學(xué)證明時(shí)，AI的能力卻遭遇了瓶頸。這一現(xiàn)象揭示了當(dāng)前AI數(shù)學(xué)研究中的一個(gè)核心矛盾，也是其“阿喀琉斯之踵”：

在“思考”與“證明”之間，存在一道難以逾越的鴻溝。

最近在頂尖數(shù)學(xué)競(jìng)賽難題（如Putnam）上的大規(guī)模評(píng)測(cè)鮮明地印證了這一點(diǎn)：最強(qiáng)大的LLM（如Gemini 2.5 Pro）能夠以超過80%的準(zhǔn)確率生成非形式化的解題思路，展現(xiàn)出驚人的數(shù)學(xué)直覺與推理能力。然而，當(dāng)要求最先進(jìn)的形式化證明器（Prover）將這些思路轉(zhuǎn)化為機(jī)器可驗(yàn)證的嚴(yán)格證明時(shí)，成功率驟降至不足8%。

AI似乎成了一個(gè)“聰明的空想家”——它能想到解法，卻無法嚴(yán)格地證明它?，F(xiàn)有SOTA證明器（如DeepSeek-Prover-v2）試圖通過在單一模型內(nèi)融合“思考”（生成草稿）與“證明”（生成代碼）來解決此問題。但我們的研究發(fā)現(xiàn)，這種“耦合”設(shè)計(jì)存在根本性缺陷：它強(qiáng)迫強(qiáng)大的“思考者”去遷就能力有限的“證明者”，從而扼殺了AI真正的數(shù)學(xué)潛能。這正是為何即便是最前沿的模型，也始終未能攻克任何一道2000年后的國(guó)際數(shù)學(xué)奧林匹克（IMO）難題。

02
核心洞見：訓(xùn)練范式導(dǎo)致推理能力退化

為應(yīng)對(duì)這一挑戰(zhàn)，目前最前沿的工作（如DeepSeek-Prover-v2, Kimina）普遍采用一種“一體化”或“耦合式”的方案，即在單個(gè)模型內(nèi)部集成“思考草稿”與“形式化證明”兩個(gè)環(huán)節(jié)。它們?cè)噲D讓模型先生成高層思路，再據(jù)此產(chǎn)出形式化代碼。

然而，我們的研究發(fā)現(xiàn)，這種看似直觀的設(shè)計(jì)存在一個(gè)根本性的缺陷：它讓模型“帶著鐐銬跳舞”。具體而言，這種耦合架構(gòu)導(dǎo)致了兩個(gè)嚴(yán)重問題：

1.推理潛力被扼殺：模型的高層“思考”受到了其自身底層“證明”能力的嚴(yán)格束縛。為了確保后續(xù)能順利生成可通過驗(yàn)證的代碼，模型不敢提出那些真正具有創(chuàng)造性、但形式化難度較高的“奇招”，其所謂的“規(guī)劃”能力因此退化。

2.訓(xùn)練范式導(dǎo)致能力退化：這些模型普遍采用“可驗(yàn)證獎(jiǎng)勵(lì)的強(qiáng)化學(xué)習(xí)”（RLVR）進(jìn)行訓(xùn)練，即只根據(jù)最終代碼是否編譯成功來給予獎(jiǎng)勵(lì)。這種“成王敗寇”式的粗暴信號(hào)，實(shí)際上在鼓勵(lì)模型“走捷徑”——放棄深度的、復(fù)雜的邏輯構(gòu)建，轉(zhuǎn)而依賴ring, omega等自動(dòng)化“戰(zhàn)術(shù)”（tactics）進(jìn)行暴力嘗試。我們的實(shí)驗(yàn)首次定量證明：這種特化訓(xùn)練，會(huì)導(dǎo)致模型在通用數(shù)學(xué)推理（如MATH, AIME基準(zhǔn)）上的性能顯著下降，即為了“證明”，犧牲了“推理”。

3.這些問題共同導(dǎo)致了現(xiàn)有方法無法真正利用LLM那高達(dá)80%的推理潛力，在面對(duì)國(guó)際數(shù)學(xué)奧林匹克（IMO）等真正需要“靈光一閃”的難題時(shí)，屢戰(zhàn)屢敗。

03
解耦框架：讓“戰(zhàn)略家”與“精算師”各司其職

基于上述診斷，我們提出了一種全新的、基于“解耦 (Decoupling)”哲學(xué)的自動(dòng)化定理證明框架。我們認(rèn)為，與其強(qiáng)迫一個(gè)模型同時(shí)扮演好“戰(zhàn)略家”和“士兵”兩個(gè)角色，不如讓最優(yōu)秀的人才各司其職。我們的框架由兩個(gè)獨(dú)立的、可靈活調(diào)度的核心模塊構(gòu)成：

1.“推理器”（The Reasoner）：我們選用業(yè)界最強(qiáng)大的通用大模型（如GPT-4o, Gemini 1.5 Pro）作為推理器。它的唯一任務(wù)，就是不受任何形式化約束地進(jìn)行最高水平的戰(zhàn)略思考，提出解決問題的核心思路，并將其凝練成一系列關(guān)鍵的子目標(biāo)或引理（Lemmas）。這些引理是純粹的數(shù)學(xué)陳述，是連接高層智慧與底層邏輯的橋梁。

2.“證明器”（The Prover）：我們選用最高效的形式化證明模型（如DeepSeek-Prover-v2）作為證明器。它的任務(wù)是接收推理器提出的引理，并像一個(gè)專注的工匠一樣，逐一驗(yàn)證它們的正確性。

通過這種“戰(zhàn)略家出謀劃策，實(shí)干家驗(yàn)證執(zhí)行”的分工，我們的框架徹底解放了推理器的思考潛力，同時(shí)又通過證明器的嚴(yán)格驗(yàn)證保證了每一步的邏輯可靠性。

04
里程碑式的實(shí)驗(yàn)結(jié)果

我們?cè)谝幌盗袠O具挑戰(zhàn)性的、2000年后的IMO非幾何難題上驗(yàn)證了我們框架的有效性。結(jié)果是突破性的：

我們的框架成功解決了5道此前所有開源自動(dòng)化證明器均未能解決的IMO難題。包括：

lIMO 2000 Problem 2

lIMO 2005 Problem 3

lIMO 2011 Problem 3

lIMO 2019 Problem 1

lIMO 2020 Problem 2

這是AI在頂尖數(shù)學(xué)競(jìng)賽難題上取得的一次里程碑式的突破，首次證明了通過精巧的框架設(shè)計(jì)，AI有能力攻克需要深邃人類智慧的數(shù)學(xué)堡壘。

05
開源貢獻(xiàn)與總結(jié)

除了方法上的創(chuàng)新，我們深知推動(dòng)整個(gè)社區(qū)發(fā)展的重要性。為此，我們向公眾開源了本次研究的全部成果：

我們?yōu)榇罅緿eepSeek-Prover-V2 671B等模型無法獨(dú)立證明的IMO難題，提供了超過600條由我們的框架生成并成功驗(yàn)證的高質(zhì)量引理。我們相信，這個(gè)數(shù)據(jù)集將為后續(xù)工作解決更多IMO級(jí)別的難題提供一個(gè)堅(jiān)實(shí)的基礎(chǔ)，無論是對(duì)于AI研究者，還是對(duì)于人類數(shù)學(xué)家，都可能帶來新的啟發(fā)。

本研究首次系統(tǒng)性地揭示并解決了AI在形式化數(shù)學(xué)證明中“思考”與“證明”能力失衡的核心矛盾。我們提出的“解耦”框架，不僅在實(shí)踐中取得了前所未有的成果，也為未來構(gòu)建更強(qiáng)大、更具洞察力的人工智能系統(tǒng)提供了一條全新的、充滿希望的路徑。

總結(jié)

本研究由騰訊AI Lab完成。我們不僅提出了一個(gè)全新的、有效的自動(dòng)化定理證明框架，更重要的是，我們深刻揭示了當(dāng)前領(lǐng)域發(fā)展的核心矛盾，并為如何彌合“非形式化推理”與“形式化證明”之間的鴻溝提供了一條清晰可行的道路。通過將“思考的藝術(shù)”與“驗(yàn)證的科學(xué)”解耦，我們成功解決了5道頂尖IMO難題。

未經(jīng)「AI科技評(píng)論」授權(quán)，嚴(yán)禁以任何方式在網(wǎng)頁(yè)、論壇、社區(qū)進(jìn)行轉(zhuǎn)載！

公眾號(hào)轉(zhuǎn)載請(qǐng)先在「AI科技評(píng)論」后臺(tái)留言取得授權(quán)，轉(zhuǎn)載時(shí)需標(biāo)注來源并插入本公眾號(hào)名片。