MMFormalizer: 実世界におけるマルチモーダル自動形式化

MMFormalizer: Multimodal Autoformalization in the Wild

January 6, 2026

著者: 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

cs.AI

要旨

自然言語の数学を形式的命題に翻訳し機械推論を可能とする自動形式化（Autoformalization）は、現実世界のマルチモーダル性により根本的課題に直面している。物理現象では視覚要素から質量やエネルギーといった暗黙の制約を推論する必要があるためである。この課題に対処するため、我々は現実世界の数学・物理領域の実体を適応的グラウンディングにより統合し、自動形式化をテキスト超えて拡張するMMFormalizerを提案する。本手法は、知覚的に接地された原始要素から再帰的グラウンディングと公理合成によって形式的命題を再帰的に構築し、適応的再帰終了機構により全ての抽象化が視覚的証拠に支えられ、次元的または公理的な基盤に固定されることを保証する。評価ではMathVerse、PhyX、合成幾何学、解析幾何学から精選した115サンプルからなる新規ベンチマークPhyX-AFを構築し、多様なマルチモーダル自動形式化タスクを網羅した。結果ではGPT-5やGemini-3-Proといった先進モデルが最高のコンパイル精度と意味精度を達成し、GPT-5は物理推論で優位性を示した一方、幾何学が最も困難な領域であることが示された。全体としてMMFormalizerは、知覚と形式的推論を橋渡しする統合的なマルチモーダル自動形式化のスケーラブルな枠組みを提供する。我々の知る限り、古典力学（ハミルトニアン由来）に加え、相対論・量子力学・熱力学を扱える初のマルチモーダル自動形式化手法である。詳細はプロジェクトページMMFormalizer.github.ioで公開されている。

English

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