論文の概要: 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 の限られた数しか解けず、このベンチマークは自動定理証明の研究にオープンな課題をもたらすことを示している。

関連論文リスト

• MM-PRM: Enhancing Multimodal Mathematical Reasoning with Scalable Step-Level Supervision [27.571090189791303]
  完全に自動化されたスケーラブルなフレームワーク内でトレーニングされたプロセス報酬モデルであるMM-PRMを提案する。 我々はまず,多様な数学的推論データに基づいて訓練された強力なマルチモーダルモデルMM-Policyを構築した。 人間のラベル付けなしで700万以上のステップレベルのアノテーションを生成します。
  論文  参考訳（メタデータ） (2025-05-19T17:55:08Z)
• 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)
• One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMs [57.48325300739872]
  証明生成のための数学的大規模言語モデルを活用することは、LLM研究の基本的なトピックである。 現状のLCMが証明できる能力は、学習中に関連する証明プロセスに遭遇したかどうかに大きく依存していると論じる。 人間の数学教育で一般的に用いられる「反例による防御」の教育的手法に触発されて,我々の研究は,反例を通して数学的推論と証明を行うLLMの能力を高めることを目的としている。
  論文  参考訳（メタデータ） (2025-02-12T02:01:10Z)
• Can MLLMs Reason in Multimodality? EMMA: An Enhanced MultiModal ReAsoning Benchmark [73.27104042215207]
  EMMAは,数学,物理,化学,コーディングにまたがる有機マルチモーダル推論を対象とするベンチマークである。 EMMAタスクは、各モードで独立に推論することで対処できない高度なクロスモーダル推論を要求する。 EMMA上での最先端MLLMの評価は、複雑なマルチモーダルおよびマルチステップ推論タスクの処理において、重大な制限を生じさせる。
  論文  参考訳（メタデータ） (2025-01-09T18:55:52Z)
• Progressive Multimodal Reasoning via Active Retrieval [64.74746997923967]
  多段階多モーダル推論タスクは、大規模言語モデル(MLLM)に重大な課題をもたらす 本稿では,MLLMの推論能力の向上を目的とした汎用フレームワークAR-MCTSを提案する。 我々は,AR-MCTSがサンプリングの多様性と精度を最適化し,信頼性の高いマルチモーダル推論を実現することを示す。
  論文  参考訳（メタデータ） (2024-12-19T13:25:39Z)
• MathScape: Evaluating MLLMs in multimodal Math Scenarios through a Hierarchical Benchmark [29.9945601202065]
  我々は,視覚情報とテキスト情報の組み合わせの理解と適用を強調する新しいベンチマークであるMathScapeを提案する。 MathScapeは、MLLMの理論的理解と応用能力を評価し、写真に基づく数学問題シナリオを評価するように設計されている。 我々は11の高度MLLMに対して多次元評価を行い、最も洗練されたモデルでさえベンチマークが困難であることを明らかにした。
  論文  参考訳（メタデータ） (2024-08-14T13:23:43Z)
• Needle In A Multimodal Haystack [79.81804334634408]
  本稿では,従来のMLLMの長大なマルチモーダル文書の理解能力を評価するために設計された,最初のベンチマークを示す。 我々のベンチマークには、マルチモーダル検索、カウント、推論の3種類の評価タスクが含まれている。 既存のモデルには、これらのタスク、特に視覚中心の評価において、改善の余地がまだ残っていることを観察する。
  論文  参考訳（メタデータ） (2024-06-11T13:09:16Z)
• math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories [10.416375584563728]
  本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。 我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
  論文  参考訳（メタデータ） (2023-10-25T23:54:04Z)
• A Survey on Multimodal Large Language Models [71.63375558033364]
  GPT-4Vで表されるマルチモーダル大言語モデル(MLLM)は、新たな研究ホットスポットとなっている。 本稿では,MLLMの最近の進歩を追跡・要約することを目的とする。
  論文  参考訳（メタデータ） (2023-06-23T15:21:52Z)
• Multimodal Chain-of-Thought Reasoning in Language Models [94.70184390935661]
  言語(テキスト)と視覚(画像)のモダリティを2段階のフレームワークに組み込んだマルチモーダルCoTを提案する。 その結果,ScienceQA と A-OKVQA のベンチマークは,提案手法の有効性を示した。
  論文  参考訳（メタデータ） (2023-02-02T07:51:19Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。