12.1萬高難度數學題讓模型性能大漲，覆蓋FIMO/Putnam等頂級賽事難度，騰訊上海交大出品
12.1萬道IMO級難度數學“特訓題”，讓AI學會像人類一樣推導數學證明！
“特訓”過后，模型定理證明性能大漲，7B模型性能比肩或超越現有的開源模型和Claude3.7等商業模型。
“特訓題”為DeepTheorem，是首個基于自然語言的數學定理證明框架與數據集，由騰訊AI Lab與上海交大團隊聯合推出。
團隊表示，定理證明是數學前沿的重要組成部分，但當前大語言模型（LLM）在數學推理，特別是通過強化學習（RL）進行訓練時，往往需要可以自動驗證的答案，導致大模型無法像數學家那樣通過自然語言進行定理證明。
而當前研究者通常通過使用大模型生成Lean、Coq、Isabelle等形式語言，配合外部定理證明引擎進行定理證明，無法充分利用LLM在自然語言預訓練過程中獲得的能力。
為解決這一問題，DeepTheorem框架橫空出世，包含了從數據、訓練、測試到評估的完整四部分：
- 121K大規模、高難度、嚴格去污染的自然語言定理與o3-mini生成的配套證明過程
- 首個使用強化學習進行數學定理證明的方法
- 分別基于FIMO、HMMT、PutnamBench構建的三個自然語言定理證明測試集
- 涵蓋結果監督與過程監督的全面評價指標
如下圖（a）所示，DeepTheorem數據在規模和難度上均顯著超越目前已有的公開定理數據集。
圖（b）展示經過強化學習訓練的DeepTheorem-7B模型性能，比肩或超越現有的開源模型和商業模型（Gemini2.0-flash， Qwen2.5-72B-Instruct， Claude3.7等），僅次于o1、o3以及Gemini2.5-pro強推理模型。
DeepTheorem-121K
1、規模與難度：專為“極限挑戰”而生
DeepTheorem訓練集的顯著特點是其大規模與高難度。其包含121K精心構造的數學定理，難度等級為5-9級，規模顯著大于現有數學定理數據且難度更高，與FIMO等國際數學奧賽級別的測試集難度分布相似。
2、嚴格去污染：確保評估“純凈”
DeepTheorem訓練集的構建過程堪稱“匠心獨運”，通過一個細致的五階段流程構造：
來源分析與收集：分析現有數據來源，選擇難題比例高的數據源。
數據去污染：使用嵌入相似性搜索和LLM-Judge來識別并消除與MATH、AIME、GPQA等14個通用數學和STEM基準以及miniF2F、PutnamBench、FIMO等四個數學定理證明基準的重疊，確保評估的完整性并防止數據泄露。
證明生成與質量控制：使用o3-mini生成定理證明過程，并使用GPT-4o對定理完整性進行評估，保留定理與證明過程完整的樣本。
難度過濾：使用GPT-4o對定理進行難度評估，保留難度等級5或更高的定理。
單命題過濾：根據定理中的子命題個數進行篩選，保留僅含一個自命題的定理。
3、獨特結構：兼顧SFT與RL
DeepTheorem訓練集中的每條數據都包含豐富的信息，支持多種數學推理研究和應用：
- 問題：核心的數學定理陳述。
- 最終答案：定理的真值（真或假），這對于在可驗證獎勵強化學習（RLVR）中基于規則的獎勵函數至關重要，是自動化評估和反饋的基礎。
- 難度：數值難度標注，支持難度感知訓練。
- 主題：分層主題分類，涵蓋從初等代數到抽象代數、微積分的廣泛數學主題。
- o3-mini證明過程：由o3-mini模型生成的證明過程，對于監督微調和模型蒸餾等多種訓練范式都具有巨大價值。
將RL-Zero引入數學定理證明
1、數據增強：定理可以被證明，也可以被證偽
為將可驗證獎勵強化學習（RLVR）引入自然語言數學定理證明，DeepTheorem通過自動化的方法來對每個原始定理進行擴展，衍生出多個可被證明或證偽的變體。
以定理“x>1”為例，若該定理成立，則變體一“x>0”也一定成立，而變體二“x<1”則一定不成立。通過這種方式，DeepTheorem僅基于定理本身（而不需要接觸證明過程）使用大模型對訓練集中的所有定理進行擴展，獲得242K定理及變體。
2、二值獎勵激發定理證明能力
在獲得定理變體后，DeepTheorem使用基于GRPO的RLVR進行定理證明訓練。對于訓練集中的每一個定理，模型的任務是將其證明或證偽，并在最終答案中給出判斷（證明或證偽）。
基于規則的獎勵函數根據模型最終答案進行打分，若答案正確則得一分，若無法提取答案或答案錯誤則得0分。
DeepTheorem評估框架
1、DeepTheorem測試集
在經過對問題難度、污染程度、數據可用性等多方面因素的綜合考慮后，作者們選擇了兩個現有的定理證明測試集FIMO與PutnamBench，并從當前污染較少的HMMT測試集中手工篩出了定理證明相關題目，構成三個自然語言定理證明測試集。
模仿對訓練數據中的定理進行數據增強的方式，DeepTheorem的作者們對這三個測試集中的每個定理手工擴展出了多個變體，構成最終測試集：
最終測試集中，平均每個定理包含約三個變體，三個測試集總變體數658個。
2、結果與過程評價指標
在DeepTheorem測試集上，模型性能由兩部分評價指標構成：結果評價與過程評價。
結果評價的指標定義為：對每一個原始定理，若模型成功將其全部變體證明或證偽則得1分，否則得0分。基于此定義，我們可以對每個變體隨機賦予“證明”或“證偽”的答案獲得隨機基線。此基線在三個測試集上的性能如上表Random Acc.列所示。
過程評價使用LLM-as-Judge，由GPT-4o從邏輯正確性、完整性、最終答案正確性以及過程清晰性四個維度對證明過程進行打分。
DeepTheorem模型性能達到SOTA
實驗結果表明，在DeepTheorem數據集上使用RL-Zero基于Qwen2.5-7B訓練的模型擁有同規模模型中的SOTA性能。
顯著優于DeepSeek-Prover等參數量相近的現有定理證明模型以及Qwen2.5-Math-72B等更大的模型，甚至比肩Claude3.7-Sonnet等閉源模型，在所評測的18個模型中性能排名第五，僅次于o1系列、o3-mini以及Gemini 2.5 Pro。
以下為DeepTheorem-RL-7B在測試集上隨機挑選的輸出樣本。模型在證明過程中展現出了清晰準確的邏輯性，且僅使用Latex，簡潔易懂。
團隊表示，DeepTheorem框架的發布，無疑為人工智能在數學推理領域的應用開辟了全新的思路，它不僅突破了使用形式語言進行定理證明的傳統范式限制，更通過其大規模、高質量的訓練數據提升了AI在前沿數學方面的卓越性能。
我們期待，在DeepTheorem的推動下，AI能夠真正學會定理證明，從封閉的計算、簡答題目走向更廣闊的數學殿堂，最終邁向更強大、更具通用性、認知上更復雜的智能系統。
團隊簡介
本文通訊作者徐嘉豪， 騰訊AI Lab高級研究員，研究方向為推理大模型，在NIPS，ACL，EMNLP等國際頂級會議上發表多篇論文。
共同通訊作者涂兆鵬，騰訊混元數字人專家研究員，研究方向為深度學習和大模型，在國際頂級期刊和會議上發表學術論文一百余篇，多次擔任ACL、EMNLP、ICLR等國際頂級會議領域主席。
共同通訊作者王瑞，上海交通大學副教授，研究方向為計算語言學。
第一作者為上海交通大學博士生張子殷。
論文地址：https://arxiv.org/abs/2505.23754
