MMFormalizer: Autoformalização Multimodal em Contextos Reais
MMFormalizer: Multimodal Autoformalization in the Wild
January 6, 2026
Autores: 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.AI
Resumo
A autoformalização, que traduz matemática em linguagem natural para declarações formais para permitir raciocínio automatizado, enfrenta desafios fundamentais em ambientes reais devido à natureza multimodal do mundo físico, onde a física exige inferir restrições ocultas (por exemplo, massa ou energia) a partir de elementos visuais. Para resolver isso, propomos o MMFormalizer, que estende a autoformalização para além do texto, integrando uma ancoragem adaptativa com entidades de domínios matemáticos e físicos do mundo real. O MMFormalizer constrói recursivamente proposições formais a partir de primitivas perceptualmente ancoradas através de ancoragem recursiva e composição axiomática, com terminação recursiva adaptativa garantindo que toda abstração seja suportada por evidência visual e ancorada em fundamentação dimensional ou axiomática. Avaliamos o MMFormalizer em um novo benchmark, o PhyX-AF, compreendendo 115 amostras curadas do MathVerse, PhyX, Geometria Sintética e Geometria Analítica, abrangendo diversas tarefas de autoformalização multimodal. Os resultados mostram que modelos de fronteira, como o GPT-5 e o Gemini-3-Pro, alcançam a maior precisão de compilação e semântica, com o GPT-5 se destacando no raciocínio físico, enquanto a geometria permanece como o domínio mais desafiador. No geral, o MMFormalizer fornece uma estrutura escalável para autoformalização multimodal unificada, conectando percepção e raciocínio formal. Até onde sabemos, este é o primeiro método de autoformalização multimodal capaz de lidar com mecânica clássica (derivada do Hamiltoniano), bem como relatividade, mecânica quântica e termodinâmica. Mais detalhes estão disponíveis em nossa página do projeto: MMFormalizer.github.io.
English
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