MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?

要約

ジオメトリのような多数の定理は、しばしばマルチモーダル形式（例えば、図）で提示されます。
人間は、そのような設定での視覚的推論から利益を得て、図を使用して直感を得て証明プロセスを導きます。
現代のマルチモーダル大手言語モデル（MLLM）は、幅広い数学的問題を解決する際の顕著な能力を実証しています。
ただし、特にマルチモーダルドメインの自動定理プロバー（ATPS）としてのMLLMの可能性は、露出していないままです。
この論文では、マルチモーダル自動定理プローバーとしてこの役割を評価するために設計された新しいマルチモーダル、マルチレベル、およびマルチ言語ベンチマークであるマルチモーダル自動化された定理ベンチマーク（MATPベンチ）を紹介します。
MATPベンチは、高校、大学、競争レベルの数学から描かれた1056のマルチモーダル定理で構成されています。
これらのすべてのマルチモーダルの問題には、Lean 4、Coq、およびIsabelleの形式化が伴うため、ベンチマークは幅広い定理プロビングフレームワークと互換性があります。
MATPベンチでは、モデルが洗練された視覚的理解を、数学的知識の広範なスペクトルの習得と、正式な証明を生成するために厳密な象徴的推論を統合する必要があります。
MATPベンチを使用して、さまざまな高度なマルチモーダル言語モデルを評価します。
既存の方法は、限られた数のMATPベンチの問題を解決することしかできず、このベンチマークが自動定理証明に関する研究のためのオープンな課題をもたらすことを示しています。

要約(オリジナル)

Numerous theorems, such as those in geometry, are often presented in multimodal forms (e.g., diagrams). Humans benefit from visual reasoning in such settings, using diagrams to gain intuition and guide the proof process. Modern Multimodal Large Language Models (MLLMs) have demonstrated remarkable capabilities in solving a wide range of mathematical problems. However, the potential of MLLMs as Automated Theorem Provers (ATPs), specifically in the multimodal domain, remains underexplored. In this paper, we introduce the Multimodal Automated Theorem Proving benchmark (MATP-BENCH), a new Multimodal, Multi-level, and Multi-language benchmark designed to evaluate MLLMs in this role as multimodal automated theorem provers. MATP-BENCH consists of 1056 multimodal theorems drawn from high school, university, and competition-level mathematics. All these multimodal problems are accompanied by formalizations in Lean 4, Coq and Isabelle, thus making the benchmark compatible with a wide range of theorem-proving frameworks. MATP-BENCH requires models to integrate sophisticated visual understanding with mastery of a broad spectrum of mathematical knowledge and rigorous symbolic reasoning to generate formal proofs. We use MATP-BENCH to evaluate a variety of advanced multimodal language models. Existing methods can only solve a limited number of the MATP-BENCH problems, indicating that this benchmark poses an open challenge for research on automated theorem proving.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google