MathForm：以知识检索与验证引导精化扩展数学自动形式化

自动形式化通常被框定为将自然语言数学陈述翻译为Lean 4等机器可验证的形式语言。然而，忠实的形式化不仅仅是翻译。模型必须将数学概念映射到Mathlib等形式库中复杂的类型与定义层级，同时确保生成的陈述保留源命题的含义。现有方法之所以表现不佳，是因为它们严重依赖模型的参数记忆来获取库特定知识，而常见的数据构建流水线往往只能过滤单次输出，缺乏反馈驱动修订的机制。为应对这些挑战，我们提出MathForm，一个通过Mathlib知识检索与验证引导迭代精化来构建经验证训练数据的自动形式化框架。生成之前，检索规划器从Mathlib收集相关定义与既有形式化以指导形式化生成器。生成的陈述随后依据编译器诊断和语义一致性反馈进行修订。利用该框架，我们构建了FormalVerse，一个包含约367K个跨多样数学领域与来源的经验证样本的Lean 4数据集。随后我们通过监督微调加强化学习训练MathForm-8B。在六个基准上，MathForm-8B在语法检查（SC）下达到平均88.06%的Pass@8率，在一致性检查（CC）下达到72.37%，优于多个专用32B自动形式化器。在具有挑战性的FATE-H和FATE-X子集上，其CC通过率分别为63%和37%，均超过最强的专用基线。