数学自动形式化迎来重大突破：OpenBMB开源MathForm，8B模型凭实力逆袭大厂

在现代数学与人工智能的交叉领域中，如何让机器准确“读懂”并通过形式化验证数学定理，一直是攻克通用人工智能（AGI）的核心挑战之一。OpenBMB团队近日正式开源了全新的数学自动形式化开源框架、数据集与模型——MathForm。

长期以来，数学形式化（例如基于 Lean4语言）不仅是把自然语言翻译成代码那么简单。一个严谨的模型必须将每一个数学概念精准映射到 Mathlib 库中正确的类型和定义上。行业内常常面临一个痛点:形式化语句即使能够顺利通过编译器编译，也可能在语义上无法准确描述原始问题。

为了攻克这一难题，MathForm 框架创新性地引入了检索增强与验证引导的数据构建机制。其核心逻辑在于，系统首先会通过检索规划器提取语句所需的 Mathlib 定义和现有形式化模型;随后，生成器会根据 Lean 编译器的诊断结果以及语义一致性反馈，对输出内容进行最多三轮的修正，从而大幅保障了代码质量与数学语义的统一。

作为核心成果之一，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