FormalVerse

FormalVerse是由模基最佳有限公司和清华大学联合构建的大规模自动形式化数据集，旨在将自然语言数学语句转化为Lean 4可验证形式。该数据集包含约367,000条经过编译和语义一致性检查的定理声明，覆盖来自NuminaMath、Lean Workbook、DeepMath等十余个数学问题集，涉及代数、数论、组合学等多个数学领域。数据通过知识检索与迭代精炼管道生成，首先利用检索器从Mathlib中获取相关定义和已有形式化，再由生成器产出候选，经编译器诊断和语义一致性判断后，对失败案例进行最多三轮修正，最终保留通过所有检查的实例。该数据集专门用于训练自动形式化模型，旨在解决现有方法依赖模型参数记忆、难以处理复杂库知识和单次生成能力上限的问题，从而提升模型在各类数学领域中的形式化准确率。FormalVerse is a large-scale automated formalization dataset jointly developed by Moji Zuijia Co., Ltd. and Tsinghua University, aiming to translate natural language mathematical statements into Lean 4-verifiable formalizations. This dataset contains approximately 367,000 theorem statements that have undergone compilation and semantic consistency checks, covering over ten mathematical problem collections including NuminaMath, Lean Workbook, DeepMath, and spanning multiple mathematical fields such as algebra, number theory, and combinatorics. The dataset is generated via a knowledge retrieval and iterative refinement pipeline: first, a retriever fetches relevant definitions and existing formalizations from Mathlib; then a generator produces candidate formalizations; after undergoing compiler diagnostics and semantic consistency verification, failed cases are revised for up to three rounds, and only instances passing all checks are finally retained. This dataset is specifically designed for training automated formalization models, aiming to address the shortcomings of existing methods that rely on model parameter memorization, struggle with complex library knowledge, and have a ceiling on single-pass generation capability, thereby improving the formalization accuracy of models across diverse mathematical domains.

原始信息汇总

数据集概述

FormalVerse 是一个经过验证的 Lean 4 自动形式化（autoformalization）数据集，由论文 MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement 发布，对应 arXiv 论文编号 2608.14221。

构建流程

数据集中每个样本均由 MathForm 流水线生成：生成前先检索相关的 Mathlib 数学知识，随后利用 Lean 编译器诊断信息和语义一致性反馈对候选结果进行迭代精炼。仅保留同时通过编译验证和语义验证的样本。

数据集规模与配置

• 规模类别：100K < n < 1M
• 配置：默认配置，包含单个训练集分割（train），数据文件为 data/FormalVerse.jsonl
• 许可证：Apache License 2.0
• 任务类型：文本生成（text-generation）
• 语言：英语

数据字段

每个样本为 JSON 对象，包含以下字段：

字段	类型	描述
id	string	样本唯一标识符
informal_statement	string	自然语言形式的问题描述
formal_statement	string	经过验证的 Lean 4 形式化陈述
source	string	非形式化问题的来源
topic_label	string	问题的数学主题
messages	list	聊天格式的对话记录
model	string	用于生成轨迹的模型

其中 messages 字段包含用户请求将非形式化数学问题转换为 Lean 4 形式化陈述的指令，以及助手模型带有推理过程（reasoning_content）和最终 Lean 4 代码（content）的回复。

数据来源

数据集中的部分非形式化问题来源于以下开放集合：

• Lean-Workbook
• NuminaMath
• DeepMath
• DeepTheorem
• AceReason-Math
• OpenR1-Math
• Principia-Collection

使用方式

可通过 Hugging Face datasets 库加载数据：

python from datasets import load_dataset

dataset = load_dataset("openbmb/FormalVerse", split="train") assistant_message = dataset[0]["messages"][1] print(assistant_message["reasoning_content"]) print(assistant_message["content"])

关联资源

• 论文：https://arxiv.org/abs/2608.14221
• 代码仓库：https://github.com/OpenBMB/MathForm
• 配套模型（MathForm-8B）：https://huggingface.co/openbmb/MathForm-8B

搜集汇总

数据集介绍

构建方式

FormalVerse 数据集依托 MathForm 框架构建，旨在突破传统自动形式化数据构建中依赖模型参数记忆与单次生成的局限。其构建流程始于多元自然语言数学问题的采集与规范化，涵盖 DeepTheorem、NuminaMath、Lean Workbook 等来源，并辅以经典教材中的定理与习题。随后，框架引入检索规划器，通过 LeanExplore 对 Mathlib 进行定向检索，为形式化生成器提供关键定义与既有形式化范例。生成候选经格式检查、Lean 4 编译验证及语义一致性评估后，失败样本携带具体诊断信息进入迭代优化环节，每样本至多三轮，直到通过全部校验。通过此流程，最终产出约 367K 条经过验证的示例，涵盖广泛数学领域与来源。

特点

FormalVerse 的显著特点在于其构建机制带来的高质量与高难度覆盖。相较于传统 Best-of-N 策略仅从单次生成分布中筛选，FormalVerse 通过检索增强和验证引导的迭代修正，将数据难度的天花板提升至流水线整体能力，而非模型单次生成水平。这使得数据集包含大量复杂前置条件、依赖 Mathlib 深度类型层次的高抽象度数学命题，如抽象代数、交换代数等高级领域。此外，每条数据经过严格的编译与语义双重验证，有效避免了编译通过但语义偏差的问题。最终数据规模约 367K 对，涵盖不等式、代数、几何、数论、组合学等多个数学分类，为训练高性能自动形式化模型提供了语义保真度高、领域覆盖广的优质资源。

使用方法

FormalVerse 专为训练自然语言到 Lean 4 的自动形式化模型而设计。每份训练样本包含自然语言命题、重建的形式化推理轨迹以及验证通过的 Lean 4 代码，可直接用于监督微调，使模型学习识别数学对象、逻辑结构与隐式类型约束。数据集还可用于强化学习阶段，例如选取未通过验证的困难命题作为训练信号，配合编译成功与语义一致性二元奖励进行优化。典型应用包括在 Qwen3-8B 基座上微调得到 MathForm-8B，进而通过 DAPO 算法进一步提升。用户可从 Hugging Face 获取数据，并按论文所述流程构建或评估自动形式化系统。

背景与挑战

背景概述

FormalVerse是由清华大学与ModelBest Inc.联合构建的大规模Lean 4自动形式化数据集，于2026年发布，旨在解决自然语言数学命题到机器可验证形式语言的自动转换问题。该数据集由Lushi Pu、Weiming Zhang等人主导，包含约36.7万条经过验证的示例，覆盖竞赛数学、抽象代数、组合学等多个数学领域。其核心研究问题在于克服现有方法过度依赖模型参数记忆、缺乏机制驱动的修正能力等局限，通过知识检索与验证引导的迭代优化构建高保真训练数据。FormalVerse的发布显著推动了自动形式化领域的发展，其配套模型MathForm-8B在多项基准测试中超越了参数规模更大的专用形式化器，为形式数学推理的规模化发展奠定了重要基础。

当前挑战

FormalVerse所面对的挑战贯穿领域问题与数据构建双重维度。就领域问题而言，自动形式化并非简单的翻译任务，模型需精准映射自然语言中的数学概念至Mathlib的复杂类型与定义层级，同时确保生成语句不改变原始命题的语义，尤其在抽象代数等高级领域，任何细微的条件强化或量词错序都会导致形式化失效。就数据构建而言，传统管道依赖单次生成与事后过滤，难以突破模型现有能力上限。FormalVerse的构建尝试通过检索规划与编译器诊断、语义一致性反馈相结合的迭代细化机制应对此挑战，每次失败均转化为具体修正信号，使数据难度上限由整个管道而非单次生成决定，同时需平衡多轮生成的计算成本与数据质量，并通过轨迹重建与去污染确保训练数据的可用性。

常用场景

经典使用场景

FormalVerse数据集的核心应用场景在于大规模数学自动形式化研究，尤其是将自然语言描述的数学命题转换为Lean 4可验证的机器语言。该数据集汇聚了约36.7万条经过验证的形式化样例，广泛涵盖不等式、代数、几何、数论、组合学等多个数学分支。其构建依托于Mathlib知识检索与验证引导的迭代精炼框架，使得研究者能够利用此数据集训练和评估自动形式化模型，推动从非形式化数学到形式化证明的自动化转化，为定理证明器提供高质量的“非形式化-形式化”平行语料。

实际应用

在实际应用中，FormalVerse为训练高效能的自动形式化模型提供了坚实基础。基于该数据集训练的MathForm-8B模型，在多个基准测试中平均语法通过率达88.06%，语义一致性通过率达72.37%，超越了众多32B参数级别的专用形式化模型。这一成果对数学教育、辅助证明编写、形式化验证工具开发等场景具有直接价值，能够加速将现行数学文献转化为机器可检查的证明，降低形式化方法的使用门槛，进而服务于软件验证、安全协议分析等工业级需求。

衍生相关工作

FormalVerse的构建框架MATHFORM衍生了多项具有影响力的后续工作。其知识检索与验证引导的迭代精炼策略启发了后续研究者探索更精细的检索增强生成（如DRIFT）与反馈驱动修正机制（如ReForm）。同时，该数据集对模型训练效能的显著提升，促使学术界重新审视数据质量与模型能力之间的关联，推动了面向形式化数学的高质量数据集构建方法的发展。此外，基于FormalVerse的强化学习训练模式也为自动形式化器的自我进化提供了新的范式，衍生出对形式化推理中语义一致性自动评判方法的深入研究。