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