MMFormalizer: Autoformalizzazione Multimodale in Contesti Reali

Abstract

L'autoformalizzazione, che traduce la matematica in linguaggio naturale in enunciati formali per abilitare il ragionamento automatico, affronta sfide fondamentali in contesti reali a causa della natura multimodale del mondo fisico, dove la fisica richiede di inferire vincoli nascosti (ad esempio, massa o energia) da elementi visivi. Per affrontare ciò, proponiamo MMFormalizer, che estende l'autoformalizzazione oltre il testo integrando un ancoraggio adattivo con entità dei domini matematici e fisici del mondo reale. MMFormalizer costruisce ricorsivamente proposizioni formali da primitive perceptualmente ancorate attraverso l'ancoraggio ricorsivo e la composizione assiomatica, con una terminazione ricorsiva adattiva che garantisce che ogni astrazione sia supportata da evidenza visiva e ancorata in basi dimensionali o assiomatiche. Valutiamo MMFormalizer su un nuovo benchmark, PhyX-AF, comprendente 115 campioni curati da MathVerse, PhyX, Geometria Sintetica e Geometria Analitica, coprendo diverse attività di autoformalizzazione multimodale. I risultati mostrano che modelli all'avanguardia come GPT-5 e Gemini-3-Pro raggiungono la più alta accuratezza di compilazione e semantica, con GPT-5 eccellente nel ragionamento fisico, mentre la geometria rimane il dominio più impegnativo. Nel complesso, MMFormalizer fornisce un framework scalabile per l'autoformalizzazione multimodale unificata, colmando il divario tra percezione e ragionamento formale. Per quanto a nostra conoscenza, questo è il primo metodo di autoformalizzazione multimodale in grado di gestire la meccanica classica (derivata dall'Hamiltoniana), così come la relatività, la meccanica quantistica e la termodinamica. Maggiori dettagli sono disponibili sulla nostra pagina progetto: 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

MMFormalizer: Autoformalizzazione Multimodale in Contesti Reali

MMFormalizer: Multimodal Autoformalization in the Wild

Abstract

Support