MMFormalizer: Multimodal Autoformalization in the Wild
作者: 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.CL
发布日期: 2026-01-06
备注: Technical Report
💡 一句话要点
MMFormalizer：提出一种多模态自动形式化方法，解决物理世界中数学推理的挑战。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 多模态学习 自动形式化 物理推理 几何推理 视觉感知 知识表示 递归神经网络
📋 核心要点
- 现有自动形式化方法难以处理物理世界的多模态特性，无法从视觉信息中推断隐藏的物理约束。
- MMFormalizer通过递归指代和公理组合，将视觉感知与形式化命题构建相结合，实现多模态自动形式化。
- 在PhyX-AF基准测试中，MMFormalizer展现了良好的性能，尤其是在物理推理方面，但几何问题仍然具有挑战性。
📝 摘要（中文）
自动形式化旨在将自然语言数学描述转化为形式化语句，从而支持机器推理。然而，现实世界中的物理问题具有多模态特性，需要从视觉元素中推断隐藏约束（如质量或能量），这给自动形式化带来了根本性挑战。为了解决这个问题，我们提出了MMFormalizer，它通过整合自适应的实体指代，将自动形式化扩展到文本之外，使其能够处理真实世界中的数学和物理领域。MMFormalizer通过递归指代和公理组合，从感知到的原始信息中递归地构建形式化命题，并利用自适应递归终止机制确保每个抽象都得到视觉证据的支持，并锚定于维度或公理基础。我们在一个新的基准测试PhyX-AF上评估了MMFormalizer，该基准包含来自MathVerse、PhyX、Synthetic Geometry和Analytic Geometry的115个精选样本，涵盖了各种多模态自动形式化任务。结果表明，GPT-5和Gemini-3-Pro等前沿模型取得了最高的编译和语义准确率，其中GPT-5在物理推理方面表现出色，而几何仍然是最具挑战性的领域。总而言之，MMFormalizer提供了一个可扩展的统一多模态自动形式化框架，弥合了感知和形式推理之间的差距。据我们所知，这是第一个能够处理经典力学（源自哈密顿量）、相对论、量子力学和热力学的多模态自动形式化方法。
🔬 方法详解
问题定义：论文旨在解决在多模态场景下，特别是涉及物理和几何问题的自动形式化问题。现有方法主要集中于文本输入，无法有效利用视觉信息来推断隐藏的物理约束，例如质量、能量等，导致在处理真实世界问题时性能受限。
核心思路：论文的核心思路是将视觉感知与形式化推理相结合，通过自适应的实体指代，从视觉信息中提取相关的物理和几何实体，并将其与形式化命题进行关联。通过递归地构建形式化命题，并利用公理进行组合，最终实现多模态场景下的自动形式化。
技术框架：MMFormalizer的技术框架主要包含以下几个阶段：1) 视觉感知：从图像中提取相关的物理和几何实体。2) 递归指代：将提取的实体与形式化命题进行关联，并递归地构建更复杂的命题。3) 公理组合：利用物理和几何领域的公理，对构建的命题进行组合和推理。4) 自适应递归终止：根据视觉证据和维度/公理基础，自适应地决定递归过程的终止条件。
关键创新：论文的关键创新在于提出了一个统一的多模态自动形式化框架，能够处理经典力学、相对论、量子力学和热力学等复杂物理问题。通过递归指代和公理组合，实现了视觉感知与形式化推理的有效结合，弥合了感知和形式推理之间的差距。
关键设计：MMFormalizer的关键设计包括：1) 自适应的实体指代机制，能够根据上下文信息选择合适的实体进行指代。2) 递归构建形式化命题的方法，能够处理复杂的物理和几何关系。3) 基于视觉证据和维度/公理基础的自适应递归终止条件，避免了过度抽象和无效推理。
🖼️ 关键图片
📊 实验亮点
MMFormalizer在PhyX-AF基准测试中取得了显著成果，GPT-5和Gemini-3-Pro等前沿模型表现出色，尤其GPT-5在物理推理方面表现突出。该方法是首个能够处理经典力学、相对论、量子力学和热力学的多模态自动形式化方法，为相关领域的研究提供了新的思路。
🎯 应用场景
MMFormalizer可应用于智能教育、科学研究、机器人等领域。例如，在智能教育中，它可以帮助学生理解物理和几何概念，并自动生成习题解答。在科学研究中，它可以辅助科学家进行物理建模和仿真。在机器人领域，它可以使机器人具备更强的环境感知和推理能力。
📄 摘要（原文）
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