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

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

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

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

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

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

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

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

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

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

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

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

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

團(tuán)隊(duì)基于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)練，增強(qiáng)其針對語義判斷的評估能力。
• 強(qiáng)化學(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)形式驗(yàn)證的定理聲明等方面的表現(xiàn).

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

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

• 數(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 覆蓋語法錯誤、語義錯誤、邏輯錯誤等多種問題，全面考察模型能力。
• 確保評估可靠有效：通過專家審查和大模型驗(yàn)證相結(jié)合的方式來保證評估基準(zhǔn)的可靠性和有效性。在不同類別中選取具有代表性的樣本，確保涵蓋各種錯誤類型，從而使評估結(jié)果更可靠。

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

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

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

• 核心指標(biāo)：Qwen3-32B-RL版本準(zhǔn)確率達(dá)87%，true negative rate（正確識別錯誤樣本）達(dá)85.6%，遠(yuǎn)超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)步增強(qiáng)。

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

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

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

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

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

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

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

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

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

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

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

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

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