将物理视觉信息转化为形式化数学命题,实现跨模态推理。
MMFormalizer: Multimodal Autoformalization in the Wild
- 通过视觉感知构建形式化命题,递归融合实体与公理
- 在115个样本上,GPT-5在物理推理中表现最优
- 首个支持经典力学、相对论等多领域跨模态形式化的方法
自动形式化将自然语言数学转化为可机器推理的形式语句,但在现实世界中因多模态特性面临挑战,如需从视觉元素中推断隐藏约束(如质量或能量)。为此,我们提出MMFormalizer,突破文本限制,整合真实数学物理领域的实体进行自适应定位。该方法通过递归定位与公理组合,从感知基础单元构建形式命题,并以自适应终止机制确保每层抽象均有视觉证据支撑,且锚定于量纲或公理体系。我们在新基准PhyX-AF上评估,该数据集包含来自MathVerse、PhyX、合成几何与解析几何的115个精选样本,涵盖多样化多模态自动形式化任务。结果表明,前沿模型如GPT-5和Gemini-3-Pro在编译与语义准确性上表现最佳,其中GPT-5在物理推理中更优,而几何仍是最大挑战。总体而言,MMFormalizer提供了一个可扩展的统一框架,连接感知与形式推理。据我们所知,这是首个能处理经典力学(源自哈密顿量)、相对论、量子力学及热力学的多模态自动形式化方法。
原文摘要 · Abstract (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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。