MathForm：用检索与验证，让数学自动形式化从翻译走向迭代

导语

把“对于任意实数……”这样的数学表述交给 Lean 4，并不只是一次语言翻译。模型还必须在 Mathlib 这类形式化数学库中找到恰当的类型、定义和已有定理，同时确保生成的命题没有改变原始自然语言的含义。MathForm 关注的正是这一更完整的问题：如何让自动形式化具备检索、验证和修订能力。

核心方法

传统流程往往依赖模型参数中记忆的库知识，并对单次生成结果进行筛选。这样做可以留下能够编译的样本，却难以系统处理定义选错、类型不匹配或语义偏移等问题。MathForm 将数据构建拆成几个相互衔接的环节：

• 先检索再生成：检索规划器从 Mathlib 中收集相关定义、类型信息和已有形式化表达，为生成器提供上下文。
• 编译反馈驱动修订：生成的 Lean 4 语句会接受编译检查，模型根据编译器诊断信息进行修改。
• 加入语义一致性反馈：除了检查代码是否通过，还要关注形式化命题是否仍然表达源文本中的数学含义。
• 用于训练数据构建：经过验证和修订的样本被汇集为 FormalVerse，覆盖多个数学领域与数据来源。

研究团队报告称，FormalVerse 包含约 367K 条经过验证的 Lean 4 示例。在此基础上，他们先进行监督微调，再进行强化学习，训练出 MathForm-8B。

结果与意义

在六个基准上，MathForm-8B 的平均 Pass@8 为 88.06%，对应语法检查；在一致性检查下为 72.37%。这些结果超过了多个专用 32B 自动形式化模型。在更具挑战性的 FATE-H 和 FATE-X 子集上，模型的一致性通过率分别达到 63% 和 37%，并在两项测试中超过最强的专用基线。

这项工作的价值不只在于模型规模。它把自动形式化中常被分开的三个问题——库知识获取、代码可验证性和命题语义保持——放进了同一个闭环。对数学模型而言，编译通过是必要条件，但不是充分条件；如果形式化后的命题悄然改变了原命题，机器验证也无法保证结果可靠。MathForm 通过检索和反馈式修订，尝试缩小这两种“正确”之间的差距。

当然，素材并未给出完整的实验设置、基线配置或人工评估细节，因此这些结果仍应结合论文全文进一步判断。已公开的代码、模型和数据集则为复现实验及后续研究提供了入口。整体来看，MathForm 展示了一条面向可验证数学数据生产的路线：让模型不再只凭记忆生成，而是在形式化库和验证器的共同约束下持续改进。

来源：Hugging Face Daily Papers