MMFormalizer: Мультимодальное автоформализирование в реальных условиях

Аннотация

Автоформализация, которая переводит математику на естественном языке в формальные утверждения для обеспечения машинного рассуждения, сталкивается с фундаментальными трудностями в реальных условиях из-за мультимодальной природы физического мира, где физика требует вывода скрытых ограничений (например, массы или энергии) из визуальных элементов. Для решения этой проблемы мы предлагаем MMFormalizer, который расширяет автоформализацию за пределы текста за счет интеграции адаптивного заземления с сущностями из реальных математических и физических областей. MMFormalizer рекурсивно строит формальные предложения из перцептивно заземленных примитивов посредством рекурсивного заземления и композиции аксиом, при этом адаптивное рекурсивное завершение гарантирует, что каждая абстракция поддерживается визуальными свидетельствами и закреплена в размерном или аксиоматическом обосновании. Мы оцениваем MMFormalizer на новом эталоне PhyX-AF, включающем 115 отобранных образцов из MathVerse, PhyX, Синтетической геометрии и Аналитической геометрии, охватывающих разнообразные мультимодальные задачи автоформализации. Результаты показывают, что передовые модели, такие как GPT-5 и Gemini-3-Pro, достигают наивысшей точности компиляции и семантической точности, причем GPT-5 превосходит в физических рассуждениях, в то время как геометрия остается наиболее сложной областью. В целом, MMFormalizer предоставляет масштабируемую основу для унифицированной мультимодальной автоформализации, связывая восприятие и формальное рассуждение. Насколько нам известно, это первый мультимодальный метод автоформализации, способный работать с классической механикой (производной от гамильтониана), а также с теорией относительности, квантовой механикой и термодинамикой. Более подробная информация доступна на странице нашего проекта: 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: Мультимодальное автоформализирование в реальных условиях

MMFormalizer: Multimodal Autoformalization in the Wild

Аннотация

Support