最強(qiáng)AI模型面對(duì)5560道數(shù)學(xué)難題，成功率僅16.46%？背后真相大揭秘。

香港中文大學(xué)、西湖大學(xué)、MAP、浙江大學(xué)、馬克斯·普朗克智能系統(tǒng)研究所等機(jī)構(gòu)聯(lián)合推出FormalMATH形式化數(shù)學(xué)推理基準(zhǔn)測(cè)試，含5560道經(jīng)過(guò)嚴(yán)格驗(yàn)證的數(shù)學(xué)題，覆蓋從奧數(shù)到大學(xué)水平的代數(shù)、微積分、數(shù)論等領(lǐng)域。

形式化數(shù)學(xué)推理是人工智能領(lǐng)域公認(rèn)的核心難題之一。

盡管大語(yǔ)言模型（LLM）在自然語(yǔ)言處理和代碼生成等領(lǐng)域取得顯著進(jìn)展，但面對(duì)需要嚴(yán)格邏輯推導(dǎo)的數(shù)學(xué)定理證明任務(wù)時(shí)，其能力仍面臨嚴(yán)峻挑戰(zhàn)。

FormalMATH基準(zhǔn)測(cè)試首次系統(tǒng)性評(píng)估了當(dāng)前LLM驅(qū)動(dòng)的定理證明器的真實(shí)水平。

結(jié)果顯示：即便是表現(xiàn)最佳的模型Kimina-Prover ，在實(shí)際計(jì)算資源限制下（Pass@32采樣量），成功率也僅為16.46% ；而多數(shù)模型在微積分等領(lǐng)域的表現(xiàn)接近「隨機(jī)猜測(cè)」。

FormalMATH：「超大規(guī)?！沟男问交瘮?shù)學(xué)推理基準(zhǔn)

規(guī)模突破：22.8倍于現(xiàn)有基準(zhǔn)

FormalMATH包含5560個(gè)經(jīng)過(guò)Lean4編譯器驗(yàn)證的數(shù)學(xué)命題，涵蓋代數(shù)、數(shù)論、微積分、離散數(shù)學(xué)等12個(gè)子領(lǐng)域，問(wèn)題難度從國(guó)際數(shù)學(xué)奧林匹克（IMO）競(jìng)賽級(jí)延伸至本科課程，規(guī)模是經(jīng)典基準(zhǔn)MiniF2F的22.8倍。

構(gòu)建創(chuàng)新：人類(lèi)在循環(huán)中的自動(dòng)化流程用于自動(dòng)形式化和語(yǔ)義一致性檢測(cè)

為解決傳統(tǒng)形式化數(shù)據(jù)依賴專(zhuān)家手動(dòng)標(biāo)注的瓶頸，研究團(tuán)隊(duì)提出了一套「三階段過(guò)濾」框架：

1. 多LLM協(xié)同翻譯 ：通過(guò)微調(diào)后的Qwen2.5-7B-Coder、Deepseek-Prover-V1.5-Base等模型將自然語(yǔ)言問(wèn)題轉(zhuǎn)為多個(gè)候選的形式化命題；
2. 自動(dòng)化驗(yàn)證 ：利用Lean4編譯器篩選語(yǔ)法正確命題，并通過(guò)多LLM語(yǔ)義一致性校驗(yàn)（如o1-mini、Claude-3.5）過(guò)濾錯(cuò)誤；
3. 否定反證過(guò)濾 ：調(diào)用LLM證明器嘗試「證偽」命題，排除無(wú)法成立的陳述。該流程在人工審核前保留了72.09%的高質(zhì)量命題，大幅降低專(zhuān)家工作量。

最后，團(tuán)隊(duì)召集了12名人類(lèi)奧賽金牌級(jí)別的專(zhuān)家花了22天檢測(cè)自然語(yǔ)言數(shù)學(xué)命題與Lean4形式化命題之間的語(yǔ)義一致性。

現(xiàn)有LLM證明器表現(xiàn)：代數(shù)尚可，微積分「翻車(chē)」

整體低迷：16%成功率暴露能力斷層

在FormalMATH全量數(shù)據(jù)集上，主流LLM證明器的表現(xiàn)遠(yuǎn)低于預(yù)期：

• 最佳模型Kimina-Prover（Pass@32）：16.46%；
• 次優(yōu)模型STP（Pass@32）：13.87%

領(lǐng)域偏見(jiàn)：代數(shù)強(qiáng)，微積分弱

現(xiàn)有模型在代數(shù)等領(lǐng)域表現(xiàn)較好，但在微積分等其他領(lǐng)域表現(xiàn)較差，顯示出明顯的領(lǐng)域偏差。

錯(cuò)誤模式：濫用「捷徑戰(zhàn)術(shù)」

分析顯示，LLM證明器頻繁濫用自動(dòng)化策略（如aesop、linarith），試圖用單一步驟替代多步推理，導(dǎo)致以下典型錯(cuò)誤（以DeepSeek-RL為例）：

1. 冗余假設(shè)（34%）： 引入無(wú)關(guān)前提條件
2. 不完整證明（62%）： 缺失關(guān)鍵推導(dǎo)步驟, 無(wú)法形成完整構(gòu)造證明
3. 自動(dòng)化策略誤用 （65.0%）：錯(cuò)誤調(diào)用自動(dòng)化工具（如用integral_mono_on跳過(guò)控制收斂定理驗(yàn)證）
4. 無(wú)法正確應(yīng)對(duì)不等式 （13.0%）：錯(cuò)誤地（例如在指數(shù)爆炸的情況）過(guò)度依賴linarith或者nlinarith等自動(dòng)化不等式計(jì)算策略

突破方向：讓LLM學(xué)會(huì)「嚴(yán)謹(jǐn)思考」

技術(shù)瓶頸：自然語(yǔ)言引導(dǎo)反拖后腿

研究團(tuán)隊(duì)發(fā)現(xiàn)一個(gè)反直覺(jué)現(xiàn)象：在鏈?zhǔn)剿季S（CoT）場(chǎng)景中，提供自然語(yǔ)言解題思路反而會(huì)降低證明成功率。

例如，DeepSeek-V1.5-RL模型在普通的CoT提示時(shí)表現(xiàn)優(yōu)于引入人為自然語(yǔ)言引導(dǎo)的情況。

未來(lái)路徑：從「戰(zhàn)術(shù)依賴」到「戰(zhàn)略規(guī)劃」

未來(lái)，提升LLM形式化推理能力需從三方面突破：

1. 強(qiáng)化多步規(guī)劃 ：減少對(duì)aesop等單步戰(zhàn)術(shù)的依賴，設(shè)計(jì)分層推理架構(gòu)；
2. 跨領(lǐng)域泛化 ：通過(guò)課程學(xué)習(xí)（Curriculum Learning）平衡代數(shù)/微積分等領(lǐng)域的訓(xùn)練數(shù)據(jù)；
3. 人機(jī)協(xié)同驗(yàn)證 ：開(kāi)發(fā)交互式證明輔助工具，讓LLM與人類(lèi)專(zhuān)家協(xié)同完成復(fù)雜定理證明。

開(kāi)源開(kāi)放：數(shù)據(jù)、代碼與模型已全面公開(kāi)

研究團(tuán)隊(duì)呼吁學(xué)術(shù)界與工業(yè)界共同推進(jìn)形式化數(shù)學(xué)推理技術(shù)的發(fā)展，助力AI在數(shù)學(xué)發(fā)現(xiàn)、形式化驗(yàn)證等領(lǐng)域?qū)崿F(xiàn)更可靠的應(yīng)用。

FormalMATH基準(zhǔn)測(cè)試的代碼、訓(xùn)練數(shù)據(jù)及評(píng)估模型已向公眾開(kāi)放：

論文鏈接 ：https://arxiv.org/pdf/2505.02735

項(xiàng)目倉(cāng)庫(kù) ：https://github.com/Sphere-AI-Lab/FormalMATH-Bench

基準(zhǔn)數(shù)據(jù)集 ：https://huggingface.co/SphereLab