MMFormalizer: Multimodal Autoformalization in the Wild

TL;DR

MMFormalizer presents a unified multimodal autoformalization framework that recursively grounds perceptual inputs into verifiable Lean propositions by weaving together visual decomposition, dimensional grounding, and axiom composition. The approach relies on a three-layer pipeline—Recursive Grounding, Axiom Composition, and Semantic Checking—coupled with LeanSearch-enabled retrieval to connect perceptual primitives to formal lemmas. A new PhyX-AF benchmark is introduced to evaluate cross-domain autoformalization in the wild, showing frontier models like GPT-5 and Gemini-3-Pro achieve the best compile and semantic accuracy, especially in physical domains, while geometry remains challenging. The work demonstrates the potential to unify perception with formal reasoning across classical mechanics, relativity, quantum mechanics, and thermodynamics, while also identifying termination and grounding as key bottlenecks for scalable, reliable multimodal autoformalization.

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

Figures (13)

• 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).
• 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.
• 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. The blue parts in the figure indicate the compiler checking process. The green part indicates the formal statements we retrieved from the dependency library.
• Figure 4: Distribution of Problem Types.
• Figure A.1: A Regular Hexagonal Prism.