MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hengyu Zhao, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang
cs.AI, cs.CL
2026-08-14
检索 Mathlib 加三轮编译与语义校验造出 36.7 万验证对,8B 模型六基准平均反超 32B 专用形式化模型。
autoformalization 把自然语言数学命题写成 Lean 4 这样的机器可验证形式语言。难点不在翻译本身:Mathlib 有复杂的类型与定义层级,同一个概念在库里可能有现成定义,模型得找对映射,还得保证写出来的命题与原命题同义,不漏假设、不强化条件、量词不走样。现有方法的短板有两个:靠参数化记忆去猜库内知识,猜错就编译失败;数据构造管线多是单次生成加过滤,生成了什么就是什么,没有反馈式修订。
MathForm 的管线分三段:
迭代不是锦上添花:第一轮产出约占最终保留对的 69%,第二、三轮分别再加约 20% 和 11%,合计回收了单次生成会直接丢掉的 31%。
用这条管线造出数据集 FormalVerse,约 367K 验证过的自然语言-形式化对,来源覆盖 DeepTheorem、NuminaMath、AceReason-Math、Lean Workbook、Principia-Collection、DeepMath、OpenR1-Math 与经典教材,分十个数学门类,对评测集做了 13-gram 去污。训练分两步:Qwen3-8B 先在 FormalVerse 上 SFT,再用 DAPO 做 RL,奖励是编译通过与语义一致的二值信号。
六个 benchmark 平均 Pass@8,与专用基线对照:
| 模型 | SC | CC |
| MathForm-8B | 88.06% | 72.37% |
| ReForm-32B | 81.61% | 68.41% |
| Goedel-Formalizer-V2-32B | 78.28% | 63.74% |
| StepFun-Formalizer-32B | 63.65% | 44.47% |
对最强专用基线 ReForm-32B 的绝对增益是 SC +6.45、CC +3.96,模型尺寸只有对方四分之一。RL 阶段的贡献单独可测:SFT-only 是 84.38/66.53,RL 后到 88.06/72.37,CC 涨幅大于 SC,验证驱动的 RL 主要提升语义对齐,语法可编译性本就接近饱和。难档 FATE 子集的 CC:FATE-M 97.33%、FATE-H 63.00%、FATE-X 37.00%,都超过最强专用基线。CC 判定器本身的质量也校验过:gpt-oss-120b 高推理档在 200 条人工标注上 F1 为 0.8940。
形式化数据是定理证明的瓶颈资产,这条管线把「检索外部知识+可执行校验+LLM 语义判分」组合成了一个数据工厂,31% 的增量全部来自迭代修订。367K 验证对直接开源。8B 尺寸意味着单卡可跑,做数学证明或形式化方法的人能本地部署。方法论本身可迁移:任何「生成物可以被机器部分验证」的任务,编译器诊断加语义判分的双关修订都值得照抄。
作者自述平均 CC 72.37% 仍低于通用前沿模型,Qwen3.7-Plus 是 83.38%,DeepSeek-V4-Pro 是 76.54%。专用训练换来的是可编译性,语义保真上大模型仍占优,这是能力与效率的取舍。两个没量化的点:CC 训练信号本身是 LLM 判分,F1 0.894 意味着约一成标签是错的,这个噪声对 RL 阶段的影响论文没有评估;检索依赖 LeanExplore 对 Mathlib 的覆盖,换 Coq 或 Isabelle 就没有现成对应物。FATE-X 只有 37%,超纲命题仍是硬骨头。