MMFormalizer: Multimodale Autoformalisierung in der Praxis

papers.abstract

Die Autoformalisierung, die natürliche mathematische Sprache in formale Aussagen übersetzt, um maschinelles Schließen zu ermöglichen, steht in der Praxis vor grundlegenden Herausforderungen aufgrund der multimodalen Natur der physikalischen Welt, in der die Physik das Ablegen versteckter Randbedingungen (z.B. Masse oder Energie) aus visuellen Elementen erfordert. Um dies zu adressieren, schlagen wir MMFormalizer vor, das die Autoformalisierung über Text hinaus erweitert, indem es adaptive Verankerung mit Entitäten aus realen mathematischen und physikalischen Domänen integriert. MMFormalizer konstruiert rekursiv formale Aussagen aus wahrnehmungsbasierten Primitiven durch rekursive Verankerung und Axiomkomposition, wobei adaptiver rekursiver Abbruch sicherstellt, dass jede Abstraktion durch visuelle Evidenz gestützt und in dimensionaler oder axiomatischer Verankerung verankert ist. Wir evaluieren MMFormalizer anhand eines neuen Benchmarks, PhyX-AF, der 115 kuratierte Beispiele aus MathVerse, PhyX, Synthetischer Geometrie und Analytischer Geometrie umfasst und verschiedene multimodale Autoformalisierungsaufgaben abdeckt. Die Ergebnisse zeigen, dass Spitzenmodelle wie GPT-5 und Gemini-3-Pro die höchste Kompilierungs- und semantische Genauigkeit erreichen, wobei GPT-5 im physikalischen Schließen hervorsticht, während Geometrie die herausforderndste Domäne bleibt. Insgesamt bietet MMFormalizer einen skalierbaren Rahmen für vereinheitlichte multimodale Autoformalisierung, der Wahrnehmung und formales Schließen verbindet. Nach unserem Wissen ist dies die erste multimodale Autoformalisierungsmethode, die klassische Mechanik (abgeleitet vom Hamilton-Formalismus), sowie Relativitätstheorie, Quantenmechanik und Thermodynamik verarbeiten kann. Weitere Details sind auf unserer Projektseite verfügbar: 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 Autoformalisierung in der Praxis

MMFormalizer: Multimodal Autoformalization in the Wild

papers.abstract

Support