🧮 介绍 MathForm：一个用于 Lean 4 数学自动形式化的开源框架、数据集与模型。

将数学形式化，能让数学知识变得可被机器检验，但其意义远不止于把命题翻译成代码。模型必须将每个概念映射到 Mathlib 中正确的类型与定义上。一段形式化命题即使能通过编译，仍可能曲解原始问题。

亮点 ✨ MathForm 框架：检索增强、验证引导的数据构建。检索规划器会提取命题所需的 Mathlib 定义与既有形式化内容。随后，生成器会根据 Lean 编译器的诊断信息与语义一致性反馈，对输出进行最多 3 轮的修订。

FormalVerse 数据集：367K+ 个经过验证的 Lean 4 示例。每个示例都将自然语言命题与经过验证的 Lean 4 代码配对，覆盖多个数学领域与来源。

结果 📊 • 在匹配的 100K 预算、相同配方与初始化条件下，基于 FormalVerse 训练的模型达到 60.32% 的一致性检查通过率，而基于 FineLeanCorpus 训练的为 46.53%，基于 NuminaMath-LEAN 训练的为 41.49% • MathForm-8B 在六个基准上达到 88.06% 的语法检查与 72.37% 的一致性检查 Pass@8，以四分之一的模型规模超越了 ReForm-32B 与 Goedel-Formalizer-V2-32B • 在难度最高的 FATE-H / FATE-X 子集上，其一致性检查分别达到 63% / 37%，比最强的专用基线高出 10 个和 12 个百分点

🔗 资源 📄 论文：http://arxiv.org/abs/2608.14221 📚 数据集：http://huggingface.co/datasets/openbmb/FormalVerse 🤖 模型：http://huggingface.co/openbmb/MathForm-8B 💻 代码：http://github.com/openbmb/MathForm