野生环境中的多模态自动形式化：MMFormalizer
计算与语言
2026-01-07 v1
摘要
自动形式化将自然语言数学翻译为形式陈述以实现机器推理,面对现实环境中的多模态特性面临根本性挑战,因为物理场景需要从视觉元素推断隐藏约束(如质量或能量)。为此,我们提出MMFormalizer,该方法超越文本,通过整合自适应 grounding 与来自真实世界数学和物理领域的实体。MMFormalizer 通过递归 grounding 和公理组合,从感知 grounding 的基本单元递归构建形式命题,以自适应递归终止确保每个抽象都得到视觉证据的支持并锚定在尺度或公理 grounding 中。我们在新的基准PhyX-AF 上对MMFormalizer进行评估,该基准包含115个来自MathVerse、PhyX、Synthetic Geometry和Analytic Geometry的精选样本,涵盖多样化的多模态自动形式化任务。结果表明,如GPT-5和Gemini-3-Pro等前沿模型在编译和语义准确率最高,GPT-5在物理推理方面表现突出,而几何仍是最具挑战性的领域。总体而言,MMFormalizer为统一的多模态自动形式化提供了可扩展框架,桥接了感知与形式推理。据我们了解,这是首个能够处理来源于哈密顿量的经典力学、相对论、量子力学和热力学的多模态自动形式化方法。更多细节请参阅我们的项目页面: MMFormalizer.github.io
引用
@article{arxiv.2601.03017,
title = {MMFormalizer: Multimodal Autoformalization in the Wild},
author = {Jing Xiong and Qi Han and Yunta Hsieh and Hui Shen and Huajian Xin and Chaofan Tao and Chenyang Zhao and Hengyuan Zhang and Taiqiang Wu and Zhen Zhang and Haochen Wang and Zhongwei Wan and Lingpeng Kong and Ngai Wong},
journal= {arXiv preprint arXiv:2601.03017},
year = {2026}
}
备注
Technical Report