MMFormalizer: Autoformalización Multimodal en Contextos Reales

Resumen

La autoformalización, que traduce matemáticas en lenguaje natural a enunciados formales para permitir el razonamiento automático, enfrenta desafíos fundamentales en entornos no controlados debido a la naturaleza multimodal del mundo físico, donde la física requiere inferir restricciones ocultas (por ejemplo, masa o energía) a partir de elementos visuales. Para abordar esto, proponemos MMFormalizer, que extiende la autoformalización más allá del texto integrando una fundamentación adaptativa con entidades de dominios matemáticos y físicos del mundo real. MMFormalizer construye recursivamente proposiciones formales a partir de primitivas perceptualmente fundamentadas mediante una fundamentación recursiva y composición axiomática, con una terminación recursiva adaptativa que garantiza que cada abstracción esté respaldada por evidencia visual y anclada en una fundamentación dimensional o axiomática. Evaluamos MMFormalizer en un nuevo benchmark, PhyX-AF, que comprende 115 muestras seleccionadas de MathVerse, PhyX, Geometría Sintética y Geometría Analítica, cubriendo diversas tareas de autoformalización multimodal. Los resultados muestran que modelos de vanguardia como GPT-5 y Gemini-3-Pro logran la mayor precisión de compilación y semántica, con GPT-5 destacándose en el razonamiento físico, mientras que la geometría sigue siendo el dominio más desafiante. En general, MMFormalizer proporciona un marco escalable para la autoformalización multimodal unificada, tendiendo un puente entre la percepción y el razonamiento formal. Hasta donde sabemos, este es el primer método de autoformalización multimodal capaz de manejar mecánica clásica (derivada del Hamiltoniano), así como relatividad, mecánica cuántica y termodinámica. Más detalles están disponibles en nuestra página del proyecto: 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: Autoformalización Multimodal en Contextos Reales

MMFormalizer: Multimodal Autoformalization in the Wild

Resumen

Support