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

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

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

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

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

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

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

項(xiàng)目主頁：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è)計(jì)

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

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

核心特點(diǎn)包括：

• 多模態(tài)上下文：每個問題都由一張圖像和一個自然語言陳述組成，二者互為補(bǔ)充，共同構(gòu)成完整的定理信息。
• 多層次與多樣性：基準(zhǔn)共包含 1056個多模態(tài)定理 ，題目難度橫跨高中、大學(xué)和競賽三個級別 。內(nèi)容上則覆蓋了平面幾何、3D幾何、解析幾何等多個領(lǐng)域 。
• 多語言形式化：所有定理都提供了在 Lean 4、Coq 和 Isabelle 三種證明輔助工具中的形式化版本，確保了廣泛的兼容性 。

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

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

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

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

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

實(shí)驗(yàn)結(jié)果

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

總結(jié)與展望

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

• 提升符號推理能力：開發(fā)新的模型架構(gòu)或訓(xùn)練方法，專門增強(qiáng)模型在嚴(yán)謹(jǐn)?shù)男问交壿嬒到y(tǒng)中的推理和證明構(gòu)建能力。
• 增強(qiáng)視覺-符號聯(lián)合推理：讓模型不僅能「看見」圖中的幾何關(guān)系，更能將其無縫轉(zhuǎn)化為可用于證明的形式化符號語言。
• 探索交互式證明生成：讓其利用外部工具進(jìn)行輔助思考，可能是一個充滿希望的研究方向 。