最強 AI 模型面對 5560 道數學難題，成功率僅 16.46%？背后真相大揭秘。
香港中文大學、西湖大學、MAP、浙江大學、馬克斯 · 普朗克智能系統研究所等機構聯合推出FormalMATH 形式化數學推理基準測試，含 5560 道經過嚴格驗證的數學題，覆蓋從奧數到大學水平的代數、微積分、數論等領域。
盡管大語言模型（LLM）在自然語言處理和代碼生成等領域取得顯著進展，但面對需要嚴格邏輯推導的數學定理證明任務時，其能力仍面臨嚴峻挑戰。
FormalMATH 基準測試首次系統性評估了當前 LLM 驅動的定理證明器的真實水平。
結果顯示：即便是表現最佳的模型 Kimina-Prover ，在實際計算資源限制下（Pass@32 采樣量），成功率也僅為 16.46% ；而多數模型在微積分等領域的表現接近「隨機猜測」。
FormalMATH：「超大規模」的形式化數學推理基準規模突破：22.8 倍于現有基準
FormalMATH 包含 5560 個經過 Lean4 編譯器驗證的數學命題，涵蓋代數、數論、微積分、離散數學等 12 個子領域，問題難度從國際數學奧林匹克（IMO）競賽級延伸至本科課程，規模是經典基準 MiniF2F 的 22.8 倍。
構建創新：人類在循環中的自動化流程用于自動形式化和語義一致性檢測
為解決傳統形式化數據依賴專家手動標注的瓶頸，研究團隊提出了一套「三階段過濾」框架：
多 LLM 協同翻譯 ：通過微調后的 Qwen2.5-7B-Coder、Deepseek-Prover-V1.5-Base 等模型將自然語言問題轉為多個候選的形式化命題；
自動化驗證 ：利用 Lean4 編譯器篩選語法正確命題，并通過多 LLM 語義一致性校驗（如 o1-mini、Claude-3.5）過濾錯誤；
否定反證過濾 ：調用 LLM 證明器嘗試「證偽」命題，排除無法成立的陳述。該流程在人工審核前保留了 72.09% 的高質量命題，大幅降低專家工作量。
最后，團隊召集了 12 名人類奧賽金牌級別的專家花了 22 天檢測自然語言數學命題與 Lean4 形式化命題之間的語義一致性。
在 FormalMATH 全量數據集上，主流 LLM 證明器的表現遠低于預期：
最佳模型 Kimina-Prover（Pass@32）：16.46%；
次優模型 STP（Pass@32）：13.87%
現有模型在代數等領域表現較好，但在微積分等其他領域表現較差，顯示出明顯的領域偏差。
分析顯示，LLM 證明器頻繁濫用自動化策略（如 aesop、linarith），試圖用單一步驟替代多步推理，導致以下典型錯誤（以 DeepSeek-RL 為例）：
冗余假設（34%）： 引入無關前提條件
不完整證明（62%）： 缺失關鍵推導步驟 , 無法形成完整構造證明
自動化策略誤用 （65.0%）：錯誤調用自動化工具（如用 integral_mono_on 跳過控制收斂定理驗證）
無法正確應對不等式 （13.0%）：錯誤地（例如在指數爆炸的情況）過度依賴 linarith 或者 nlinarith 等自動化不等式計算策略
突破方向：讓 LLM 學會「嚴謹思考」技術瓶頸：自然語言引導反拖后腿
研究團隊發現一個反直覺現象：在鏈式思維（CoT）場景中，提供自然語言解題思路反而會降低證明成功率。
例如，DeepSeek-V1.5-RL 模型在普通的 CoT 提示時表現優于引入人為自然語言引導的情況。
未來，提升 LLM 形式化推理能力需從三方面突破：
強化多步規劃 ：減少對 aesop 等單步戰術的依賴，設計分層推理架構；
跨領域泛化 ：通過課程學習（Curriculum Learning）平衡代數 / 微積分等領域的訓練數據；
人機協同驗證 ：開發交互式證明輔助工具，讓 LLM 與人類專家協同完成復雜定理證明。
開源開放：數據、代碼與模型已全面公開
研究團隊呼吁學術界與工業界共同推進形式化數學推理技術的發展，助力 AI 在數學發現、形式化驗證等領域實現更可靠的應用。
FormalMATH 基準測試的代碼、訓練數據及評估模型已向公眾開放：
論文鏈接 ：
https://arxiv.org/pdf/2505.02735
項目倉庫 ：
https://github.com/Sphere-AI-Lab/FormalMATH-Bench
基準數據集 ：
https://huggingface.co/SphereLab
一鍵三連「點贊」「轉發」「小心心」
歡迎在評論區留下你的想法！
— 完 —
學術投稿請于工作日發郵件到：
ai@qbitai.com
標題注明【投稿】，告訴我們：
你是誰，從哪來，投稿內容
附上論文 / 項目主頁鏈接，以及聯系方式哦
我們會（盡量）及時回復你
科技前沿進展每日見
