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

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

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

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

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

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

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

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

這種不匹配就像要求一個(gè)熟悉中餐烹飪的廚師突然制作精致的法式甜點(diǎn)，而且不允許他查看食譜——即使他有出色的烹飪天賦，也會(huì)因?yàn)楣ぞ吆图记傻牟町惗憩F(xiàn)不佳。同樣，當(dāng)語言模型被迫使用形式化語言進(jìn)行定理證明時(shí)，它們的真實(shí)能力受到了嚴(yán)重限制。

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

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

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

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

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

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

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

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

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

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

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

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

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

三、通過強(qiáng)化學(xué)習(xí)進(jìn)行定理證明：突破傳統(tǒng)限制

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

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

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

**可驗(yàn)證獎(jiǎng)勵(lì)的定理變體**

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

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

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

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

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

**二元獎(jiǎng)勵(lì)激活定理證明生成**

有了上述定理變體，研究團(tuán)隊(duì)現(xiàn)在可以將強(qiáng)化學(xué)習(xí)應(yīng)用于自然語言定理證明。具體來說，他們采用了GRPO算法。

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

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

**評(píng)估方法**

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

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

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

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

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

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

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

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

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

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

**與最先進(jìn)模型的比較**

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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