OpenBMB 开源 MathForm-8B：8B 模型 + 36.7 万条 Lean 4 验证数据

整体开源：模型、数据、评测代码

OpenBMB 把 MathForm 这套数学自动形式化方案整体开源：MathForm-8B 模型权重、约 36.7 万条验证过的 Lean 4 数据集 FormalVerse、评测代码与 Pass@k 脚本一并放出。模型挂在 Hugging Face，Apache-2.0 许可，基座为 Qwen3-8B，BF16 权重。项目由清华 NLP 实验室与面壁智能共同支持的 OpenBMB 团队完成。

自动形式化把自然语言写的数学命题翻译成 Lean 4 这类机器可验证的形式语言，难点在于把「连续函数」「有限群」精确对应到 Mathlib 庞大的类型层级与定义体系，同时保证形式化后的命题和原命题说的是同一件事。

8B 怎么压过 32B

数据流水线分四步：规划器针对命题里的数学概念查询 Mathlib（检索工具 LeanExplore 每次返回前 22 条结果），模型在检索上下文中生成 Lean 4 命题，候选依次过格式检查与编译测试，再由大模型裁判做语义一致性判定；通过的路径回溯重构成干净训练轨迹。论文显示后续迭代轮次贡献了全部保留样本中额外的 31.0%。

评测铺开六个基准，MathForm-8B 在 FATE-X 上拿到 37% 一致性通过率，压过多款 32B 专用形式化模型；语法检查平均 Pass@8 为 88.06%，一致性检查平均 72.37%。BF16 加载约需 16GB 显存，一张 24GB 消费级显卡即可运行，硬件门槛从集群级降到单机级。

把 Mathlib 交给检索工具、只让模型负责组装，8B 和 32B 掰手腕靠的本来就不是同一件事。