超越DeepSeek-R1，數(shù)學形式化準確率飆升至84% | 字節(jié)&南大開源

CriticLean 團隊 投稿
量子位 | 公眾號 QbitAI

當人工智能已經(jīng)能下圍棋、寫代碼，如何讓機器理解并證明數(shù)學定理，仍是橫亙在科研界的重大難題。

字節(jié)跳動Seed團隊與南京大學聯(lián)合發(fā)布CriticLean框架，一舉將數(shù)學自然語言到Lean 4代碼的形式化準確率從38%提升至84%。

該框架創(chuàng)新性地將評估模型置于核心位置。通過強化學習訓練的CriticLeanGPT模型，能像數(shù)學專家一樣精準判斷形式化代碼是否貼合原始語義，配合迭代優(yōu)化機制，讓生成的定理證明既符合語法規(guī)范，又忠實于數(shù)學邏輯。

?前論?和數(shù)據(jù)代碼倉庫均已對外公開，歡迎開源使用。

數(shù)學形式化領域的核心挑戰(zhàn)

將自然語言描述的數(shù)學命題轉化為機器可驗證的形式化代碼（如Lean 4定理），是自動化定理證明領域的基礎性難題，其核心挑戰(zhàn)不僅在于語法層面的準確轉換，更在于對數(shù)學語義的深度理解與忠實還原。

盡管現(xiàn)有研究在生成模型與編譯有效性上取得一定進展，但在復雜問題的語義對齊上仍存在顯著瓶頸，具體體現(xiàn)在以下三方面：

• 語義鴻溝：
• 自然語言數(shù)學命題的隱含條件等難精準映射為形式邏輯，易出現(xiàn)前提翻譯偏差等問題，過往方法因缺語義一致性校驗，導致大量邏輯錯誤的形式化結果。
• 評價缺位：
• 對形式化結果的評價依賴編譯檢查或 LLM 簡單判斷，存在錯誤類型覆蓋不全、評價可靠性不足的問題，難以識別邏輯矛盾等。
• 數(shù)據(jù)瓶頸：
• 現(xiàn)有數(shù)學形式化數(shù)據(jù)集規(guī)模和多樣性不足、難度分布單一、語義校驗缺失，制約了模型應對復雜數(shù)學命題的能力。

引入Critic角色以實現(xiàn)可靠形式化

上述挑戰(zhàn)的核心在于：形式化流程中“評價”與“生成”的割裂。

CriticLean框架將引入強化學習的 Critic 模型，通過訓練專門的語義評價模型（CriticLeanGPT）、結合 Lean 4 編譯器反饋進行迭代生成。系統(tǒng)性解決語義對齊、評價可靠性與數(shù)據(jù)質量問題，為數(shù)學自動化形式化提供了全新范式。

圖1：CriticLean框架通過編譯器與評估器的雙重反饋，實現(xiàn)數(shù)學形式化的迭代優(yōu)化

CriticLeanGPT：會“挑錯”的數(shù)學評估專家

團隊基于Qwen2.5和Qwen3系列模型，通過兩步訓練打造專業(yè)評估器：

• 有監(jiān)督微調(diào)（SFT）
• ：在4.8萬條包含：數(shù)學、代碼以及數(shù)學語句-形式化代碼對一致性相關的Critic數(shù)據(jù)CriticLeanInstruct數(shù)據(jù)集上訓練，增強其針對語義判斷的評估能力。
• 強化學習優(yōu)化（RL）
• ：采用GRPO算法，以“判斷是否準確”和“輸出格式是否規(guī)范”作為獎勵信號，讓模型學會在評估中迭代提升。

該模型能識別12類常見錯誤，包括類型錯誤（占比24.9%）、數(shù)學表示錯誤（23.8%）等，能夠發(fā)現(xiàn)“代碼編譯通過但邏輯偏離原題”的隱性問題。

△圖2：不同類型錯誤的分布

CriticLeanBench：首個聚焦形式化任務語義評估的基準測試

CriticLeanBench是用于評估模型在數(shù)學形式化任務中關鍵推理能力的基準測試，旨在全面衡量模型將自然語言數(shù)學陳述轉化為經(jīng)形式驗證的定理聲明等方面的表現(xiàn).

其構建和實現(xiàn)過程如下：

CriticLeanBench 在數(shù)據(jù)收集階段，從多個數(shù)據(jù)來源選取數(shù)學陳述及對應的Lean 4 陳述，提交Lean 4陳述到編譯器。1）對于編譯失敗的語句，隨機采樣保留編譯器反饋信息。2）對于編譯成功的部分，通過使用 DeepSeek R1 結合專家校驗的方式保留正確和錯誤的樣本（錯誤的樣本保留錯誤信息）。

• 數(shù)據(jù)來源多樣：
• 數(shù)學陳述選取了Omni-MATH、AIME、U-MATH等多個數(shù)據(jù)源，這些數(shù)據(jù)源涵蓋了不同難度層次和數(shù)學領域的問題。有助于更全面準確地評估模型在不同數(shù)學內(nèi)容上的表現(xiàn)。
• 覆蓋多種錯誤類型：
• CriticLeanBench 覆蓋語法錯誤、語義錯誤、邏輯錯誤等多種問題，全面考察模型能力。
• 確保評估可靠有效：
• 通過專家審查和大模型驗證相結合的方式來保證評估基準的可靠性和有效性。在不同類別中選取具有代表性的樣本，確保涵蓋各種錯誤類型，從而使評估結果更可靠。

△圖3: CriticLeanBench 構建的概覽

△表1：CriticLeanBench 數(shù)據(jù)集統(tǒng)計信息與各類代碼基準數(shù)據(jù)集的對比

在包含500組測試樣本的CriticLeanBench基準中，CriticLeanGPT的準確率達到87%，遠超GPT-4o（67.8%）和Claude 3.5（74.2%），甚至超過DeepSeek-R1（84%）的表現(xiàn)。

• 核心指標：
• Qwen3-32B-RL版本準確率達87%，true negative rate（正確識別錯誤樣本）達85.6%，遠超GPT-4o的40.0%。
• 對比優(yōu)勢：
• 在相同模型規(guī)模下，經(jīng)CriticLean訓練的Qwen2.5-32B模型準確率（78.6%）較基礎版（73.0%）提升5.6%，且對錯誤樣本的識別能力提升明顯。

△表2：在 CriticLeanBench 上的性能表現(xiàn)

模型大小的Scaling分析表明，模型性能隨規(guī)模提升穩(wěn)步增強。

△圖4: 大語言模型在 CriticLeanBench 上的擴展性分析(? 表示閉源的大語言模型)

FineLeanCorpus：28.5萬條高質量形式化數(shù)據(jù)

依托CriticLean框架，團隊構建了目前規(guī)模最大、質量最高的數(shù)學形式化數(shù)據(jù)集之一：

• 規(guī)模與多樣性：
• 包含285,957條樣本，覆蓋從高中奧數(shù)到大學數(shù)學的16個領域，其中高難度子集（Diamond）含36,033條問題。
• 質量保障：
• 每條樣本均通過編譯器語法檢查與CriticLeanGPT語義驗證，人工抽檢準確率達84%以上。
• 結構優(yōu)勢：
• 相比LeanWorkbook，其難度分布更均衡（多峰分布），領域覆蓋更全面（如解析幾何樣本量提升300%）。

△表3：FineLeanCorpus 的不同來源及數(shù)據(jù)集統(tǒng)計信息

與高度偏斜的 Lean-Workbook 相比，F(xiàn)ineLeanCorpus 提供了更透明的批判過程、更高比例的頂級問題，以及更加平衡和多樣化的主題分布

△表4：數(shù)據(jù)集統(tǒng)計信息的對比

與高度偏斜的 Lean-Workbook 相比，F(xiàn)ineLeanCorpus 提供了更透明的批判過程、更高比例的頂級問題，以及更加平衡和多樣化的主題分布

△圖5：數(shù)據(jù)集統(tǒng)計信息的對比()

實驗結果：大幅提高數(shù)學形式化準確率

將該框架應用于自動形式化流程，配合Kimina-Autoformalizer-7B生成器，準確率從38%（單輪生成）提升至84%（多輪迭代優(yōu)化），其中語義評估環(huán)節(jié)貢獻了30個百分點的提升。

△表5：自動化形式化性能的人類評估準確率結果

論文鏈接：https://arxiv.org/pdf/2507.06181
項目鏈接：https://github.com/multimodal-art-projection/CriticLean