論文の概要: MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
- arxiv url: http://arxiv.org/abs/2506.06034v1
- Date: Fri, 06 Jun 2025 12:33:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-09 17:28:43.471117
- Title: MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
- Title（参考訳）: MATP-BENCH:MLLMはマルチモーダル問題のための良い自動定理プロバーになれるか?
- Authors: Zhitao He, Zongwei Lyu, Dazhong Chen, Dadi Guo, Yi R. Fung,
- Abstract要約: MATP-BENCH(Multimodal Automated Theorem Proving benchmark)を導入する。
MATP-BENCHは、高校、大学、および競争レベルの数学から引き出された1056のマルチモーダル定理からなる。
MATP-BENCHを用いて、様々な高度なマルチモーダル言語モデルを評価する。
- 参考スコア（独自算出の注目度）: 4.492392159047302
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 幾何的定理のような多くの定理は、しばしばマルチモーダル形式(例えば図形)で表される。
人間はこのような設定での視覚的推論の恩恵を受け、図を使って直観を得、証明プロセスを導く。
現代のマルチモーダル大言語モデル(MLLM)は、幅広い数学的問題を解く際、顕著な能力を示した。
しかし、自動定理プローバー(ATPs)としてのMLLMのポテンシャルは、特にマルチモーダル領域において未解明のままである。
本稿では,MATP-BENCH(Multimodal Automated Theorem Proving benchmark)を紹介する。
MATP-BENCHは、高校、大学、および競争レベルの数学から引き出された1056のマルチモーダル定理からなる。
これらのマルチモーダル問題はLean 4、Coq、Isabelleの形式化が伴うため、ベンチマークは幅広い定理証明フレームワークと互換性がある。
MATP-BENCHは、数学的知識の幅広いスペクトルと厳密なシンボリック推論の熟達と洗練された視覚的理解を統合するモデルを必要とし、形式的な証明を生成する。
MATP-BENCHを用いて、様々な高度なマルチモーダル言語モデルを評価する。
既存の手法は MATP-BENCH の限られた数しか解けず、このベンチマークは自動定理証明の研究にオープンな課題をもたらすことを示している。
関連論文リスト
- MV-MATH: Evaluating Multimodal Math Reasoning in Multi-Visual Contexts [34.972503583614674]
MV-MATHは,2,009の高次数問題からなる厳密にキュレートされたデータセットである。
それぞれの問題は、K-12シナリオから派生したテキストでインターリーブされた複数の画像を統合し、詳細なアノテーションで富む。
MV-MATHには、複数の選択、自由形式、多段階の質問が含まれており、3つの困難レベルにわたる11の主題領域をカバーしている。
我々は,マルチ視覚数学におけるMLLMの課題が,MV-MATH上での人間の能力に比較してかなりの性能差があることを観察した。
論文 参考訳（メタデータ） (2025-02-28T07:50:36Z) - Can MLLMs Reason in Multimodality? EMMA: An Enhanced MultiModal ReAsoning Benchmark [73.27104042215207]
EMMAは,数学,物理,化学,コーディングにまたがる有機マルチモーダル推論を対象とするベンチマークである。
EMMAタスクは、各モードで独立に推論することで対処できない高度なクロスモーダル推論を要求する。
EMMA上での最先端MLLMの評価は、複雑なマルチモーダルおよびマルチステップ推論タスクの処理において、重大な制限を生じさせる。
論文 参考訳（メタデータ） (2025-01-09T18:55:52Z) - Needle In A Multimodal Haystack [79.81804334634408]
本稿では,従来のMLLMの長大なマルチモーダル文書の理解能力を評価するために設計された,最初のベンチマークを示す。
我々のベンチマークには、マルチモーダル検索、カウント、推論の3種類の評価タスクが含まれている。
既存のモデルには、これらのタスク、特に視覚中心の評価において、改善の余地がまだ残っていることを観察する。
論文 参考訳（メタデータ） (2024-06-11T13:09:16Z) - A Survey on Multimodal Large Language Models [71.63375558033364]
GPT-4Vで表されるマルチモーダル大言語モデル(MLLM)は、新たな研究ホットスポットとなっている。
本稿では,MLLMの最近の進歩を追跡・要約することを目的とする。
論文 参考訳（メタデータ） (2023-06-23T15:21:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。