MMFormalizer : Autoformalisation multimodale en contexte réel

papers.abstract

L'autoformalisation, qui traduit les mathématiques en langage naturel en énoncés formels pour permettre le raisonnement machine, est confrontée à des défis fondamentaux dans des conditions réelles en raison de la nature multimodale du monde physique, où la physique nécessite d'inférer des contraintes cachées (par exemple, la masse ou l'énergie) à partir d'éléments visuels. Pour y remédier, nous proposons MMFormalizer, qui étend l'autoformalisation au-delà du texte en intégrant un ancrage adaptatif avec des entités issues des domaines mathématiques et physiques du monde réel. MMFormalizer construit récursivement des propositions formelles à partir de primitives ancrées perceptuellement via un ancrage récursif et une composition d'axiomes, avec une terminaison récursive adaptative garantissant que chaque abstraction est étayée par des preuves visuelles et ancrée dans un fondement dimensionnel ou axiomatique. Nous évaluons MMFormalizer sur un nouveau benchmark, PhyX-AF, comprenant 115 échantillons sélectionnés issus de MathVerse, PhyX, Géométrie Synthétique et Géométrie Analytique, couvrant diverses tâches d'autoformalisation multimodale. Les résultats montrent que les modèles de pointe tels que GPT-5 et Gemini-3-Pro atteignent la plus haute exactitude de compilation et sémantique, GPT-5 excellant dans le raisonnement physique, tandis que la géométrie reste le domaine le plus difficile. Globalement, MMFormalizer fournit un cadre évolutif pour une autoformalisation multimodale unifiée, faisant le lien entre la perception et le raisonnement formel. À notre connaissance, il s'agit de la première méthode d'autoformalisation multimodale capable de traiter la mécanique classique (dérivée du Hamiltonien), ainsi que la relativité, la mécanique quantique et la thermodynamique. Plus de détails sont disponibles sur notre page projet : 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 : Autoformalisation multimodale en contexte réel

MMFormalizer: Multimodal Autoformalization in the Wild

papers.abstract

Support