MMFormalizer: 실제 환경에서의 다중 양식 자동 형식화

초록

자연어 수학을 형식적 명제로 변환하여 기계 추론을 가능하게 하는 자동형식화는 물리적 세계의 다중모달적 특성으로 인해 현실 적용에 근본적 어려움을 직면합니다. 특히 물리학 분야에서는 시각 요소에서 질량이나 에너지와 같은 숨겨진 제약 조건을 추론해야 합니다. 이를 해결하기 위해 우리는 실제 수학 및 물리 영역의 개체를 적응적 접지와 통합하여 자동형식화를 텍스트를 넘어 확장하는 MMFormalizer를 제안합니다. MMFormalizer는 지각적으로 접지된 기본 요소로부터 재귀적 접지와 공리 구성을 통해 형식적 명제를 재귀적으로 구성하며, 적응적 재귀 종료를 통해 모든 추상화가 시각적 증거에 기반하고 차원적 또는 공리적 접지에 고정되도록 합니다. 우리는 MathVerse, PhyX, Synthetic Geometry, Analytic Geometry에서 선별한 115개 샘플로 구성된 새로운 벤치마크 PhyX-AF에서 MMFormalizer를 평가하며, 다양한 다중모달 자동형식화 작업을 포괄합니다. 결과에 따르면 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