在现代数学与人工智能的交叉领域中，如何让机器准确“读懂”并通过形式化验证数学定理，一直是攻克通用人工智能（AGI）的核心挑战之一。OpenBMB团队近日正式开源了全新的数学自动形式化开源框架、数据集与模型——MathForm。
长期以来，数学形式化（例如基于 Lean4语言）不仅是把自然语言翻译成代码那么简单。一个严谨的模型必须将每一个数学概念精准映射到 Mathlib 库中正确的类型和定义上。行业内常常面临一个痛点:形式化语句即使能够顺利通过编译器编译，也可能在语义上无法准确描述原始问题。
为了攻克这一难题，MathForm 框架创新性地引入了检索增强与验证引导的数据构建机制。其核心逻辑在于，系统首先会通过检索规划器提取语句所需的 Mathlib 定义和现有形式化模型;随后，生成器会根据 Lean 编译器的诊断结果以及语义一致性反馈，对输出内容进行最多三轮的修正，从而大幅保障了代码质量与数学语义的统一。
在数据与模型层面，OpenBMB 推出了包含超过36.7万个已验证 Lean4示例的 FormalVerse 数据集，涵盖了多元化的数学领域和来源。实验结果表明，在同等训练预算和初始条件下，基于 FormalVerse 训练的模型一致性检查率达到了60.32%，远超 FineLeanCorpus 的46.53% 和 NuminaMath-LEAN 的41.49%。
作为核心成果之一，MathForm-8B 模型在六项基准测试中交出了亮眼答卷，实现了88.06% 的语法检查通过率和72.37% 的一致性检查通过率（8分制）。尤为引人注目的是，它以仅为对手四分之一的参数体量，反超了 ReForm-32B 和 Goedel-Formalizer-V2-32B 等更大体量的模型。特别是在难度最高的 FATE-H 和 FATE-X 子集中，其一致性检查成功率分别达到了63% 和37%，比最强的专项基准分别高出10和12个百分点，展现出极强的推理与形式化纠错能力。
项目地址:https://github.com/openbmb/MathForm
