新智元報道

編輯：LRST

【新智元導讀】MATP-BENCH是一個新推出的多模態自動定理證明基準，旨在評估多模態大模型（MLLMs）在處理包含圖像和文本的幾何定理證明中的能力。實驗表明，盡管模型在將圖文信息轉化為形式化定理方面有一定能力，但在構建完整證明時面臨重大挑戰，尤其是復雜邏輯推理和輔助線構造方面。

近年來，自動定理證明（ATP）取得了顯著進展，但大部分工作都集中在處理純文本形式的定理。

然而，在現實世界中，尤其是在幾何學領域，許多定理的呈現和理解都離不開圖像、圖表等視覺元素。

人類數學家善于從這些圖表中獲取直覺，并將其作為引導嚴謹證明過程的關鍵。

那么，當下的多模態大模型（MLLMs）能否模仿人類的這一能力，從圖文中汲取信息，完成可被機器嚴格驗證的形式化證明 (Formal Proof) 呢？

這一重要潛能，在很大程度上仍未被探索。

為了系統性地回答這一問題，香港科技大學的研究團隊推出了MATP-BENCH，一個全新的多模態、多層次、多形式化語言的自動定理證明基準，旨在全面評估MLLMs作為自動定理證明者 (Automated Theorem Prover)的真實能力。

論文地址：https://arxiv.org/pdf/2506.06034

項目主頁：https://matpbench.github.io/

MATP-BENCH任務與傳統ATP任務的對比。傳統ATP僅依賴文本化的定理陳述，而MATP-BENCH要求模型必須結合圖像和自然語言，并從中提取文本中未明確說明的關鍵前提（如圖中「From diagram」部分所示），才能構建完整的形式化定理 。

MATP-BENCH的設計

MATP-BENCH是首個專為多模態定理證明設計的基準，涵蓋了三種主流的形式化證明語言：Lean 4、Coq和Isabelle。

MATP-BENCH 的統計數據。左表展示了不同難度級別和幾何類型的題目分布，右表展示了更細分的數學主題分布 。

核心特點包括：

• 多模態上下文：每個問題都由一張圖像和一個自然語言陳述組成，二者互為補充，共同構成完整的定理信息。

• 多層次與多樣性：基準共包含1056個多模態定理，題目難度橫跨高中、大學和競賽三個級別 。內容上則覆蓋了平面幾何、3D幾何、解析幾何等多個領域 。

• 多語言形式化：所有定理都提供了在Lean 4、Coq 和 Isabelle三種證明輔助工具中的形式化版本，確保了廣泛的兼容性 。

MATP-BENCH與相關可驗證基準的詳細對比。MATP-BENCH在多模態、多層次和多形式化語言支持上具有綜合優勢。

多數現有基準如 miniF2F 和 ProofNet 僅包含純文本定理 。雖然 LeanEuclid 等基準包含多模態幾何問題，但其主要任務是「自動形式化」（將人類語言證明轉為代碼），而非從零開始生成證明 。

為了精準評估模型在不同階段的能力，MATP-BENCH設置了兩個關聯的核心任務：

（1）多模態自動定理證明 (Multimodal Automated Theorem Proving)：模擬人類專家的端到端形式化定理及證明過程；

（2）多模態定理形式化 (Multimodal Theorem Formalization)：單獨評估模型理解和翻譯多模態信息為形式化定理的能力。

實驗結果

通過在MATP-BENCH上進行的大量實驗，研究團隊不僅定位了當前多模態大模型（MLLM）在形式化定理證明上的核心瓶頸，更從多個維度揭示了其能力的邊界和挑戰。

實驗揭示了模型在不同形式化語言上的性能差異，最強大的模型在Lean 4語言上pass@10成功率僅為4.26%，而在生成Coq語言上表現出人意料地好，任務一的成功率達到了12.15%，顯著高于Lean 4和Isabelle。

研究者推測，這可能得益于Coq更成熟的策略庫、豐富的數學資源以及更適合大模型學習的命令式策略風格。

模型的性能隨著題目難度的增加而顯著下降。

在Lean 4的任務一中，模型在高中、大學和競賽級別問題上的平均成功率分別為6.39%、2.85%和1.29%

不同模型「犯錯」方式不同

圖中展示了三類模型在 Lean 4 任務上的錯誤分布?？梢郧逦乜吹?，Qwen2.5-VL（右）的基礎性錯誤（如變量定義和庫導入）比例顯著高于 Claude-3.7（左）和 GPT-4.1（中）

對于表現較好的閉源模型（如Claude-3.7和GPT-4.1），其錯誤主要集中在「無效或未完成的證明步驟」和「缺失前提/隱藏假設」 。而對于一些開源模型（如Qwen2.5-VL），錯誤模式則有所不同。

雖然它們同樣存在邏輯推理問題，但取它們出現了更多基礎性的生成錯誤，例如「不正確或未聲明的變量/定義」以及「缺失/錯誤的庫導入」。這說明，這類模型不僅在高級邏輯上面臨挑戰，在掌握形式化語言的基本語法和規范上就已困難重重 。

核心瓶頸——「證明」而非「看懂」

實驗另外揭示了一個普遍現象：模型在任務一（端到端形式化證明）上的表現普遍不佳，但在任務二（僅形式化定理）上表現要好得多。

以Lean 4語言為例，模型在任務二上的平均pass@10成功率（即10次嘗試內成功一次的概率）可達45.16%，這說明它們具備了相當不錯的圖文理解和形式化轉譯能力。

然而，在需要完整證明的任務一上，該數值驟降至僅4.26%，這一差距清晰地表明：當前MLLM的主要瓶頸并非「看懂題目」，而是后續「構建證明」的復雜邏輯推理過程。

輔助線難題——「畫不好也用不好」

圖中灰色曲線顯示需要輔助線的問題比例隨難度上升。模型的嘗試率（虛線）也隨之上升，但成功率（實線）卻始終處于極低水平

在人類的幾何解題中，添加輔助線是一種常見且強大的策略。

實驗發現，隨著題目難度的增加，需要輔助線的問題比例也顯著上升。

模型在一定程度上能夠模仿人類，嘗試在證明中引入輔助線等構造性步驟 。

然而，它們幾乎無法有效構造和利用輔助線來推進證明，導致包含輔助線構造的證明成功率極低 。

總結與展望

MATP-BENCH的研究結果清晰地表明要讓MLLM成為合格的多模態定理證明者，研究需要重點關注：

• 提升符號推理能力：開發新的模型架構或訓練方法，專門增強模型在嚴謹的形式化邏輯系統中的推理和證明構建能力。

• 增強視覺-符號聯合推理：讓模型不僅能「看見」圖中的幾何關系，更能將其無縫轉化為可用于證明的形式化符號語言。

• 探索交互式證明生成：讓其利用外部工具進行輔助思考，可能是一個充滿希望的研究方向 。

參考資料：

https://arxiv.org/abs/2506.06034