在機器智能的歷史長河中，數(shù)學定理證明一直是檢驗人工智能系統(tǒng)推理能力的終極試金石。2025年5月29日，來自騰訊和上海交通大學的研究團隊在arXiv上發(fā)表了題為《DeepTheorem: 通過自然語言和強化學習推進大型語言模型的定理證明推理》的研究論文，為這一領(lǐng)域帶來了重要突破。這項由張子寅、徐嘉浩（通訊作者）、何志偉等研究人員主導的工作，提出了一種全新的非形式化定理證明框架，該論文已發(fā)布在GitHub (https://github.com/Jiahao004/DeepTheorem) 和Hugging Face (https://huggingface.co/datasets/Jiahao004/DeepTheorem)上。

想象一下數(shù)學家如何證明定理：他們通常使用自然語言和數(shù)學符號，在草稿紙上勾畫思路，逐步形成嚴謹?shù)耐评礞?。而傳統(tǒng)的自動化定理證明系統(tǒng)卻要求使用非常嚴格的形式化語言，如Lean、Coq或Isabelle這樣的證明助手系統(tǒng)，這與大型語言模型（LLMs）在預訓練階段學到的知識類型存在巨大鴻溝。這就像強迫一個在中文環(huán)境長大的人突然用古希臘語寫詩一樣困難。

DeepTheorem項目就像是在搭建一座橋梁，讓語言模型能夠用它們最擅長的方式——自然語言——來進行數(shù)學定理證明。研究團隊構(gòu)建了一個包含12.1萬個高質(zhì)量非形式化定理和證明的大規(guī)模數(shù)據(jù)集，這些定理難度可媲美國際數(shù)學奧林匹克（IMO）水平。更令人興奮的是，他們開發(fā)了一種創(chuàng)新的強化學習策略（RL-Zero），專門針對非形式化定理證明進行優(yōu)化。

簡單來說，這項研究就像是教會了AI用"人類數(shù)學家的思維方式"而非"計算機程序員的思維方式"來解決復雜的數(shù)學問題。接下來，讓我們深入了解這項突破性工作的細節(jié)，看看它如何改變AI數(shù)學推理的未來。

一、為什么定理證明對大型語言模型如此重要？

想象你正在教一個孩子學習數(shù)學。一開始，你可能會教他簡單的加減法；隨著他的成長，你會引入更復雜的概念，如代數(shù)和幾何。最終，當他能夠證明復雜的數(shù)學定理時，你才會說他真正掌握了數(shù)學推理能力。類似地，定理證明已成為評估人工智能系統(tǒng)推理能力的"奧林匹克比賽"。

在人工智能領(lǐng)域，定理證明被視為檢驗復雜推理能力的最高標準之一。它要求AI同時掌握抽象思維、戰(zhàn)略推理、模式識別和精確的邏輯推導能力。近年來，隨著深度學習特別是大型語言模型（LLMs）的進步，自動化定理證明（ATP）領(lǐng)域發(fā)生了翻天覆地的變化。

然而，傳統(tǒng)的ATP方法面臨一個根本性問題：它們主要依賴Lean、Coq和Isabelle等形式化證明系統(tǒng)，或來自ProofWiki的特定領(lǐng)域語言。這些系統(tǒng)要求使用高度結(jié)構(gòu)化、嚴格的形式語言，而這與大型語言模型在預訓練過程中接觸到的自然語言和LaTeX數(shù)學文本有著本質(zhì)區(qū)別。

這種不匹配就像要求一個熟悉中餐烹飪的廚師突然制作精致的法式甜點，而且不允許他查看食譜——即使他有出色的烹飪天賦，也會因為工具和技巧的差異而表現(xiàn)不佳。同樣，當語言模型被迫使用形式化語言進行定理證明時，它們的真實能力受到了嚴重限制。

騰訊和上交大的研究團隊意識到，如果想要充分發(fā)揮大型語言模型在數(shù)學推理方面的潛力，必須創(chuàng)建一個與它們預訓練知識相匹配的框架。這就是DeepTheorem項目的核心理念：不是強迫語言模型適應形式化證明系統(tǒng)，而是設(shè)計一個框架，讓它們能夠使用自然語言進行數(shù)學推理，就像人類數(shù)學家那樣。

研究團隊的方法包含三個關(guān)鍵要素：首先，構(gòu)建一個大規(guī)模的非形式化定理證明數(shù)據(jù)集；其次，開發(fā)一種專門針對非形式化定理證明的強化學習策略；最后，設(shè)計全面的評估指標來衡量證明的正確性和推理過程的質(zhì)量。

這種自然語言驅(qū)動的方法不僅更符合語言模型的預訓練知識，還提供了更大的靈活性和可擴展性。它允許AI系統(tǒng)采用更接近人類數(shù)學家的啟發(fā)式思維方式，而不是受限于嚴格的形式化規(guī)則。

二、DeepTheorem數(shù)據(jù)集：為何它如此與眾不同？

想象你正在教一個學生學習烹飪。你可以給他一本只有幾道簡單菜譜的食譜書，或者提供一本包含成百上千種不同難度和風格菜肴的百科全書式烹飪指南。顯然，后者能讓學生接觸到更廣泛的技巧和知識。DeepTheorem數(shù)據(jù)集就像是這樣一本全面的"數(shù)學烹飪指南"，涵蓋了從基礎(chǔ)數(shù)學"菜肴"到高級"大師級配方"的各種定理。

DeepTheorem數(shù)據(jù)集包含約12.1萬個經(jīng)過精心挑選的非形式化數(shù)學定理和高質(zhì)量證明，其規(guī)模遠超現(xiàn)有的類似數(shù)據(jù)集。如圖1(a)所示，DeepTheorem的規(guī)模明顯超過了Lean-Workbook、Deepseek-Prover-v1的訓練語料庫和OpenR1-Math中的定理。

但這個數(shù)據(jù)集的價值不僅僅在于它的規(guī)模。以下幾個特點讓它在數(shù)學推理訓練資源中脫穎而出：

首先，DeepTheorem的每一條數(shù)據(jù)都像一幅完整的畫卷，包含定理本身、相應的證明、正確性標簽（真或假）、難度評分（例如，1到10分的精細難度評分）和主題分類（如數(shù)論、幾何等）。這就像每道菜譜不僅告訴你材料和步驟，還標明了難度級別、烹飪風格和可能的變化。

其次，這些定理的難度水平非常高，大多集中在6-9級（滿分10級），與國際數(shù)學奧林匹克（IMO）級別的挑戰(zhàn)相當。如圖3所示，DeepTheorem在高難度定理上的比例遠高于其他數(shù)據(jù)集，這使它能夠真正挑戰(zhàn)和提升AI系統(tǒng)的數(shù)學推理能力。

第三，數(shù)據(jù)集的主題覆蓋面非常廣泛。如圖4所示，DeepTheorem涵蓋了代數(shù)、離散數(shù)學、應用數(shù)學、微積分、幾何、數(shù)學分析、數(shù)論等眾多數(shù)學領(lǐng)域。這種多樣性確保了訓練出的模型不會只擅長特定類型的數(shù)學問題，而是能夠處理整個數(shù)學領(lǐng)域的各種挑戰(zhàn)。

第四，DeepTheorem經(jīng)過嚴格的除污處理，避免與廣泛使用的基準測試集重疊。研究團隊實施了一個嚴格的三步流程：首先使用嵌入模型生成所有定理語句的句子嵌入；然后計算訓練樣本與所有測試樣本的嵌入余弦相似度；最后使用GPT-4o評估召回的測試樣本是否在當前訓練樣本中被污染。這個過程移除了約19.9萬個污染樣本，有效識別了相同案例、泛化問題和逆定理。

最后，數(shù)據(jù)集中的證明由o3-mini生成，經(jīng)過了精心調(diào)整，專為監(jiān)督微調(diào)（SFT）量身定制。這些證明提供了完成證明所需邏輯步驟的簡潔而完整的概述，以清晰和簡潔為重點。這些用LaTeX表達的證明與LLM的非形式化性質(zhì)相一致，使它們成為有效的學習信號。

構(gòu)建這個龐大數(shù)據(jù)集的過程也十分復雜。如圖5所示，研究團隊從多個來源聚合原始數(shù)據(jù)，包括MMIQC、WebInstruct和NuminaMath-CoT。然后通過一系列處理步驟，包括除污、質(zhì)量控制、證明生成、邏輯驗證、難度標注和單一語句過濾，最終得到了121K高質(zhì)量的挑戰(zhàn)性定理。

三、通過強化學習進行定理證明：突破傳統(tǒng)限制

傳統(tǒng)上，非形式化定理證明數(shù)據(jù)集主要通過監(jiān)督微調(diào)（SFT）來使用，AI模型通過模仿數(shù)據(jù)集中的例子來學習生成證明。然而，最近關(guān)于RL-Zero的研究表明，這種方法可以通過利用基礎(chǔ)模型的預訓練知識和探索能力在SFT之上取得更好的性能。

這就引出了一個自然的問題：我們能否利用基礎(chǔ)模型的探索能力來進行非形式化定理證明？研究團隊探索了將RL-Zero應用于非形式化定理證明的可能性，并取得了令人矚目的成果。

整個過程可以分為三個關(guān)鍵步驟：1）數(shù)據(jù)增強，生成用于二元獎勵的矛盾定理變體；2）使用GRPO算法進行RL-Zero訓練；3）評估定理-證明生成。

**可驗證獎勵的定理變體**

為了構(gòu)建適用于RL-Zero的帶獎勵的定理，研究團隊做出了一個關(guān)鍵觀察：定理陳述不必是正確的，也可以被證明是錯誤的，這使得可以構(gòu)建一個與RL-Zero兼容的二元獎勵結(jié)構(gòu)。

這一發(fā)現(xiàn)允許他們將DeepTheorem的定理轉(zhuǎn)化為真或假的變體，促進強化學習訓練，鼓勵穩(wěn)健的推理。具體來說，研究團隊使用LLM擴展原始定理為可以被反駁的矛盾變體。

例如，考慮下面三個定理變體（為簡潔起見省略假設(shè)）： - 原始定理：x > 1 - 變體1：x > 0 - 變體2：x < 1

如果原始定理可以被證明，變體1也是正確的，可以用與原始定理相同的方式進行數(shù)學證明，而變體2必然是錯誤的，可以被反駁。

通過這種邏輯上蘊含或矛盾的轉(zhuǎn)換，研究團隊能夠構(gòu)建保證正確或錯誤的定理變體，而只需訪問定理本身而不是證明過程。這使得這個轉(zhuǎn)換任務(wù)比注釋新的數(shù)學陳述要容易得多，從而允許相對較弱的LLM（如Qwen2.5-72B-Instruct）來執(zhí)行它。經(jīng)過這個擴展階段，研究團隊進一步注釋了結(jié)果定理池的完整性，最終獲得了一個包含24.2萬個數(shù)學定理的訓練集，這些定理可以被證明或反駁，每個都有完整的證明軌跡。

**二元獎勵激活定理證明生成**

有了上述定理變體，研究團隊現(xiàn)在可以將強化學習應用于自然語言定理證明。具體來說，他們采用了GRPO算法。

受到R1等推理專用模型成功的啟發(fā)，研究團隊在系統(tǒng)提示中鼓勵模型在 標簽中封閉其推理過程，以激勵更詳細的推理行為，然后要求模型以"\boxed{proved}"或"\boxed{disproved}"結(jié)束每個證明。在獎勵函數(shù)中，他們提取這個答案并將其與真實情況進行比較，如果答案匹配則給予1的獎勵，否則給予0。

他們還強制執(zhí)行幾項健全性檢查以防止模型崩潰：如果模型解決方案中的空白比例低于0.05或平均字符重復計數(shù)大于300，則無論答案如何都會發(fā)出0的獎勵。

**評估方法**

用于評估的定理證明問題來自兩個具有挑戰(zhàn)性的基準測試——FIMO和Putnam——以及新構(gòu)建的HMMT定理證明子集。研究團隊手動擴展了這三個數(shù)據(jù)源中的每個問題，生成多個蘊含或矛盾的變體，結(jié)果基準如表3所示。

對于結(jié)果評估，研究團隊提出了一個新穎的評估框架，利用從每個定理派生的多個蘊含和矛盾變體。通過評估模型在這些變體上一致分配正確真值的能力，他們間接估計了其定理證明能力。當變體數(shù)量足夠大時，這種方法為評估非形式化證明的正確性提供了一個穩(wěn)健的代理。

對于過程評估，研究團隊開發(fā)了一個框架，評估證明質(zhì)量的四個維度： - 邏輯有效性：檢查每一步是否從前一步邏輯上推導出來 - 完整性：驗證是否包含證明定理所需的所有必要情況和步驟 - 正確性：確認最終結(jié)論是否正確 - 清晰度：評估證明是否清晰、明確和解釋得當

四、實驗結(jié)果：DeepTheorem如何改變游戲規(guī)則？

研究團隊進行了一系列實驗，以評估DeepTheorem數(shù)據(jù)集和RL-Zero訓練方法的有效性。他們訓練了兩組模型，一組使用監(jiān)督微調(diào)（SFT），另一組使用零強化學習（RL-Zero），兩組都從Qwen2.5-Base開始。

對于SFT，他們在數(shù)據(jù)集中的完整證明解決方案上訓練模型3個周期。對于RL-Zero，他們采用GRPO算法，批量大小為128，組大小為64，最大推出長度為8192。他們訓練模型1000步，并在訓練期間將每個模型分布在兩臺機器上。

作為基線，他們選擇了OpenR1-Math的定理證明子集，這是現(xiàn)有的最高質(zhì)量定理證明數(shù)據(jù)集，具有完整的問題和回答。他們對其應用與2.1節(jié)詳述的相同處理流程，這產(chǎn)生了總共66K原始定理和130K變體。

**主要結(jié)果**

如表4所示，DeepTheorem在OpenR1-Math-Proof上展示了優(yōu)越的性能，特別是對于7B骨干和過程評估方面。另一方面，RL-Zero訓練范式始終優(yōu)于SFT，驗證了RL-Zero在推動模型的推理能力超越SFT限制方面的有效性。

特別令人印象深刻的是，在7B模型上使用DeepTheorem進行RL訓練（稱為DeepTheorem-RL-7B）在FIMO基準上達到了55.56%的準確率，在HMMT基準上達到了28.81%的準確率，在Putnam基準上達到了57.29%的準確率。這些結(jié)果顯著優(yōu)于使用相同架構(gòu)但用OpenR1-Proof訓練的模型。

**與最先進模型的比較**

在表5中，研究團隊還提供了最先進LLM在三個基準上的評估結(jié)果。這些結(jié)果表明，定理證明，特別是他們新構(gòu)建的HMMT基準，對LLM仍然是相當具有挑戰(zhàn)性的。另一方面，他們的7B模型，用DeepTheorem上的RL-Zero訓練，優(yōu)于大得多的SOTA模型，包括那些專門用于數(shù)學和推理的模型，展示了DeepTheorem和他們創(chuàng)新的結(jié)果監(jiān)督RL訓練方法對定理證明的卓越質(zhì)量。

**參數(shù)效率**

圖7展示了DeepTheorem-RL策略如何實現(xiàn)強大的參數(shù)效率。與作為骨干模型的Qwen2.5系列相比，在1.5到7B模型上訓練DeepTheorem顯著提高了參數(shù)-性能空間中的非形式化定理證明邊界。此外，DeepTheorem參數(shù)效率也超過了SOTA商業(yè)模型，如o1和o3-mini。

**分析：RL-Zero與DeepTheorem激活骨干模型的定理證明能力**

為了更深入地理解DeepTheorem-RL訓練模型的能力，研究團隊提供了一個案例研究，分析了由其模型生成的證明。他們選擇了一個涉及多項式和固定點的復雜問題。模型成功地識別了問題的核心，正確地分析了Q(x)的性質(zhì)（它是P應用k次的結(jié)果），并準確地推斷出Q(x)不可能有超過n個整數(shù)固定點。

該證明展示了模型在處理復雜的多項式組合和理解迭代性質(zhì)方面的能力，突顯了它對這類問題的深刻理解。該模型正確地識別了關(guān)鍵觀察點，即整數(shù)固定點的數(shù)量受到多項式預周期點數(shù)量的限制，并基于此得出正確的結(jié)論。

在圖8中，研究團隊還可視化了他們的7B模型在DeepTheorem上進行RL訓練時使用的證明技術(shù)分布。直接證明最常用，其次是窮舉證明和構(gòu)造證明。這表明模型已經(jīng)學會了應用多種證明策略，適應不同類型的數(shù)學問題。

五、結(jié)論：DeepTheorem如何改變AI數(shù)學推理的未來？

歸根結(jié)底，DeepTheorem項目代表了AI數(shù)學推理領(lǐng)域的重要里程碑。通過創(chuàng)建一個利用自然語言進行數(shù)學推理的框架，研究團隊成功解決了傳統(tǒng)ATP方法與大型語言模型預訓練知識之間的不匹配問題。

這項工作的核心貢獻包括： - 一個包含12.1萬個IMO級別非形式化數(shù)學定理和相應高質(zhì)量證明的大規(guī)模自然語言數(shù)據(jù)集，這些定理經(jīng)過系統(tǒng)標注，包括正確性、難度、主題多樣性，并包含適用于高級強化學習的可驗證定理變體。 - 一種專門為非形式化定理證明設(shè)計的新型RL-Zero訓練方法，顯著增強了LLM的推理能力，超越了傳統(tǒng)SFT方法。 - 全面的評估框架，評估定理證明的正確性（結(jié)果評估）和生成的推理過程的完整性、邏輯有效性和正確性（過程評估）。

通過廣泛的實驗，研究團隊確立了DeepTheorem范式的優(yōu)越性，實現(xiàn)了最先進的性能，超越了現(xiàn)有的非形式化定理數(shù)據(jù)集和訓練方法。

這項研究的意義遠遠超出了數(shù)學領(lǐng)域。通過改進AI系統(tǒng)進行復雜推理的能力，DeepTheorem為更廣泛的問題解決應用鋪平了道路。隨著AI系統(tǒng)變得越來越擅長數(shù)學推理，我們可以期待它們在科學發(fā)現(xiàn)、工程優(yōu)化和其他需要嚴格邏輯思維的領(lǐng)域做出更大貢獻。

對于普通人來說，這項研究的意義在于，它使AI系統(tǒng)更接近于以人類可以理解和驗證的方式解決復雜問題。通過使用自然語言而非形式化語言，DeepTheorem創(chuàng)建的AI系統(tǒng)將更容易與人類協(xié)作，可能成為從學生到研究人員等各類用戶的強大工具。

未來的研究方向可能包括將DeepTheorem框架擴展到其他推理領(lǐng)域，開發(fā)更先進的非形式化證明驗證技術(shù)，以及探索如何將自然語言證明與形式化證明系統(tǒng)結(jié)合起來，獲得兩者的優(yōu)勢。

對于那些想要深入了解這項研究的讀者，完整論文可在arXiv上獲取，代碼和數(shù)據(jù)集可通過GitHub和Hugging Face訪問。隨著這些資源的公開，我們期待看到社區(qū)如何構(gòu)建和擴展這項開創(chuàng)性工作。