IXThinker·2025-05-08 22:40

FormalMATH基準出爐 模型成功率僅16%

港中文、西湖大學、浙江大學及馬克斯·普朗克智能系統研究所等機構聯合推出形式化數學推理基準FormalMATH，收錄5560道經嚴格驗證的數學題。測試顯示，最強AI模型成功率僅16.46%，定理證明仍是AI公認難題。

基準規模與範圍

FormalMATH包含5560道經嚴格驗證的數學題，覆蓋從奧數到大學水平的代數、微積分、數論等領域，是首次系統性評估LLM驅動定理證明器的大型基準，為後續研究提供統一標尺。