现实世界中，几何学定理常借助图像等视觉元素呈现，人类数学家擅长从中获取直觉引导证明。但当前多模态大模型（MLLMs）能否模仿人类完成形式化证明，这一潜能尚待挖掘。为此，香港科技大学团队推出了多模态自动定理证明基准——MATP-BENCH ，用以评估MLLMs在处理包含图像和文本的几何定理证明中的能力。
MATP-BENCH 专为多模态定理证明设计，涵盖Lean4、Coq和Isabelle三种主流形式化证明语言。其核心特点鲜明：一是多模态上下文，每个问题由图像和自然语言陈述构成，共同提供定理信息；二是多层次与多样性，包含1056个多模态定理，难度跨越高中、大学和竞赛级别，覆盖多种几何领域；三是多语言形式化，所有定理都有三种证明辅助工具的形式化版本，兼容性广泛。
与传统自动定理证明（ATP）任务不同，MATP-BENCH要求模型结合图像和自然语言，提取关键前提构建形式化定理。为精准评估模型能力，它设置了两个核心任务：多模态自动定理证明和多模态定理形式化。
通过大量实验，研究团队发现了MLLMs在形式化定理证明上的核心瓶颈。不同模型的「犯错」方式有别，闭源模型如Claude-3.7和GPT-4.1主要在证明步骤和前提假设方面出错，而开源模型如Qwen2.5-VL则存在更多基础性生成错误。
实验还揭示了模型在不同形式化语言上的性能差异。最强大的模型在Lean4语言上的pass@10成功率仅为4.26%，而在Coq语言上任务一的成功率达12.15%。此外，模型性能随题目难度增加显著下降，在Lean4的任务一中，高中、大学和竞赛级别问题的平均成功率分别为6.39%、2.85%和1.29%。
核心瓶颈在于「证明」而非「看懂」。模型在任务二（仅形式化定理）上表现较好，Lean4语言的平均pass@10成功率可达45.16%，但在任务一（端到端形式化证明）上骤降至4.26%。而且，模型在辅助线构造和利用上能力不足，包含辅助线构造的证明成功率极低。
要让MLLMs成为合格的多模态定理证明者，后续研究需重点关注：提升符号推理能力，增强视觉 – 符号联合推理，探索交互式证明生成。
