MathForm: 基于知识检索与验证引导精炼的数学自动形式化规模化

TL;DR MathForm 框架结合 Mathlib 知识检索与验证引导迭代细化，自动形式化数学命题；基于其构建的 FormalVerse 数据集训练的 8B 模型，在多个基准的 Pass@8 上超越 32B 专用自动形式化器。

问题

问题背景

数学自动形式化(autoformalization)旨在将自然语言数学命题转化为 Lean 4 等可机器验证的形式语言，为定理证明和大规模数学推理提供严格基础。

现有方法局限

• 过度依赖参数记忆：模型需从 Mathlib 等大型形式化库中准确定位类型、定义和已有定理，但单靠预训练记忆难以覆盖复杂层级和惯用符号，导致大量形式化结果因类型不匹配或未知常量而编译失败。
• 数据构建缺乏反馈闭环：常见流程是单次生成后做语法检查过滤，丢弃大量接近正确但含编译错误的候选，且无法利用编译器诊断信息指导修订。
• 语义一致性保障不足：仅通过语法检查会漏掉“形式化语句可编译但与原命题含义偏离”的错误，这种错误会直接污染后续训练数据。

为什么难且重要

Mathlib 的类型层级深、定义之间关联复杂，自动形式化需要在生成前精准检索相关符号和前置定理，而不是依赖模糊记忆。同时，形式化错误代价高：编译失败意味着无法进入验证流程，语义偏离则会让模型学到错误映射。业界当前关注如何把验证器反馈闭环到生成过程，类似于 RLHF 在代码生成中的编译器反馈，这是扩展形式化训练数据规模的瓶颈。

行业类比

等价于代码生成中引入 compiler-in-the-loop：不是一次写完就过滤，而是让编译器诊断和测试反馈驱动迭代修复，从而把接近正确的生成转化为可验证的正确结果。

核心洞察

• MathForm 通过 **Mathlib 检索规划器** 引入外部知识，改变了 autoformalization 对模型参数记忆的依赖。与以往依赖模型内部记忆并过滤单次输出的 pipeline 不同，MathForm 在生成前显式检索相关定义和已有形式化，将检索增强生成应用于数学形式化，提升了概念映射的准确性。这为解决库特定知识覆盖不足提供了结构化方案，也为其他依赖大型知识库的生成任务提供了检索增强的参考。
• **验证引导迭代细化** 使 autoformalization 从“一次生成、过滤”转变为反馈驱动的闭环修订。利用 Lean 编译器诊断和语义一致性反馈，模型能根据错误信息修正形式化结果，而不是直接丢弃失败样本。这种机制与常见的数据构建流程形成对比，后者缺少反馈修正，导致低产出和低质量。迭代细化不仅提高了数据验证通过率，还构建了含修订轨迹的训练数据，有助于模型学习修正能力。
• **MathForm-8B 以 8B 参数超越多个 32B 专用 autoformalizer**，表明小模型配合高质量数据和 RL 可以在专业任务上超越大模型。其成功来自检索增强、迭代细化和奖励设计，而不是单纯扩大参数。这为行业提供了在算力有限条件下提升专业能力的路径：通过精细的数据工程和训练策略，小模型能够达到或超过大模型效果，降低了部署成本。

方法

输入为多源自然语言数学命题，经收集与规范化后进入 MathForm 框架。

关键模块与流程

1. 检索规划器：从 Mathlib 中检索相关定义、定理与既有形式化，将库知识显式注入生成上下文，缓解参数记忆不足。
2. 形式化生成器：基于检索结果与源命题生成 Lean 4 语句。
3. 验证引导迭代细化：利用编译器诊断和语义一致性反馈对生成语句进行多轮修订，而非仅过滤单遍输出。
4. 轨迹重建：从成功验证的迭代过程中提取“初始生成→反馈→修正→通过”的完整轨迹，保留中间状态与决策序列。
5. 数据去污染：排除与评测基准重叠的内容，保证训练数据独立性。

最终输出为 FormalVerse 数据集，包含约 367K 条已验证 Lean 4 示例，覆盖多个数学领域。

模型训练

• 监督微调：以重建轨迹为训练数据，让模型学会生成并修正形式化语句。
• 强化学习：设计基于验证结果（语法通过、语义一致性）的奖励函数，并通过 RL 数据选择聚焦高价值样本，进一步提升生成质量。

与同类方法仅依赖参数记忆、单遍生成加过滤不同，MathForm 将自动形式化重构为“检索增强生成 + 验证反馈闭环”，使 8B 模型在多个基准上超越 32B 专用模型。

实验

实验设计

• 构建 FormalVerse：约 367K 条经验证的 Lean 4 形式化数据，利用 Mathlib 知识检索与验证引导迭代精化。
• 训练 MathForm-8B：先监督微调 (SFT)，后强化学习 (RL)。
• 评估：在六个基准上使用 Pass@8 指标，分别做语法检查 (SC) 和一致性检查 (CC)；与多个 32B 专门 autoformalizer 对比。

关键发现

• 平均 Pass@8 SC 达 88.06%，CC 达 72.37%，均超越 32B 专门基线。
• 在 FATE-H / FATE-X 上 CC 分别 63% 和 37%，仍优于最强专门基线。
• 收益集中于高抽象陈述，证明检索与反馈对复杂概念映射尤其有效。

深度解读

• 8B 模型超越 32B 专门模型说明：显式检索 Mathlib 定义比依赖参数记忆更可靠；验证引导的精化能生成更准确的语句。
• 但 FATE-X 仅 37%，表明对极抽象或长尾概念的检索和语义一致性判断仍有明显瓶颈，未来需改进检索覆盖和判别器。

行业影响

落地场景

MathForm 面向需要高可信数学推理的场景，可嵌入以下产品：

• 数学教育平台：自动检查学生证明草稿与定理陈述的一致性，生成 Lean 4 练习并即时反馈。
• 金融风控与智能合约：将衍生品定价模型或合约条款形式化为可验证规范，降低逻辑漏洞风险。
• AI 辅助证明工具：作为插件集成到 VS Code + Lean 4 环境，辅助研究员编写形式化证明。

商业价值

• 降本：MathForm-8B 以 8B 参数量达到 32B 专用模型效果，显著降低推理与部署成本；其自动构建 FormalVerse 数据集（367K 验证样本）替代人工标注，省去大量专家标注费用。
• 体验提升：在六个基准上平均 Pass@8 一致性检查（CC）达 72.37%，可提供可信的实时形式化反馈，提升用户对自动验证服务的信任度。

与现有工作流的接口

MathForm 的 检索规划器 调用 Mathlib API 获取定义与已有形式化，可封装为 REST 服务或本地推理端点，接入现有 LLM 应用管道（如 RAG、Agent）。其输出为 Lean 4 代码，可直接由 Lean 编译器验证，因此可自然集成到 CI/CD 或形式化验证工作流中，无需改造底层工具链。

具体落地用例

• 金融行业：量化团队使用 MathForm-8B 将衍生品定价公式自动形式化为 Lean 4，通过编译器检查与原始文档的语义一致性，减少人工合规审查时间。
• 教育科技：在线数学学习平台集成 MathForm-8B，对学生提交的证明草稿进行语义一致性判断，识别逻辑纰漏并给出针对性反馈，提升学习闭环效率。

局限

• **语义一致性判断的可靠性存疑**。框架依赖 LLM 进行语义一致性判断，但 LLM 判断本身可能有误，尤其在高抽象数学陈述中。论文虽有可靠性分析，但未完全消除误判风险。如果判断模型将错误形式化标为正确，会向训练数据引入噪声，影响模型学习真实映射。
• **知识检索受限于 Mathlib 覆盖范围**。检索规划器从 Mathlib 获取定义和已有形式化，但 Mathlib 并未覆盖所有数学分支，且处于动态更新中。对未收录的前沿数学概念或小众领域，检索可能无法提供有效引导，导致形式化失败或生成不完整定义，泛化能力受限。
• **评估指标与部署成本的权衡**。报告 `Pass@8` 高通过率，但实际单次生成（`Pass@1`）可能显著更低，意味着部署时要多次采样与验证，增加推理延迟和计算开销。此外，与通用大模型最新版本的对比不足，可能高估专属模型的相对优势。