論文の概要: MMFormalizer: Multimodal Autoformalization in the Wild

• arxiv url: http://arxiv.org/abs/2601.03017v1
• Date: Tue, 06 Jan 2026 13:42:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-07 17:02:12.955934
• Title: MMFormalizer: Multimodal Autoformalization in the Wild
• Title（参考訳）: MMFormalizer:野生におけるマルチモーダルオートモーダル化
• Authors: Jing Xiong, Qi Han, Yunta Hsieh, Hui Shen, Huajian Xin, Chaofan Tao, Chenyang Zhao, Hengyuan Zhang, Taiqiang Wu, Zhen Zhang, Haochen Wang, Zhongwei Wan, Lingpeng Kong, Ngai Wong,
• Abstract要約: MMFormalizerは、適応グラウンドを現実の数学的および物理的ドメインのエンティティと統合することにより、テキスト以外の自動形式化を拡張する。 MMFormalizerを新しいベンチマークであるPhyX-AFで評価し,MathVerse,PhyX,Synthetic Geometry,Analytic Geometryから115個のキュレートされたサンプルを作成した。 その結果, GPT-5 と Gemini-3-Pro が最も高いコンパイル精度と意味的精度が得られ, GPT-5 は物理的推論に優れていた。
• 参考スコア（独自算出の注目度）: 79.24853896733154
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Autoformalization, which translates natural language mathematics into formal statements to enable machine reasoning, faces fundamental challenges in the wild due to the multimodal nature of the physical world, where physics requires inferring hidden constraints (e.g., mass or energy) from visual elements. To address this, we propose MMFormalizer, which extends autoformalization beyond text by integrating adaptive grounding with entities from real-world mathematical and physical domains. MMFormalizer recursively constructs formal propositions from perceptually grounded primitives through recursive grounding and axiom composition, with adaptive recursive termination ensuring that every abstraction is supported by visual evidence and anchored in dimensional or axiomatic grounding. We evaluate MMFormalizer on a new benchmark, PhyX-AF, comprising 115 curated samples from MathVerse, PhyX, Synthetic Geometry, and Analytic Geometry, covering diverse multimodal autoformalization tasks. Results show that frontier models such as GPT-5 and Gemini-3-Pro achieve the highest compile and semantic accuracy, with GPT-5 excelling in physical reasoning, while geometry remains the most challenging domain. Overall, MMFormalizer provides a scalable framework for unified multimodal autoformalization, bridging perception and formal reasoning. To the best of our knowledge, this is the first multimodal autoformalization method capable of handling classical mechanics (derived from the Hamiltonian), as well as relativity, quantum mechanics, and thermodynamics. More details are available on our project page: MMFormalizer.github.io
• Abstract（参考訳）: 自然言語数学を形式的ステートメントに翻訳して機械推論を可能にするオートフォーマル化は、物理世界のマルチモーダルな性質により、視覚的要素から隠れた制約(質量やエネルギーなど)を推論する必要があるため、自然界の根本的な課題に直面している。 そこで本研究では,現実の数学的・物理的領域の実体と適応的なグラウンドリングを統合することで,テキスト以外の自己形式化を拡張できるMMFormalizerを提案する。 MMFormalizer は、視覚的証拠によって全ての抽象が支持され、次元的または公理的な接地によって固定されることを保証する適応的再帰的終端(adaptive recursive termination)で、再帰的接地と公理的合成を通じて知覚的接地プリミティブから形式的命題を再帰的に構成する。 MMFormalizerをMathVerse,PhyX,Synthetic Geometry,Analytic Geometryから115個のキュレートされたサンプルからなる新しいベンチマークPhyX-AFで評価した。 その結果, GPT-5やGemini-3-Proのようなフロンティアモデルが最もコンパイル精度が高く, GPT-5は物理的推論に優れ, 幾何学は依然として最も困難な領域であることがわかった。 全体として、MMFormalizerは、統合マルチモーダルオートモーダル化、ブリッジング認識、フォーマル推論のためのスケーラブルなフレームワークを提供する。 我々の知る限りでは、これは古典力学(ハミルトン力学から派生した)や相対性理論、量子力学、熱力学を扱うことができる最初のマルチモーダル自己形式化法である。 詳細はプロジェクトのページにある。 MMFormalizer.github.io

関連論文リスト

• Learning Geometry: A Framework for Building Adaptive Manifold Models through Metric Optimization [8.201374511929538]
  本稿では,従来のパラメータ最適化を超越した機械学習のパラダイムを提案する。 既定位相を持つ多様体上の計量テンソル場を最適化することにより、モデル空間の幾何学的構造を動的に形成する。 この研究は、その幾何学とトポロジーを自律的に進化させることができる完全にダイナミックな「メタ・ラーナー」を構築するための確固たる基礎を築いた。
  論文  参考訳（メタデータ） (2025-10-30T01:53:32Z)
• Automated Formalization via Conceptual Retrieval-Augmented LLMs [19.328918823576153]
  CRAMFは概念駆動のRetrieval-Augmented Mathematical Formalizationフレームワークである。 概念定義知識ベースをMathlib4から自動構築するフレームワークを提案する。 miniF2F, ProofNet, そして新たに提案したAdvancedMathベンチマークでは, CRAMF を LLM ベースのオートフォーマライザにシームレスに統合できることが示されている。
  論文  参考訳（メタデータ） (2025-08-09T10:54:25Z)
• MM-Agent: LLM as Agents for Real-world Mathematical Modeling Problem [11.81434494801394]
  我々は,Large Language Models (LLMs) を用いた実世界の数学的モデリングのタスクを定式化する。 本稿では,オープンエンド問題解析,構造化モデル定式化,計算問題解決,レポート生成の4つの段階に,モデリングを分解する専門家主導のフレームワークMM-Agentを提案する。 MM-Agentはベースラインエージェントを著しく上回り、人間の専門家ソリューションよりも11.88%改善している。
  論文  参考訳（メタデータ） (2025-05-20T09:55:31Z)
• GeoMFormer: A General Architecture for Geometric Molecular Representation Learning [84.02083170392764]
  我々はこの目的を達成するためにGeoMFormerと呼ばれるトランスフォーマーに基づく新しい分子モデルを導入する。 我々は,GeoMFormerが,異なる型やスケールの不変タスクと同変タスクの両方において,高い性能を達成することを示す。
  論文  参考訳（メタデータ） (2024-06-24T17:58:13Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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