新智元報道

編輯：LRST

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

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

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

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

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

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

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

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

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

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

MATP-BENCH的設(shè)計

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

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

核心特點包括：

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

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

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

MATP-BENCH與相關(guān)可驗證基準的詳細對比。MATP-BENCH在多模態(tài)、多層次和多形式化語言支持上具有綜合優(yōu)勢。

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

為了精準評估模型在不同階段的能力，MATP-BENCH設(shè)置了兩個關(guān)聯(lián)的核心任務(wù)：

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

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

實驗結(jié)果

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

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

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

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

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

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

圖中展示了三類模型在 Lean 4 任務(wù)上的錯誤分布。可以清晰地看到，Qwen2.5-VL（右）的基礎(chǔ)性錯誤（如變量定義和庫導入）比例顯著高于 Claude-3.7（左）和 GPT-4.1（中）

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

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

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

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

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

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

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

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

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

實驗發(fā)現(xiàn)，隨著題目難度的增加，需要輔助線的問題比例也顯著上升。

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

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

總結(jié)與展望

MATP-BENCH的研究結(jié)果清晰地表明要讓MLLM成為合格的多模態(tài)定理證明者，研究需要重點關(guān)注：

• 提升符號推理能力：開發(fā)新的模型架構(gòu)或訓練方法，專門增強模型在嚴謹?shù)男问交壿嬒到y(tǒng)中的推理和證明構(gòu)建能力。

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

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

參考資料：

https://arxiv.org/abs/2506.06034