MMFormalizer: Multimodale Autoformalisering in de Praktijk

Samenvatting

Autoformalisering, die natuurlijketaalwiskunde vertaalt naar formele uitspraken om machineredenering mogelijk te maken, wordt in de praktijk geconfronteerd met fundamentele uitdagingen vanwege de multimodale aard van de fysieke wereld, waar de natuurkunde vereist dat verborgen beperkingen (bijvoorbeeld massa of energie) worden afgeleid uit visuele elementen. Om dit aan te pakken, stellen we MMFormalizer voor, dat autoformalisering uitbreidt voorbij tekst door adaptieve grounding te integreren met entiteiten uit de wiskundige en natuurkundige domeinen van de echte wereld. MMFormalizer construeert recursief formele proposities vanuit perceptueel verankerde primitieven door recursieve grounding en axiomasamenstelling, waarbij adaptieve recursieve beëindiging ervoor zorgt dat elke abstractie wordt ondersteund door visueel bewijs en verankerd is in dimensionale of axiomatische grounding. We evalueren MMFormalizer op een nieuwe benchmark, PhyX-AF, bestaande uit 115 geselecteerde samples van MathVerse, PhyX, Synthetische Meetkunde en Analytische Meetkunde, die diverse multimodale autoformaliseringstaken bestrijken. Resultaten tonen aan dat frontiermodellen zoals GPT-5 en Gemini-3-Pro de hoogste compilatie- en semantische nauwkeurigheid bereiken, waarbij GPT-5 uitblinkt in fysisch redeneren, terwijl meetkunde het meest uitdagende domein blijft. Over het algemeen biedt MMFormalizer een schaalbaar raamwerk voor verenigde multimodale autoformalisering, dat perceptie en formeel redeneren verbindt. Voor zover wij weten, is dit de eerste multimodale autoformaleringsmethode die klassieke mechanica (afgeleid van de Hamiltoniaan), evenals relativiteit, kwantummechanica en thermodynamica aankan. Meer details zijn beschikbaar op onze projectpagina: 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: Multimodale Autoformalisering in de Praktijk

MMFormalizer: Multimodal Autoformalization in the Wild

Samenvatting

Support