MMFormalizer: Multimodal Autoformalization in the Wild

TL;DR

MMFormalizer introduces a novel multimodal autoformalization framework that integrates visual perception with formal reasoning, enabling the translation of real-world multimodal data into formal mathematical statements across diverse physics domains.

Contribution

It extends autoformalization to multimodal inputs, recursively constructs formal propositions from perceptual primitives, and evaluates on a new benchmark, demonstrating capabilities in complex physical reasoning.

Findings

GPT-5 achieves high accuracy in physical reasoning tasks.

Geometry remains the most challenging domain.

First method to handle classical mechanics, relativity, quantum mechanics, and thermodynamics multimodally.

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