AREX Feed Article
OpenBMB 发布 MathForm：8B 模型自称六基准超越 32B 级专用模型
8 月 21 日，OpenBMB（Open Lab for Big Model Base）官方 X 账号宣布发布 MathForm：一套面向 Lean 4 数学自动形式化的开源框架、数据集与模型组合（）。公告给出的核心数字有两组：FormalVerse 数据集含 36.7 万余条经验证的 Lean 4 样例；MathForm-8B 在六项基准上 Syntax Check 与 Consistency Check 的平均 Pass@8 分别达到 88.06% 与 72.37%，宣称以四分之一参数量超越 ReForm-32B、Goedel-Formalizer-V2-32B 等 32B 级专用模型。
这些成绩均为团队自报口径。配套论文（）由 ModelBest（面壁智能）与清华大学的研究者合著，公告本身只能证明发布方作出了上述宣称。
编译通过，命题仍可能被改错
公告解释了为什么自动形式化不只是翻译：模型必须把每个数学概念映射到 Mathlib 中正确的类型与定义，而一个形式化语句可以编译通过，却仍然曲解原题，比如悄悄加强条件或丢掉关键假设。
论文把这类错误归因于两个常见缺陷：模型过度依赖参数记忆库知识，而 Mathlib 本身在持续演进；常见的数据管道采用 Best-of-N 策略，单次生成大批候选再事后过滤，判别器只能整体接受或拒绝，指不出语义偏差在哪里、如何修复。
MathForm 的答案是检索加修订。生成前，检索规划器（retrieval planner）先从 Mathlib 拉取该语句需要的定义与既有形式化；生成后，生成器依据 Lean 编译器诊断与语义一致性反馈修订输出，最多 3 轮。检索、自动验证与迭代修订由此构成闭环，数据难度的上限由整个管道决定，而不是被模型的单次生成能力封顶（第 1 节）。
只留下编译与语义双重通过的样例
FormalVerse 在 Hugging Face 上显示 366,568 行、约 2.16 GB，每条样例把自然语言命题与验证通过的 Lean 4 语句配对，并附带生成轨迹（）。
数据字段包括自然语言命题、形式化语句、来源、数学主题标签、对话记录与生成所用模型；自然语言题目取自 DeepTheorem、NuminaMath、AceReason-Math、Lean Workbook、Principia-Collection、DeepMath、OpenR1-Math 等公开集合。只有同时通过编译与语义验证的样本才会被保留。
MathForm-8B 是 8B 参数的模型，在 FormalVerse 上先做监督微调（SFT）、再做强化学习（RL），反馈信号来自 Lean 编译与语义一致性检查（）。
模型卡提供了 Transformers、vLLM、SGLang 三种调用方式；仓库代码覆盖数据构造与评测两条管道，编译检查需要自建 Kimina Lean Server，实验基于 Lean 4.21.0（）。
在六项基准上，8B 自称压过 32B 级模型
公告还报告了一组同预算对照：在 10 万条（100K）预算、相同配方与初始化下，用 FormalVerse 训练的模型 Consistency Check 达到 60.32%，用 FineLeanCorpus 为 46.53%，用 NuminaMath-LEAN 为 41.49%。
六项基准（FormalMATH-Lite、DeepSeek-ProverBench、CombiBench、FATE-M/H/X）的宏平均成绩为 Syntax Check 88.06%、Consistency Check 72.37%；在最难的 FATE-H 与 FATE-X 子集上分别为 63% 与 37%，比最强专用基线高出 10 与 12 个百分点。
仓库自带的对比图显示，Consistency Check 宏平均上 MathForm-8B（72.37）排在 ReForm-32B（68.41）、Goedel-V2-32B（63.74）等 32B 级模型之前。论文同时报告，在 FormalMATH-Lite、DeepSeek-ProverBench、CombiBench 与 FATE 上它超过同量级模型，并在多个挑战性子集上匹敌或超过明显更大的专用模型；消融实验显示知识检索、自动验证与强化学习各自都有贡献。
自动形式化的瓶颈在数据管道
背景在于：AlphaProof、DeepSeek-Prover-V2、Goedel-Prover-V2 等系统已经能为形式化陈述生成复杂的 Lean 4 证明，但进一步规模化需要大量可机器检查的语句与证明，这类语料稀缺。多数数学知识只以自然语言存在，手工形式化既要求精确的数学理解，又要求证明助手的专长。既有数据集集中在竞赛式代数与数论，抽象代数等需要深层库知识的领域长期欠代表。
MathForm 把形式化重新定义为"知识检索加反复验证收敛"的过程，而不是一次性翻译；论文称训练会把整个管道的难度压缩进模型的单次生成，形成数据与模型的共同进化（data-model co-evolution）。这也解释了为什么一次发布同时包含框架、数据集与模型：框架负责产出数据，数据负责训练模型，模型与评测代码则把自报的成绩变成可复现的对象。
8 月 14 日提交论文，8 月 21 日官宣
时间线把发布过程交代得很清楚：论文 v1 于 8 月 14 日提交 arXiv，GitHub 仓库同日创建；8 月 17 日仓库 README 的新闻条目标注论文、代码、数据与模型一并发布。
8 月 18 日，ModelScope 官方账号先行发帖介绍 FormalVerse，给出与公告一致的基准数字，并注明 Apache 2.0 许可，附上其在 ModelScope 平台的数据集与论文页面（）；8 月 21 日 OpenBMB 才正式官宣。
框架、数据集与模型全部以 Apache 2.0 开源，代码覆盖数据构造与评测两条管道，用同一套基准复现这套数字的入口已经齐备。88.06% 与 72.37% 目前只能作为发布方自报口径记录，这也是本次发布最需要被独立检验的部分。