MathForm：结合知识检索与验证引导精炼的数学自动形式化扩展 MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
MathForm用知识检索与验证迭代构造36.7万条Lean数据，8B形式化模型超越32B对手
前置知识
自动形式化（Autoformalization）
把自然语言数学陈述翻译成 Lean 4 等机器可验证形式语言的过程。评判分两层：Syntax Check（SC）要求生成的代码能通过编译，Consistency Check（CC）进一步要求形式化忠实保留原陈述的数学含义，比如量词范围不被改变、前提条件不被悄悄加强或削弱。CC 远比 SC 难，因为一个看似合理的陈述完全可以编译通过却语义失真。
这是论文要解决的核心任务，SC/CC 也是全文所有实验的统一评测维度，读懂主表必须先分清这两个指标。
Lean 4 与 Mathlib
Lean 4 是交互式定理证明器，兼有编程语言与依赖类型检查器；Mathlib 是其社区维护的大型数学库，内含层层嵌套的类型、定义、记号约定与数万条已形式化的定理。形式化任何陈述都必须正确映射到 Mathlib 的类型层级，例如把变量类型化为 $\mathbb{N}$ 还是 $\mathbb{Z}$ 会直接改变定理的数学内容。
Mathlib 既是本文检索知识的来源，又是编译验证与语义偏差判定的基准，理解它的庞大与演进性才能明白为何依赖模型参数记忆不可靠。
Best-of-N（BoN）采样
让模型对同一输入独立采样 $N$ 个候选，再用判别器事后整体筛选，只能接受或拒绝整个候选。它只能从模型现有输出分布中挑选，无法指出错误发生在哪里、如何修复，因此数据难度被锁死在模型单次生成能力的上限之内。
BoN 是本文要超越的主流数据构造范式，理解它'只筛选、不纠错'的局限，才能体会验证引导迭代精炼的价值所在。
SFT 与 RL 微调（DAPO）
SFT 用（自然语言陈述、形式化轨迹、验证过的 Lean 代码）三元组做监督微调；RL 阶段采用 DAPO（Decoupled Clip and Dynamic sAmpling Policy Optimization），在 token 级目标 $J(\theta)=\mathbb{E}\sum_{i,t}\min(\rho_{i,t}A_i,\ \mathrm{clip}(\rho_{i,t},1-\epsilon_{low},1+\epsilon_{high})A_i)$ 上优化，配合 Clip-Higher 与动态采样，奖励为二值函数 $r(x,y)=\mathbb{1}[C(y)=1\wedge S(x,y)=1]$。
MathForm-8B 的最终能力完全由'SFT 后接 RL'这条朴素配方产生，而奖励函数直接对齐可编译性与语义保真两个目标。
Pass@k 评测协议
对每个测试陈述采样 $k$ 个候选：$\text{SC@}k(x)=\max_{1\le i\le k}C(y_i)$ 表示只要有一个候选编译成功即通过；$\text{CC@}k(x)=\max_{1\le i\le k}C(y_i)S(x,y_i)$ 要求同一候选既编译成功又语义一致。本文统一取 $k=8$、采样温度 0.6，并对各基准做等权宏平均。
主表所有数字（如平均 CC 72.37%）都是 Pass@8 指标，不清楚定义就无法正确解读实验结果与模型间比较。
研究动机
现有自动形式化方法把任务当作一次性翻译，存在两个相互纠缠的短板。其一是知识依赖参数记忆：TheoremLlama、Herald、Kimina-Autoformalizer、Mathesis 等端到端模型全靠参数内化 Mathlib 的定义、类型层级与记号约定，而 Mathlib 极其庞大且持续演进，导致模型频繁误用已有定义、调用不存在的引理、写出合法却偏离库惯例的表述。其二是数据构造管道普遍采用 Best-of-N（BoN）策略：模型大批量采样候选，判别器事后整体过滤，只能接受或拒绝，无法指出语义偏差发生在哪里、如何修复，数据难度被锁死在单次生成能力上限。后果是现有数据集与模型集中于竞赛风格的代数与数论（如 miniF2F），而依赖更深库知识的抽象代数等领域严重欠覆盖——在 FATE-H、FATE-X 这类高抽象基准上，现有 7B 级专用形式化器的 CC 通过率普遍不足 20%。
本文的目标是本文目标是把自动形式化改造成'知识接地 + 重复验证收敛'的闭环数据工厂：在生成前检索 Mathlib 中相关定义与既有形式化来增强生成器，在生成后用编译诊断和语义一致性反馈驱动迭代修订，使数据难度上限由整条流水线而非单次生成决定。在此框架下构造约 36.7 万条经过验证的 Lean 4 训练语料 FormalVerse，并用最朴素的 SFT+RL 配方训练 MathForm-8B，让 8B 模型在六个基准的平均 Syntax Check 通过率达到 88.06%、Consistency Check 达到 72.37%，从而超过 ReForm-32B 等多个 32B 专用自动形式化器，并在最难的 FATE-H（63%）和 FATE-X（37%）CC 上大幅领先。
与已有工作不同的是，作者的关键洞察是：一个看似合理的 Lean 陈述可能编译通过，却悄悄加强条件或丢掉关键假设，这样的陈述对下游毫无用处。因此忠实形式化不应被理解为翻译，而应被理解为一个在验证信号引导下逐步收敛的知识加工过程。与 BoN 把验证信号只用于事后筛选不同，MathForm 把编译错误（可定位到具体行列）和语义偏差的文字描述转化为下一轮的具体修改指令；与 RAutoformalizer、DRIFT、Aria 等面向推理时逐实例检索的方法不同，它面向大规模端到端的训练数据构造。这一闭环把整条流水线的能力蒸馏进模型单次生成，实现数据—模型协同进化。
核心方法
直觉上，这套流程让生成器在动手前先'查资料'，写完后先'过编译器'再'过语义审校'，错了就带着反馈重写。技术上，检索规划器与形式化生成器均由 gpt-oss-120b 驱动：给定自然语言数学陈述，规划器分析涉及的对象、关系与类型约束，判断是否需要外部知识并发出少量定向查询，经 LeanExplore 返回每个查询 top-2 的 Mathlib 定义、定理、记号与既有形式化；生成器结合原陈述与检索结果产出 Lean 4 形式陈述。候选先过格式检查剔除含证明步骤的输出，再经 Lean 4 编译验证语法，最后由 QwQ-32B 担任裁判做语义一致性检查；任一环节失败则携带反馈进入下一轮，至多三轮，通过即停。验证通过的 NL-FL 对再回溯重构干净的推理轨迹，经 13-gram 去污染后得到约 367K 样本的 FormalVerse；用它对 Qwen3-8B 做 SFT，再用 verl 框架实现 DAPO 强化学习，奖励为编译成功与语义一致的合取。
核心创新是把验证信号从'筛选器'变成'纠错器'。编译诊断能精确指出错误类型与位置（如 failed to synthesize OfNat Lang 0，定位到第 2 行第 46 列），语义裁判能描述偏差性质（如自然语言对 $n$ 在全体整数 $\mathbb{Z}$ 上量化，而 Lean 把 $n$ 类型化为 $\mathbb{N}$，排除了负数），这些具体反馈让修订有明确方向，而不是靠更多独立采样碰运气。第二点是检索规划与代码生成分离：只在需要时按需检索 Mathlib，降低对参数记忆的依赖并提升与库中规范表示的一致性。第三点是 RL 数据恰恰取自流水线中从未通过验证的约 20000 条难题，经离线难度筛选后留下 3000 条，把'啃不动的硬骨头'直接转化为优化信号，奖励 $r(x,y)=\mathbb{1}[C(y)=1\wedge S(x,y)=1]$ 同时约束可编译性与语义保真。
方法步骤详情
流程分五步。第一步问题收集与规范化：从 DeepTheorem、NuminaMath、Lean Workbook、DeepMath 等七个数据集及经典教材筛选定理型问题，剔除非数学内容与纯数值题并改写冗余指令，最终语料中 Lean Workbook 占 32.8%、NuminaMath 占 26.0%。第二步知识检索与生成：检索规划器按需发起查询，经 LeanExplore 取回 Mathlib 定义与既有形式化（每查询 top-2），生成器据此产出 Lean 4 陈述。第三步验证引导迭代：格式检查剔除含证明或解题步骤的输出，编译检查语法错误，QwQ-32B 语义裁判检查遗漏假设、条件加强、量词顺序错误等，失败样本带反馈重写，至多三轮、通过即停。第四步轨迹重构：为每个验证过的对回溯合成干净轨迹并显式排除证明策略，形成（陈述、轨迹、代码）三元组，再以 13-gram 对评测基准去污染。第五步训练：LLaMA-Factory 做 SFT 得到 MathForm-8B-SFT；再从约 20000 条未解难题中筛出 3000 条作 RL 数据，用 verl 实现 DAPO，二值奖励要求编译与语义同时通过。
技术新颖性
新颖性可从三个维度看。对比 BoN 管道：反馈驱动的迭代修订使第二、三轮额外贡献 31.0% 的保留对（第一轮 254K 占 69.2%，第二轮约 73K 占 20%，第三轮约 40K 占 11%），打破了单次生成的难度天花板；消融显示完整管道比最强单组件配置（检索、反馈迭代或预算匹配采样）在两个生成器上分别再提升 7.00/6.90 与 8.80/7.46 个百分点的 SC/CC。对比检索增强形式化（RAutoformalizer、DRIFT、Aria）：那些方法面向推理时逐实例形式化，本文把检索嵌入大规模端到端数据构造。对比训练配方：裁判与生成器刻意分属不同家族以抑制自我偏好——数据构造用 QwQ-32B、RL 奖励用推理更快且精确率接近的 gpt-oss-20b、最终评测用高推理档的 gpt-oss-120b，并在 200 例人工标注集上验证了裁判可靠性（gpt-oss-120b F1 0.8940）。
实验结果
主结果（Table 1）：六基准 Pass@8 宏平均上 MathForm-8B 达 SC 88.06%、CC 72.37%，超最强专用基线 ReForm-32B（81.61/68.41）6.45 和 3.96 个百分点；RL 把平均 CC 从 SFT 版 66.53% 提到 72.37%，说明验证驱动 RL 主要改善语义对齐。增益集中在高抽象领域：FATE-M/H/X 的 CC 为 97.33%/63.00%/37.00%，分别领先最强专用基线 6/10/12 个百分点。消融（Table 2）：gpt-oss-120b 在 FATE 系列平均 SC 由单次生成 27.33% 升至完整管道的 49.67%（+22.34pp），换 Qwen3-235B 生成器则从 7.43% 升至 37.57%（+30.14pp），证明检索与迭代互补且不绑定生成器。数据质量（Table 3）：各取 100K 样本同配方微调 Qwen3-8B，FormalVerse 平均 CC 60.32%，超 FineLeanCorpus 13.79、超 NuminaMath-LEAN 18.83 个百分点，而 SC 各家相当，差距几乎全部来自语义保真。训练中 FATE-H 的 Mean@3 从 0.30 升至约 0.40（+33% 相对增益）；FATE-M/H 人工评测确认其 SC 与人工判定 CC 全场最高。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 六基准宏平均（FormalMATH-Lite / ProverBench / CombiBench / FATE-M / FATE-H / FATE-X） | Pass@8 语法检查（SC） | MathForm-8B：88.06% | ReForm-32B：81.61% | +6.45 个百分点 |
| 六基准宏平均 | Pass@8 一致性检查（CC） | MathForm-8B：72.37% | ReForm-32B：68.41% | +3.96 个百分点 |
| FATE-M（中等抽象，含抽象代数） | Pass@8 CC | 97.33% | 最强专用基线 ReForm-8B：91.33% | +6.00 个百分点 |
| FATE-H（高抽象） | Pass@8 CC | 63.00% | 最强专用基线 ReForm-8B：53.00% | +10.00 个百分点 |
| FATE-X（超高抽象，交换代数/同调代数/代数几何基础） | Pass@8 CC | 37.00% | 最强专用基线 ReForm-32B：25.00% | +12.00 个百分点 |
| 数据质量对照（各 100K 样本、同配方微调 Qwen3-8B） | 六基准平均 CC | FormalVerse：60.32% | FineLeanCorpus 46.53% / NuminaMath-LEAN 41.49% | +13.79 / +18.83 个百分点 |
局限与改进
作者承认的局限：语义一致性依赖 LLM 裁判，人工标注 200 例上最优的 gpt-oss-120b F1 也只有 0.8940，误判会同时污染数据构造与 RL 奖励；每个样本至多三轮，始终无法通过的样本被丢弃，约 20000 条未解难题只有 3000 条进入 RL；评测固定在 $k=8$、温度 0.6 下，作者也明言未来需要更大规模的测试时扩展。我自己的观察：其一，整个框架深度绑定 Lean 4/Mathlib 生态，迁移到 Isabelle、Coq 等系统需重建检索索引与验证器；其二，流水线由 gpt-oss-120b 驱动生成，367K 样本的构造预算（生成+编译+裁判调用量）论文未披露，成本可能不低；其三，LLM 裁判对'两可'表述可能系统性偏向某一种形式化风格，论文为此在 RL 数据中剔除了多种合理形式化并存的样本，但这本身就是信息损失；其四，方法只处理陈述形式化，不涉及证明生成，距离端到端形式数学仍有一步之遥。
独立分析的弱点
独立分析三个弱点。第一，裁判瓶颈：数据构造裁判 QwQ-32B 的 F1 为 0.8609，RL 奖励裁判 gpt-oss-20b 为 0.8579，假阳性会直接变成错误正样本污染 SFT 数据或错误奖励信号——在 CC 指标约 72% 的水平上，几个百分点的裁判噪声足以改变模型排名。改进方向是训练专门的语义等价判别模型或过程奖励模型（PRM）替代通用 LLM 裁判，并用人工抽检闭环持续校准。第二，难度天花板依然存在：三轮上限意味着最难的一批陈述永远进不了 SFT 数据，只能以极少数量进入 RL，例如 FATE-X 上仍有约 63% 未通过；可探索按样本自适应分配轮数预算，或把语义检查拆成对前提、量词、结论的逐项核对以给出更细粒度的修复信号。第三，13-gram 去污染无法防御改写式污染，竞赛基准一旦被改写进训练语料，评测数字会虚高；可补充基于嵌入相似度或 TF-IDF 加权 n-gram 集合的软匹配过滤。另外，'编译通过'与'符合库惯例'是两回事，论文未量化生成结果与 Mathlib 规范表示的风格一致性。
未来方向
作者明确提出的方向是探索更大规模的测试时扩展（test-time scaling），在推理阶段做验证引导的迭代以强化复杂问题的形式化。基于本文成果还可自然延伸：其一，把'检索+验证+迭代'闭环用于定理证明与证明自动形式化，用同样的编译与语义信号重构证明轨迹，打通陈述到证明的完整链条；其二，数据—模型协同进化的下一轮迭代——用 MathForm-8B 本身替换 gpt-oss-120b 作为生成器重跑流水线，检验自我提升能否持续、是否会出现风格坍缩；其三，把检索索引从 LeanExplore 扩展到 Isabelle/HOL、Coq 等其他证明助手的库，研究跨系统迁移的形式化；其四，研究更可靠的语义一致性度量，例如基于双向蕴含检查或类型级等价验证的专门模型，降低对通用 LLM 裁判的依赖；其五，迭代轮次找回了 31% 的数据，这个比例可作为信号研究轮数预算的动态分配与提前停止策略。
复现评估
复现条件较好：FormalVerse 数据集发布于 Hugging Face（openbmb/FormalVerse，约 367K 验证样本），模型权重 openbmb/MathForm-8B 与代码 github.com/openbmb/MathForm 均公开。流水线的外部组件都可获得：生成器 gpt-oss-120b 与奖励裁判 gpt-oss-20b 为开放权重模型，构造裁判 QwQ-32B 开放，Lean 编译验证可复用 Kimina Lean Server，知识检索走 LeanExplore。训练本身不算重：SFT 基于 LLaMA-Factory 在 Qwen3-8B 上进行，RL 用 verl 实现 DAPO（仅 3000 条 RL 数据、8B 模型），单机多卡即可尝试。主要门槛在于从零复现数据构造：367K 样本需要海量的生成、编译与裁判调用，论文未公布总预算与构造时长；评测侧需复现六基准的 Pass@8（$k=8$、温度 0.6）采样与语义裁判流程。综合评估：用已发布数据复现训练属于中等难度，完整复现数据构造则相当昂贵。
论文图表
