多模态AI的数学困境：从图像到形式化证明，准确率仅4%揭示深层推理鸿沟

香港科技大学研究团队新推出的MATP-BENCH基准测试揭示，尽管多模态大模型（MLLMs）能较好地理解包含图像的数学问题，但在将这些理解转化为可验证的形式化证明时，其准确率骤降至仅4%，暴露了AI在严谨逻辑推理上的根本性瓶颈。

在人工智能领域，大型语言模型（LLMs）的飞速发展已使其在处理文本信息方面取得了令人瞩目的成就。然而，人类智能的真正体现，往往超越了纯粹的语言范畴，融入了对视觉、听觉等多模态信息的综合感知与推理。特别是在数学和科学领域，图形、图表等视觉元素不仅是辅助理解的工具，更是构建严谨逻辑证明的直觉来源。那么，当下的多模态大模型（MLLMs）能否像人类数学家一样，从图文中汲取信息，并完成机器可严格验证的形式化证明（Formal Proof）呢？香港科技大学的研究团队与合作者推出的MATP-BENCH基准测试，给出了一个清醒的答案：我们距离实现这一目标，仍有漫长的路要走。

挑战几何直觉：MATP-BENCH的诞生与设计理念

长期以来，自动定理证明（ATP）的研究主要聚焦于纯文本形式的定理，取得了显著进展。然而，现实世界的数学问题，尤其是几何学，其表达和理解离不开视觉元素。人类凭借对图形的直觉，能够迅速把握关键信息并指引证明过程。MATP-BENCH正是为了填补这一空白而生，它旨在系统性地评估MLLMs在多模态自动定理证明方面的真实能力 ¹。

MATP-BENCH作为首个专为多模态定理证明设计的基准，具有多项核心特点：

• 多模态上下文： 每个问题都由一张图像和一个自然语言陈述构成，两者互为补充，共同提供完整的定理信息。这要求模型不仅能处理文本，更要从图像中提取未明确表达的几何关系（例如，通过图像判断线段平行或垂直，而不仅仅是文本描述）。
• 多层次与多样性： 基准共包含1056个多模态定理，题目难度涵盖高中、大学和竞赛三个级别，内容上则覆盖了平面几何、3D几何、解析几何等多个领域。这种设计旨在全面评估模型在不同复杂程度和知识广度下的表现。
• 多语言形式化： 所有定理都提供了在Lean 4、Coq 和 Isabelle这三种主流形式化证明辅助工具中的形式化版本。这些语言具有高度的逻辑严谨性，确保了证明的机器可验证性，同时也使得评估结果更具通用性。

为了精准定位模型的瓶颈，MATP-BENCH设置了两个关联的核心任务：

1. 多模态自动定理证明 (Multimodal Automated Theorem Proving)： 模拟人类专家从图文理解到端到端生成形式化定理及证明的全过程。
2. 多模态定理形式化 (Multimodal Theorem Formalization)： 仅评估模型将多模态信息理解并翻译为形式化定理陈述的能力，不要求生成完整证明。

这项基准与现有纯文本或仅侧重“自动形式化”的基准（如miniF2F、ProofNet、LeanEuclid等）形成了鲜明对比，它聚焦于MLLM从零开始构建可验证证明的端到端能力 ¹。

揭示瓶颈：大模型在严谨推理面前的真实表现

MATP-BENCH的实验结果清晰地描绘了当前MLLM在形式化定理证明上的能力边界和核心瓶颈。最令人警醒的发现是，模型的主要瓶颈并非“看懂题目”，而是后续“构建证明”的复杂逻辑推理过程 ¹。

• 理解与证明的巨大鸿沟： 以Lean 4语言为例，模型在任务二（仅形式化定理）上的平均pass@10成功率（即10次尝试内成功一次的概率）可达45.16%。这表明，MLLMs已具备相当不错的图文理解和形式化转译能力，能够将视觉和文本信息转化为形式化语言可理解的数学命题。然而，在需要完整证明的任务一上，这一数值骤降至仅4.26%。这一巨大落差直观地揭示了当前MLLMs在严谨逻辑推理和证明生成方面的深层缺陷。
• 难度与准确率的负相关： 模型的性能随着题目难度的增加而显著下降。在Lean 4的任务一中，模型在高中、大学和竞赛级别问题上的平均成功率分别为6.39%、2.85%和1.29%，这表明复杂逻辑和抽象思维是模型的巨大挑战 ¹。
• 形式化语言的差异与错误模式： 实验显示，模型在不同形式化语言上的性能存在差异。令人意外的是，在生成Coq语言上，某些模型的任务一成功率达到了12.15%，显著高于Lean 4和Isabelle。研究者推测，这可能与Coq更成熟的策略库、丰富的数学资源以及其命令式策略风格更适合大模型学习有关 ¹。
  • 不同模型的错误类型也揭示了其能力层次。 表现较好的闭源模型（如Claude-3.7和GPT-4.1）的错误主要集中在“无效或未完成的证明步骤”和“缺失前提/隐藏假设”，这意味着它们理解了基本概念，但无法完成复杂逻辑跳跃或发现隐含条件。而一些开源模型（如Qwen2.5-VL）则暴露出更多“基础性的生成错误”，例如“不正确或未声明的变量/定义”以及“缺失/错误的库导入”，表明它们甚至在掌握形式化语言的基本语法和规范上就已困难重重 ¹。
• 辅助线难题： 在人类几何解题中，添加辅助线是一种常见且强大的策略，它需要高度的直觉、创造性和前瞻性思维。MATP-BENCH的实验发现，随着题目难度的增加，需要辅助线的问题比例也显著上升。尽管模型能够尝试引入辅助线等构造性步骤，但它们几乎无法有效构造和利用辅助线来推进证明，导致包含辅助线构造的证明成功率极低 ¹。这凸显了当前AI在处理需要非显式信息或创造性构造才能解决的问题时的局限性。

这些结果与更广泛的多模态大模型评估趋势相符。例如，小红书和上海交通大学发布的WorldSense基准也指出，现有MLLMs在音视频融合和理解方面表现不佳，甚至某些开源模型的准确率与随机猜测相当 ²。知乎上关于2024年多模态大模型综述的文章也强调，MLLM的“推理”（Reasoning）能力是超越“理解”（Understanding）的更高层次挑战，它涉及执行复杂的跨模态推理 [^4, ^5]。

超越表面理解：AI迈向真正智能的深远路径

MATP-BENCH的研究结果清晰地表明，尽管MLLMs在处理多模态信息方面取得了进步，但它们远未达到人类在严谨数学推理和证明构建上的能力。这种理解和推理之间的巨大鸿沟，对于AI的未来发展具有深远影响。

当前的MLLMs更像是一种高级的模式识别器和信息转换器，而非真正的逻辑推理者。它们能够识别图像中的几何实体，将其转化为符号表达，但在构建从前提推导结论的逻辑链条时，却步履维艰。这种局限性不仅仅是数学问题，它意味着在任何需要严谨、可验证逻辑推理的领域，如软件验证、医疗诊断、法律判决甚至科学发现，我们都不能盲目依赖当前的AI系统。一旦AI的输出涉及高风险决策，其背后的逻辑透明度和可信度就变得至关重要。

要让MLLM成为合格的多模态定理证明者，研究需要重点关注以下方向：

• 提升符号推理能力： 这要求开发新的模型架构或训练方法，专门增强模型在严谨的形式化逻辑系统中的推理和证明构建能力。这可能涉及到对经典符号AI方法和深度学习方法的更深层次融合，或者探索像链式思维（M-CoT）和上下文学习（M-ICL）这类旨在提升推理链条的方案 ³。
• 增强视觉-符号联合推理： 让模型不仅能“看见”图中的几何关系，更能将其无缝转化为可用于证明的形式化符号语言。这意味着需要更强大的跨模态对齐和融合机制，使得视觉特征能够直接、准确地驱动符号操作。
• 探索交互式证明生成： 借鉴人类与证明辅助工具（Proof Assistants）交互的模式，允许模型利用外部工具进行辅助思考，或在证明过程中接受人类的指导和反馈。这种人机协作的模式，可能是一个充满希望的研究方向，尤其是在自动化程度尚未达到要求但又急需辅助的复杂场景中 ¹。

MATP-BENCH的发布，不仅为多模态自动定理证明领域提供了一个重要的评估工具，更像是一面镜子，清晰地映照出当前大模型能力与人类智能之间的核心差距。它提醒我们，真正的通用人工智能，不仅仅是拥有庞大的参数和处理多模态数据的能力，更在于其是否能掌握逻辑的本质，进行严谨的、可验证的推理。这是AI研究的下一个前沿，也是决定AI能否真正赋能人类高阶认知任务的关键所在。

References

• 多模态大模型
• 形式化证明
• 人工智能
• 逻辑推理
• MATP-BENCH
• 几何学
• AI瓶颈
• 计算机科学