The Year in AI Papers
The year/Independent research

Paper 2601.03017

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, et al.

Published
Jan 2026
Research lab
Independent
Citations
0
GitHub
Not linked

01 In brief

Summary

The paper introduces MMFORMALIZER, a framework for multimodal autoformalization that translates natural language and visual inputs into formal LEAN statements.

It addresses challenges in grounding physical concepts by using recursive grounding and dimensional analysis, with adaptive termination to ensure visual evidence supports abstractions.

The authors introduce PHYX-AF, a benchmark of 115 curated samples from MathVerse, PhyX, Synthetic Geometry, and Analytic Geometry, covering mathematics and physics including classical mechanics, relativity, quantum mechanics, and thermodynamics.

Evaluations show frontier models like 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.

Ablation studies highlight the importance of termination conditions, image grounding, and pass@k sampling.

The framework is the first to handle classical mechanics derived from the Hamiltonian, as well as relativity, quantum mechanics, and thermodynamics.

02 From the paper

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