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

摘要

自动形式化通常被定义为将自然语言数学陈述翻译成机器可验证的形式语言（如 Lean 4）的过程。然而，忠实的形式化不仅仅是翻译。模型必须将数学概念映射到形式库（如 Mathlib）中复杂的类型和定义层级结构，同时确保生成的陈述保留源命题的含义。现有方法面临挑战，因为它们严重依赖模型的参数化记忆来获取库特定知识，而常见的数据构建流程往往采用过滤单次输出的方式，缺乏反馈驱动的修订机制。为了解决这些挑战，我们提出了 MathForm，一个通过 Mathlib 知识检索和验证引导的迭代细化来构建经过验证的训练数据的自动形式化框架。在生成之前，检索规划器从 Mathlib 中收集相关定义和现有形式化内容，以指导形式化生成器。随后，生成的陈述会利用编译器诊断和语义一致性反馈进行修订。利用该框架，我们构建了 FormalVerse，这是一个 Lean 4 数据集，包含约 36.7 万个经过验证的示例，覆盖多个数学领域和来源。随后，我们通过监督微调和强化学习训练了 MathForm-8B。在六个基准测试中，MathForm-8B 在语法检查（SC）下的平均 Pass@8 通过率达到 88.06%，在一致性检查（CC）下达到 72.37%，优于多个专门的 32B 自动形式化模型。在具有挑战性的 FATE-H 和 FATE-X 子集上，其 CC 通过率分别达到 63% 和 37%，在这两项上都超过了最强的专门基线。

English

Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.