MathForm: 通过知识检索与验证引导的精炼实现数学自动形式化的规模化

摘要

自动形式化通常被视为将自然语言数学命题翻译为机器可验证的正式语言（如 Lean 4）。然而，忠实的形式化需要将数学概念映射到 Mathlib 等正式库中的类型和定义，现有方法依赖参数记忆而缺乏反馈修订。本文提出 MathForm 框架，通过 Mathlib 知识检索和验证引导的迭代精炼构建经校验的训练数据。利用该框架构建了 FormalVerse 数据集，包含约367K个 Lean 4 验证示例，并训练了 MathForm-8B 模型。在六个基准测试中，MathForm-8B 在语法检查和一致性检查下的平均 Pass@8 分别为 88.06% 和 72.37%，优于多个专业的 32B 自动形式化系统；在 FATE-H 和 FATE-X 子集上，CC 通过率分别为 63% 和 37%，均超过最强基线。