自动定理证明领域虽有进展，但多集中于纯文本定理。现实中，几何学定理常需结合图像理解，而多模态大模型能否基于图文完成可被机器验证的形式化证明，此前尚未得到充分探索。香港科技大学研究团队推出的 MATP-BENCH 基准，填补了这一空白，为评估多模态大模型（MLLMs）在此领域的能力提供了新方向。
MATP-BENCH 基准：多模态定理证明新标尺
MATP-BENCH 是首个专为多模态定理证明设计的基准，涵盖 Lean 4、Coq 和 Isabelle 三种主流形式化证明语言。其设计具备三大核心特点：多模态上下文，每个问题由图像与自然语言陈述构成，相互补充；多层次与多样性，1056 个多模态定理覆盖高中、大学和竞赛难度，涉及平面、3D、解析几何等多领域；多语言形式化，定理提供三种证明辅助工具的形式化版本，确保兼容性。
与现有基准相比，MATP-BENCH 优势显著。多数基准仅含纯文本定理，部分虽涉及多模态几何问题，但主要聚焦 “自动形式化”，而非生成证明。MATP-BENCH 设置多模态自动定理证明和多模态定理形式化两个核心任务，分别模拟端到端证明过程与评估图文转形式化定理的能力 。
实验揭示：MLLMs 的能力边界与挑战
实验结果显示，MLLMs 在形式化定理证明上困难重重。在最强大的模型中，于 Lean 4 语言的多模态自动定理证明任务里，10 次尝试内成功一次的概率仅为 4.26%；而在 Coq 语言上，任务一成功率达 12.15%，或因 Coq 策略库成熟、数学资源丰富且命令式策略风格利于大模型学习。
随着题目难度提升，模型性能显著下降。在 Lean 4 任务一中，高中、大学和竞赛级问题平均成功率分别为 6.39%、2.85% 和 1.29%。不同模型错误模式各异，闭源模型如 Claude-3.7 和 GPT-4.1 多因无效证明步骤、缺失前提出错；开源模型如 Qwen2.5-VL 除逻辑问题外，还存在变量定义错误、库导入缺失等基础问题 。
进一步分析发现，模型在将图文信息转为形式化定理方面有一定能力，在多模态定理形式化任务中，Lean 4 语言下平均 pass@10 成功率达 45.16%，但在完整证明构建上表现极差，自动定理证明任务成功率仅 4.26%，说明 “构建证明” 的复杂逻辑推理是主要瓶颈。此外，在几何证明关键的辅助线构造与运用上，模型虽有尝试，但成功率极低 。
未来方向：突破瓶颈的三大路径
基于研究结果，让 MLLM 成为合格的多模态定理证明者，需从三方面发力。一是提升符号推理能力，开发新架构或训练方法，强化模型在形式化逻辑系统中的推理与证明构建能力；二是增强视觉 - 符号联合推理，使模型能将视觉几何关系高效转化为证明用的形式化符号语言；三是探索交互式证明生成，借助外部工具辅助模型思考，为研究提供新方向 。
上述内容呈现了多模态定理证明研究的新动态。若你想补充案例、深入分析某部分内容，或调整文章风格，随时和我说。