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

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

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

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

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

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

數(shù)學(xué)形式化領(lǐng)域的核心挑戰(zhàn)

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

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

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

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

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

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

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

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

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

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

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

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

CriticLeanBench：首個聚焦形式化任務(wù)語義評估的基準(zhǔn)測試

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

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

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

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

△圖3: CriticLeanBench 構(gòu)建的概覽

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

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

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

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

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

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

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

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

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

實驗結(jié)果：大幅提高數(shù)學(xué)形式化準(zhǔn)確率

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

△表5：自動化形式化性能的人類評估準(zhǔn)確率結(jié)果

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