← 返回 2026-01-12

MMFormalizer：野外环境下的多模态自动形式化 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 📅 2026-01-06 👍 106 2026-07-13 08:35
几何推理 多模态学习 定理证明 物理推理 自动形式化
arXiv HuggingFace PDF

将视觉和文本数学物理问题转换为可验证的LEAN形式化代码

前置知识

自动形式化

自动形式化是将非形式化的数学或物理文本转换为机器可验证的形式语言（如LEAN、Isabelle/HOL、Coq）的过程。这些形式语言基于严格的逻辑系统，能够自动验证数学证明的正确性。例如，将牛顿第二定律F=ma转换为LEAN代码，使得计算机能够检查推导过程的逻辑一致性。这一过程涉及词法分析、语法解析、语义映射和类型检查等步骤，最终生成符合形式语言规范的代码。

本文核心任务就是将多模态的数学物理问题自动形式化，理解这一概念是理解整个研究框架的基础。

依赖类型理论

依赖类型理论是一种类型系统，其中类型可以依赖于值。例如，在标准类型系统中，数组类型Array可能只携带元素类型信息，但在依赖类型系统中，可以定义Vector(n, T)表示长度为n、元素类型为T的向量，这里n是一个运行时值。LEAN就是一种基于依赖类型理论的定理证明器和编程语言。依赖类型使得数学对象可以以构造性方式表示，证明作为计算对象存在，确保了数学表达式的类型正确性和语义一致性。

本文采用LEAN作为形式化目标语言，依赖类型理论是理解LEAN工作原理和论文方法中类型组合算子的关键。

递归基线

递归基线是指通过递归过程将高层抽象概念逐步分解为基础要素的推理方法。例如，在理解一个复杂几何形状（如正六棱柱）时，递归基线将其分解为六个矩形侧面和两个六边形底面，每个侧面又分解为四条边，每条边分解为两个顶点，最终终止于点这个基础要素。每一步分解都必须有视觉或文本证据支撑，确保每个抽象都有实际意义。这种方法保证了形式化的逐层可验证性和语义 groundedness。

递归基线是MMFormalizer的核心机制，理解它对于把握论文方法的创新性和有效性至关重要。

维度分析

维度分析是一种通过检查物理量的量纲（如长度L、时间T、质量M、电荷Q、温度Θ）来验证物理方程合理性的方法。例如，检查方程F=ma的量纲，验证其合理性。在形式化物理问题时，维度分析可以作为递归终止的条件：当物理量可以表示为基本量纲的幂次组合时，可以认为已经达到充分基线，无需继续分解。

维度分析是本文在物理领域递归终止的重要依据，也是理解论文如何处理经典力学、相对论、量子力学的基础。

Hamiltonian形式主义

Hamiltonian形式主义是经典力学的一种表述方式，使用广义坐标q和广义动量p来描述系统状态，系统的动力学由Hamilton函数H(q,p)通过Hamilton方程给出。与Newton形式主义相比，Hamiltonian形式主义更对称且易于推广到量子力学。论文中展示了如何从Hamiltonian出发，递归推导出牛顿三定律，这体现了形式化推理的递归构建过程。

论文以从Hamiltonian推导牛顿定律为例说明MMFormalizer的工作原理，理解Hamiltonian形式主义有助于把握这个案例。

研究动机

现有的自动形式化系统主要处理纯文本数学问题，但现实世界中的数学和物理问题本质上是多模态的，包含图像、公式和文本。以物理问题为例，牛顿定律中涉及的量（如质量、长度、时间）之间的关系不能仅通过逻辑推理获得，必须通过测量经验地确定。一个数学上自洽的系统必须通过显式的维度定义回溯到物理经验。现有系统缺乏从视觉元素推断隐藏约束的能力，例如从几何图形中推断等长边或角度关系，从物理场景中推断势能分布或电荷分布。这导致现有方法难以处理复杂的多模态推理任务，特别是在处理合成几何问题（如正六边形）和现代物理问题（如量子隧穿）时表现不佳。

本文的目标是本文的目标是提出一个统一的多模态自动形式化框架MMFormalizer，能够将视觉和文本输入（如图表、自然语言描述、物理场景）转换为机器可验证的形式化代码（特别是LEAN代码）。该框架需要能够递归地构建形式化命题，确保每个抽象都有视觉证据支撑，并能够在维度或公理层面实现递归终止。最终目标是桥接感知理解（视觉）和形式推理（逻辑），使模型能够处理包括经典力学、相对论、量子力学和热力学在内的广泛数学物理领域。

与已有工作不同的是，本文的独特切入角度在于将维度分析作为递归终止的判断依据，这是与现有自动形式化方法的本质区别。现有工作主要依赖预定义的词表或符号词库，而MMFormalizer采用依赖类型理论的维度嵌入机制，使得物理量的维度结构可以直接编码到类型系统中。此外，本文首次尝试在物理领域进行多模态自动形式化，涵盖经典力学（从Hamiltonian推导）、相对论（速度叠加）、量子力学（波函数衰减）和热力学等多个子领域，这是之前工作未曾涉及的。本文还引入了递归终止条件，防止无限制的分解导致计算爆炸，这一点在论文的失败案例研究中得到了重点说明。

核心方法

MMFormalizer的整体思路是将多模态自动形式化分解为三个递归阶段：递归基线、递归终止和公理组合。首先，从输入图像I出发，通过解析函数将其分解为场景图SceneGraph，包含基本视觉实体（点、线、面）及其空间关系。然后，为每个视觉实体分配初始语义假设，形成基线层L0。接着，通过递归基线过程RG: I 到 PropChain，增量式地构建形式化命题的依赖层次，其中每个命题的语义都基线于感知数据。在递归过程中，使用LeanSearch从mathlib和PhysLean中检索相关的定理和定义，并使用LLM选择最佳匹配。当命题达到基本维度（如长度、时间、质量）或基础公理时，递归终止。最后，通过类型组合算子Compose将所有子节点递归组合，构建完整的AxiomChain，确保每个命题都经过编译检查，验证其结构和逻辑有效性。

核心创新点在于引入维度作为递归终止的判断依据，这是与现有自动形式化方法的本质区别。现有方法要么依赖预定义的词表，要么采用启发式规则，而MMFormalizer采用依赖类型理论的维度嵌入机制，使得物理量的维度结构可以直接编码到类型系统中，确保所有物理表达式都是类型良好且维度一致的。另一个关键创新是递归基线机制，确保每个形式化抽象都有视觉证据支撑，这通过语义检查模块实现，验证每个形式化语句是否同时得到视觉和文本证据的支持。此外，MMFormalizer还集成了PhysLean搜索工具，允许模型检索和复用现有的物理定理和定义，这与之前几何领域的自动形式化工作形成对比。

方法步骤详情

MMFormalizer的工作流程包含以下步骤：第一步是视觉分解，解析函数parse: I 到 SceneGraph将输入图像分解为场景图，包含基本视觉实体和它们之间的关系Rel(V_t)。每个视觉实体vi被分配初始语义假设l_t，形成基线层L0。第二步是递归基线，通过映射map: (V_t, l_t) 到 L_t将每个视觉元素映射到公理空间，构建可验证的公理语句层次。在每一阶段，使用LeanSearch从mathlib和PhysLean中检索相关的定理和定义，使用嵌入和离线索引实现语义搜索。第三步是递归终止，当命题P_t满足Termination(P_t)时停止分解，Termination(P_t)定义为：如果p属于基本量纲集合D_t（如质量、长度、时间），则dim(p)；如果p属于基础公理集合A_t（如牛顿定律、守恒定律），则axiom(p)。第四步是公理组合，通过类型组合算子Compose将所有子节点递归组合为非叶子节点，确保维度结构和符号可操作性的同时，支持几何、物理和逻辑领域的统一推理。第五步是语义检查，对于每个图像-文本-公式三元组，检查器输出指示值（1表示语义接受，0表示拒绝），只有所有命题都被分配1时，链才被认为是有效的。

技术新颖性

技术新颖性体现在四个方面。第一，首次在物理领域实现多模态自动形式化，涵盖经典力学（从Hamiltonian推导牛顿定律）、相对论（速度叠加公式）、量子力学（隧穿效应波函数，其中波函数衰减形式包含质量、能量、势垒高度和普朗克常数等参数）和热力学等多个子领域。第二，引入维度作为递归终止的判断依据，这是与现有自动形式化方法的本质区别，维度基线机制确保每个抽象都有物理意义。第三，递归基线机制确保每个形式化抽象都有视觉证据支撑，语义检查模块验证多模态一致性。第四，集成PhysLean搜索工具，允许模型检索和复用现有的物理定理和定义，这是之前工作在几何领域未曾涉及的。此外，论文还提出了PHYX-AF基准，包含115个精心策划的样本，涵盖MathVerse、PhyX、Synthetic Geometry和Analytic Geometry，这是首个多模态自动形式化基准。

Conceptual dependency graph illustrating how Newton's three laws give rise to key structures in classical mechanics, including momentum, Hamiltonian formulation, phase space, and spacetime representations.
Figure 2: Conceptual dependency graph illustrating how Newton's three laws give rise to key structures in classical mechanics, including momentum, Hamiltonian formulation, phase space, and spacetime representations.
The pipeline overview consists of three stages: Recursive Grounding, identifying physical primitives (the red parts in the figure, e.g., the Hamiltonian or dimensional quantities) for Termination, and Axiom Composition.
Figure 3: The pipeline overview consists of three stages: Recursive Grounding, identifying physical primitives (the red parts in the figure, e.g., the Hamiltonian or dimensional quantities) for Termination, and Axiom Composition.

实验结果

实验结果表明，前沿模型在多模态推理方面表现更强。Gemini-3-Pro在MATHVERSE和ANALYTIC GEOMETRY上获得最高的编译准确率和语义准确率，而GPT-5在PHYX数据集上表现优异，特别是在包含量子力学和相对论问题的MODERN类别中，反映出更强的物理推理和基线能力。具体数字上，在MATHVERSE Plane Geometry上，GPT-5的编译准确率为24.0%，Gemini-3-Pro为76.0%；在PHYX Modern Physics上，GPT-5的编译准确率为71.4%，语义准确率为71.4%，而Gemini-3-Pro仅为14.3%。几何推理仍然具有挑战性，所有模型在SYNTHETIC GEOMETRY和ANALYTIC GEOMETRY子集上的准确率都显著较低，表明模型在准确理解具体长度和角度关系，以及泛化到训练分布之外的任务方面仍面临困难。即使在SYNTHETIC GEOMETRY Plane Geometry上，Gemini-3-Pro的编译准确率也只有33.3%，GPT-5为0.0%。最强大的开源模型Qwen3-VL-235B在物理领域或分布外合成几何任务上几乎无法解决问题。消融实验表明，移除检索到的参考代码可以提高模型在SYNTHETIC GEOMETRY设置下的性能，说明允许模型自由合成而非约束其输出空间可以显著增强其分布外泛化能力。不指定详细的终止条件会导致递归树过深和依赖图过大，最终导致合成过程失败。图像基线可以显著增强更具挑战性的设置下的性能，如包含相对论和量子力学的Modern Physics类别以及SYNTHETIC GEOMETRY。增加采样数量(pass@k)可以提高更难问题的性能，表明测试时扩展具有很大潜力。

Comparison across MATHVERSE, PHYX, SYNTHETIC GEOMETRY, and ANALYTIC GEOMETRY datasets. We report Compile accuracy, semantic correctness, and human verification results. The Modern category under PHYX includes problems from both quantum mechanics and relativity.
Table 1: Comparison across MATHVERSE, PHYX, SYNTHETIC GEOMETRY, and ANALYTIC GEOMETRY datasets. We report Compile accuracy, semantic correctness, and human verification results. The Modern category under PHYX includes problems from both quantum mechanics and relativity.
Ablation Study on the Model Components: Evaluating the Effect of Different Modifications on Performance.
Table 2: Ablation Study on the Model Components: Evaluating the Effect of Different Modifications on Performance.
Accuracy of Semantic Checking by Different LLMs, evaluated through human validation.
Table 3: Accuracy of Semantic Checking by Different LLMs, evaluated through human validation.
Geometric construction operators used during synthetic data generation.
Table 4: Geometric construction operators used during synthetic data generation.
Comparison of Termination Logic for Autoformalization in Mathematics and Physics Domains.
Table 5: Comparison of Termination Logic for Autoformalization in Mathematics and Physics Domains.
Multimodal autoformalization performance of five representative models across mathematical and physical domains, reported in terms of compilation accuracy (left) and human verification accuracy (right).
Figure 1: Multimodal autoformalization performance of five representative models across mathematical and physical domains, reported in terms of compilation accuracy (left) and human verification accuracy (right).
Distribution of Problem Types.
Figure 4: Distribution of Problem Types.
查看结构化数据
任务指标本文基线提升
MATHVERSE Plane Geometry (Image-Only) Compile Accuracy Gemini-3-Pro: 76.0% GPT-5: 24.0% Gemini-3-Pro比GPT-5提升52个百分点
PHYX Modern Physics (Image-Only) Compile Accuracy GPT-5: 71.4% Gemini-3-Pro: 14.3% GPT-5比Gemini-3-Pro提升57.1个百分点
PHYX Modern Physics (Image-Only) Semantic Accuracy GPT-5: 71.4% Gemini-3-Pro: 14.3% GPT-5比Gemini-3-Pro提升57.1个百分点
ANALYTIC GEOMETRY Plane Geometry (Image-Only) Compile Accuracy Gemini-3-Pro: 80.0% GPT-5: 40.0% Gemini-3-Pro比GPT-5提升40个百分点
SYNTHETIC GEOMETRY Plane Geometry (Image-Only) Compile Accuracy Gemini-3-Pro: 33.3% GPT-5: 0.0% Gemini-3-Pro表现最优，但整体准确率较低

局限与改进

作者承认的局限性包括：几何推理仍然具有挑战性，所有模型在SYNTHETIC GEOMETRY和ANALYTIC GEOMETRY子集上的准确率都显著较低，表明模型在准确理解具体长度和角度关系方面仍面临困难。开源模型与前沿模型之间存在显著性能差距，最强大的开源模型Qwen3-VL-235B在物理领域或分布外合成几何任务上几乎无法解决问题。消融实验表明，不指定详细的终止条件会导致递归树过深和依赖图过大，最终导致合成过程失败，如论文中的失败案例所示：在没有明确终止条件的情况下，递归分解导致8层684步分解，产生指数级计算增长。我自己观察到的局限性包括：论文中的消融实验样本量较小（总共只有约29个样本），可能不足以得出统计显著的结论。论文没有详细讨论计算效率，递归基线过程可能计算开销较大。论文没有提供端到端的误差分析，难以确定失败发生在哪个阶段（视觉分解、基线、终止或组合）。论文没有讨论模型对噪声的鲁棒性，而在实际应用中，图像可能包含各种噪声和失真。

独立分析的弱点

独立的弱点分析表明，MMFormalizer在处理复杂几何形状时表现不佳，例如需要递归组合复杂角度关系的正六边形，这需要定义编码几何约束的依赖类型，如等长边和角度构造。改进方向包括引入更强大的几何感知模块，能够直接从图像中提取精确的几何关系（如角度、长度比例），而不是仅仅依赖文本描述。另一个弱点是在处理分布外任务时性能下降显著，如在SYNTHETIC GEOMETRY中，模型需要合成预训练语料库中不存在的依赖类型和构造器。改进方向包括引入元学习机制，使模型能够快速适应新的几何构造模式，或者增强测试时采样策略（如pass@k）。第三个弱点是递归终止条件不够精确，可能导致过早终止或过度分解。改进方向包括引入更复杂的终止启发式，如结合维度分析和语义一致性检查，或者学习式终止策略，根据历史分解深度和成功率动态调整终止条件。

未来方向

作者提出的未来研究方向包括扩展到其他物理领域，如电磁学、热力学和流体力学，这将需要引入新的基线原语和公理。另一个方向是改进递归终止条件，使其更精确和高效，防止过深递归导致的计算爆炸。基于论文成果可延伸的方向包括将MMFormalizer应用于跨领域推理，如将几何问题转换为物理问题（例如，将静电场问题转换为几何等势线问题），或者将物理问题转换为几何问题（例如，将力学问题转换为几何路径问题）。还可以探索将MMFormalizer与现有的定理证明器（如自动化定理证明器或强化学习驱动的证明搜索）结合，构建端到端的形式化推理系统。另一个有趣的方向是探索多模态形式化的教育应用，例如帮助学生理解复杂的数学物理概念，或者生成可验证的数学物理教材。最后，可以探索将MMFormalizer扩展到其他领域，如化学（分子几何）、生物学（蛋白质折叠）或工程学（结构分析），这将需要引入新的基线原语和领域特定的形式化语言。

复现评估

复现评估表明，论文提供了PHYX-AF基准的详细描述和构建过程，包括数据来源、过滤标准和验证机制，这有助于其他研究者复现基准。论文还提供了合成几何生成管道的详细描述，包括构造算子、演绎闭包、最小依赖提取和数值验证，这使得其他研究者可以生成类似的合成数据。论文没有公开代码，但提供了足够的方法细节，使得其他研究者可以重新实现MMFormalizer框架。论文使用的模型（GPT-5、Gemini-3-Pro、Qwen3-VL-235B等）要么是商业API，要么是开源模型，这使得其他研究者可以使用相同的模型进行实验。论文没有提供计算资源的详细信息，但考虑到使用了大型多模态模型和递归基线过程，计算需求可能较高。论文提供了消融实验的详细描述，包括样本选择、实验设置和结果分析，这有助于其他研究者理解不同设计因素的影响。总体而言，论文的复现性较好，但代码未公开是一个限制。

论文图表

Figure A.7: A failed case. In the absence of explicit termination conditions, recursive decomposition of fundamental laws leads to infinite loops and spurious primitives, producing a dependency graph of 8 layers and 684 decomposition steps, and resulting in exponential computational growth.

图A.7展示了一个失败案例，在没有明确终止条件的情况下，基本定律的递归分解导致无限循环和虚假原语，产生8层684步分解的依赖图，导致指数级计算增长。图从左上角的根问题（静电场中的点电荷悬挂问题）开始，递归分解为多个节点，包括Electromagnetism、Mechanics、Geometry、Math等领域的概念，如Force、Velocity、ElectricField、LorentzForceLaw、Gravity、Mass、Trigonometry等。由于没有终止条件，递归过程不断分解，产生了大量虚假原语，导致计算爆炸。图中用红色节点表示过度分解，蓝色节点表示Mechanics相关的概念，绿色节点表示Math相关的概念。

这张图对理解论文的失败案例和递归终止的重要性至关重要，它直观地展示了没有明确终止条件时的灾难性后果，支持了论文中关于递归终止条件的设计选择。

Figure A.8: Synthetic Geometry Generation and Verification Pipeline. Symbolic pipeline for generating synthetic geometry problem instances, from construction and deduction to dependency extraction and verification.

图A.8展示了合成几何生成和验证管道，用于生成合成几何问题实例的符号管道，从构造和演绎到依赖提取和验证。图分为两个主要空间：构造空间和演绎空间。构造空间包括目标选择和依赖提取，演绎空间包括几何配置、符号演绎和演绎闭包。管道的最终阶段是验证，包括数值验证和可行性验证。图中还展示了数据流，从初始点采样开始，应用构造原语，添加定义谓词，触发演绎规则，推导关系，最终通过数值验证过滤无效实例。

这张图对理解论文的合成几何数据生成过程至关重要，它清晰地展示了生成管道的各个阶段和数据流向，有助于理解合成几何问题的构建和验证机制。

Figure A.9: Example Instantiation Trace for Synthetic Geometry Generation. An example showing how sampled points are expanded into a symbolic geometric configuration and yield a derived relation via Horn-style deduction.

图A.9展示了合成几何生成的实例化跟踪示例，说明采样的点如何扩展为符号几何配置，并通过Horn风格演绎产生推导关系。图从构造空间开始，采样初始点a、b、c（非共线），然后应用构造原语circumcenter（外心），生成点o。接着添加定义谓词，如coplanar(o, a, b, c)（共面）、cong(o, a, o, b)（距离相等）、cong(o, a, o, c)（距离相等）。然后进入演绎空间，触发演绎规则，如从cong(o, a, o, b)和ncoll(o, a, b)推导出eqangle6(o, a, b, o, b, a)（角度相等）。图中用不同颜色表示不同阶段，构造空间用蓝色，演绎空间用绿色，推导关系用红色。

这张图对理解论文的合成几何生成过程至关重要，它提供了一个具体的实例，展示了从初始点到最终推导关系的完整过程，有助于理解合成几何问题的构建机制。