香港科技大学推出多模态自动定理证明基准，探索AI在几何定理证明中的潜力

近年来，自动定理证明（Automated Theorem Proving, ATP）的研究取得了显著进展，但绝大多数研究仍然局限于处理文本形式的定理。这在一定程度上限制了研究的广度，尤其是在几何学领域，许多定理的呈现和理解往往依赖于图像、图表等视觉元素。传统的文本导向模型在处理这些多模态信息时，往往显得力不从心。人类数学家在作出严谨证明时，善于从视觉信息中提取直觉，这是当前多模态大模型（Multimodal Large Language Models, MLLMs）尚未充分探索的潜能。

为了解决这一问题，香港科技大学的研究团队正式推出了一个全新的多模态、多层次和多形式化语言的自动定理证明基准，名为“”。该基准旨在从多个维度对MLLMs的真实能力进行全面评估，以探索AI在几何定理证明中的潜力。

新推出的基准设计旨在模拟实际的数学问题解决过程，涵盖了文本和图像两种形式的信息。每个问题都由一张图像和一个自然语言陈述构成，二者相辅相成，共同提供了完整的定理信息。相比之下，传统的ATP任务主要依赖纯文本定理的陈述，限制了其表达的完整性和直观性。新的基准专为多模态定理证明设计，涵盖了Lean 4、Coq和Isabelle三种主流的形式化证明语言，具有良好的兼容性。

在具体实施上，该基准共包含大量几何定理，难度涵盖高中和大学竞赛等多个级别，内容横跨平面几何、三维几何和解析几何等多个领域。这一设计的核心在于帮助模型理解并翻译图文信息，从而构建出严谨的形式化定理。研究团队通过大量实验，揭示了模型在不同语言和任务中的表现差异，定位了当前多模态大模型在形式化定理证明上的核心瓶颈。

实验结果表明，当前最强大的模型在Lean 4语言上成功率仅为，而在生成Coq语言时表现出意想不到的良好，任务一的成功率达到了12.15%。这一现象的背后，研究者推测主要是得益于Coq的策略库更为成熟，使得数学资源能够更有效地供给给模型与命令式策略风格的学习。

随着题目难度的增加，模型的性能显著下降。在Lean 4的任务一中，模型在高中和大学竞赛级别问题上的平均成功率相对较低，分别为和。这表明，尽管模型在处理基本几何定理时具备一定能力，但在面对更为复杂的定理时，依然需要更多的学习和优化。

在对不同模型的错误分析中，研究发现基础性错误，例如变量定义及库导入的问题，明显高于其他模型。尤其是在Lean 4任务中的主要错误集中于无效或未完成的证明步骤，以及缺失前提或隐藏假设等方面。这显示出多模态大模型在逻辑推理方面面临的挑战，尤其是在基本语法规范的把握上存在显著困难。

进一步的实验还揭示了一种普遍现象：模型的形式化定理翻译能力相对较强，以Lean 4任务二为例，模型在进行多模态信息的理解与转译时，平均成功率达到了显著的水平，但在需要完整证明的任务一中，该数值骤降至低，显示出当前多模态大模型在构建严密证明方面的不足。

结合几何解题的实际情况，添加辅助线是一种常见且有效的策略。实验中发现，当题目难度上升时，需要辅助线的问题比例显著增加，而模型的尝试率也随之一同上升。模型在有效构造和利用辅助线推进证明的能力极为有限，由此导致包含辅助线的证明成功率极低。

通过这一系列研究，香港科技大学的团队不仅为多模态自动定理证明领域提供了一套系统化的评估基准，同时也为未来的研究指明了方向。这一基准的推出，将推动学术界在AI与数学领域交叉研究方面的深入探索，并为实现智能化数学解决方案奠定基础。