12.1萬道IMO級難度數(shù)學“特訓題”，讓AI學會像人類一樣推導數(shù)學證明！

“特訓”過后，模型定理證明性能大漲，7B模型性能比肩或超越現(xiàn)有的開源模型和Claude3.7等商業(yè)模型。

“特訓題”為DeepTheorem，是首個基于自然語言的數(shù)學定理證明框架與數(shù)據(jù)集，由騰訊AI Lab與上海交大團隊聯(lián)合推出。

團隊表示，定理證明是數(shù)學前沿的重要組成部分，但當前大語言模型（LLM）在數(shù)學推理，特別是通過強化學習（RL）進行訓練時，往往需要可以自動驗證的答案，導致大模型無法像數(shù)學家那樣通過自然語言進行定理證明。

而當前研究者通常通過使用大模型生成Lean、Coq、Isabelle等形式語言，配合外部定理證明引擎進行定理證明，無法充分利用LLM在自然語言預訓練過程中獲得的能力。

為解決這一問題，DeepTheorem框架橫空出世，包含了從數(shù)據(jù)、訓練、測試到評估的完整四部分：

• 121K大規(guī)模、高難度、嚴格去污染的自然語言定理與o3-mini生成的配套證明過程
• 首個使用強化學習進行數(shù)學定理證明的方法
• 分別基于FIMO、HMMT、PutnamBench構建的三個自然語言定理證明測試集
• 涵蓋結果監(jiān)督與過程監(jiān)督的全面評價指標

如下圖（a）所示，DeepTheorem數(shù)據(jù)在規(guī)模和難度上均顯著超越目前已有的公開定理數(shù)據(jù)集。

圖（b）展示經(jīng)過強化學習訓練的DeepTheorem-7B模型性能，比肩或超越現(xiàn)有的開源模型和商業(yè)模型（Gemini2.0-flash， Qwen2.5-72B-Instruct， Claude3.7等），僅次于o1、o3以及Gemini2.5-pro強推理模型。

DeepTheorem-121K

1、規(guī)模與難度：專為“極限挑戰(zhàn)”而生

DeepTheorem訓練集的顯著特點是其大規(guī)模與高難度。其包含121K精心構造的數(shù)學定理，難度等級為5-9級，規(guī)模顯著大于現(xiàn)有數(shù)學定理數(shù)據(jù)且難度更高，與FIMO等國際數(shù)學奧賽級別的測試集難度分布相似。

2、嚴格去污染：確保評估“純凈”

DeepTheorem訓練集的構建過程堪稱“匠心獨運”，通過一個細致的五階段流程構造：

來源分析與收集：分析現(xiàn)有數(shù)據(jù)來源，選擇難題比例高的數(shù)據(jù)源。

數(shù)據(jù)去污染：使用嵌入相似性搜索和LLM-Judge來識別并消除與MATH、AIME、GPQA等14個通用數(shù)學和STEM基準以及miniF2F、PutnamBench、FIMO等四個數(shù)學定理證明基準的重疊，確保評估的完整性并防止數(shù)據(jù)泄露。

證明生成與質量控制：使用o3-mini生成定理證明過程，并使用GPT-4o對定理完整性進行評估，保留定理與證明過程完整的樣本。

難度過濾：使用GPT-4o對定理進行難度評估，保留難度等級5或更高的定理。

單命題過濾：根據(jù)定理中的子命題個數(shù)進行篩選，保留僅含一個自命題的定理。

3、獨特結構：兼顧SFT與RL

DeepTheorem訓練集中的每條數(shù)據(jù)都包含豐富的信息，支持多種數(shù)學推理研究和應用：

• 問題：核心的數(shù)學定理陳述。
• 最終答案：定理的真值（真或假），這對于在可驗證獎勵強化學習（RLVR）中基于規(guī)則的獎勵函數(shù)至關重要，是自動化評估和反饋的基礎。
• 難度：數(shù)值難度標注，支持難度感知訓練。
• 主題：分層主題分類，涵蓋從初等代數(shù)到抽象代數(shù)、微積分的廣泛數(shù)學主題。
• o3-mini證明過程：由o3-mini模型生成的證明過程，對于監(jiān)督微調和模型蒸餾等多種訓練范式都具有巨大價值。

將RL-Zero引入數(shù)學定理證明

1、數(shù)據(jù)增強：定理可以被證明，也可以被證偽

為將可驗證獎勵強化學習（RLVR）引入自然語言數(shù)學定理證明，DeepTheorem通過自動化的方法來對每個原始定理進行擴展，衍生出多個可被證明或證偽的變體。

以定理“x>1”為例，若該定理成立，則變體一“x>0”也一定成立，而變體二“x<1”則一定不成立。通過這種方式，DeepTheorem僅基于定理本身（而不需要接觸證明過程）使用大模型對訓練集中的所有定理進行擴展，獲得242K定理及變體。

2、二值獎勵激發(fā)定理證明能力

在獲得定理變體后，DeepTheorem使用基于GRPO的RLVR進行定理證明訓練。對于訓練集中的每一個定理，模型的任務是將其證明或證偽，并在最終答案中給出判斷（證明或證偽）。

基于規(guī)則的獎勵函數(shù)根據(jù)模型最終答案進行打分，若答案正確則得一分，若無法提取答案或答案錯誤則得0分。

DeepTheorem評估框架

1、DeepTheorem測試集

在經(jīng)過對問題難度、污染程度、數(shù)據(jù)可用性等多方面因素的綜合考慮后，作者們選擇了兩個現(xiàn)有的定理證明測試集FIMO與PutnamBench，并從當前污染較少的HMMT測試集中手工篩出了定理證明相關題目，構成三個自然語言定理證明測試集。

模仿對訓練數(shù)據(jù)中的定理進行數(shù)據(jù)增強的方式，DeepTheorem的作者們對這三個測試集中的每個定理手工擴展出了多個變體，構成最終測試集：

最終測試集中，平均每個定理包含約三個變體，三個測試集總變體數(shù)658個。

2、結果與過程評價指標

在DeepTheorem測試集上，模型性能由兩部分評價指標構成：結果評價與過程評價。

結果評價的指標定義為：對每一個原始定理，若模型成功將其全部變體證明或證偽則得1分，否則得0分。基于此定義，我們可以對每個變體隨機賦予“證明”或“證偽”的答案獲得隨機基線。此基線在三個測試集上的性能如上表Random Acc.列所示。

過程評價使用LLM-as-Judge，由GPT-4o從邏輯正確性、完整性、最終答案正確性以及過程清晰性四個維度對證明過程進行打分。

DeepTheorem模型性能達到SOTA

實驗結果表明，在DeepTheorem數(shù)據(jù)集上使用RL-Zero基于Qwen2.5-7B訓練的模型擁有同規(guī)模模型中的SOTA性能。

顯著優(yōu)于DeepSeek-Prover等參數(shù)量相近的現(xiàn)有定理證明模型以及Qwen2.5-Math-72B等更大的模型，甚至比肩Claude3.7-Sonnet等閉源模型，在所評測的18個模型中性能排名第五，僅次于o1系列、o3-mini以及Gemini 2.5 Pro。

以下為DeepTheorem-RL-7B在測試集上隨機挑選的輸出樣本。模型在證明過程中展現(xiàn)出了清晰準確的邏輯性，且僅使用Latex，簡潔易懂。

團隊表示，DeepTheorem框架的發(fā)布，無疑為人工智能在數(shù)學推理領域的應用開辟了全新的思路，它不僅突破了使用形式語言進行定理證明的傳統(tǒng)范式限制，更通過其大規(guī)模、高質量的訓練數(shù)據(jù)提升了AI在前沿數(shù)學方面的卓越性能。

我們期待，在DeepTheorem的推動下，AI能夠真正學會定理證明，從封閉的計算、簡答題目走向更廣闊的數(shù)學殿堂，最終邁向更強大、更具通用性、認知上更復雜的智能系統(tǒng)。

團隊簡介

本文通訊作者徐嘉豪， 騰訊AI Lab高級研究員，研究方向為推理大模型，在NIPS，ACL，EMNLP等國際頂級會議上發(fā)表多篇論文。

共同通訊作者涂兆鵬，騰訊混元數(shù)字人專家研究員，研究方向為深度學習和大模型，在國際頂級期刊和會議上發(fā)表學術論文一百余篇，多次擔任ACL、EMNLP、ICLR等國際頂級會議領域主席。

共同通訊作者王瑞，上海交通大學副教授，研究方向為計算語言學。

第一作者為上海交通大學博士生張子殷。

論文地址：https://arxiv.org/abs/2505.23754

數(shù)據(jù)地址：https://huggingface.co/datasets/Jiahao004/DeepTheorem

代碼地址：https://github.com/Jiahao004/DeepTheorem