FormalVerse
收藏资源简介：
FormalVerse 是一个经过验证的 Lean 4 自动形式化数据集，与论文《MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement》一同发布。该数据集由 MathForm 流水线生成，该流水线在生成之前检索相关的 Mathlib 知识，并利用 Lean 编译器诊断和语义一致性反馈对每个候选进行细化，最终只保留通过编译和语义验证的样本。数据集包含约 10 万到 100 万个样本，每条样本为 JSON 格式，包含以下字段：id（唯一标识符）、informal_statement（自然语言问题）、formal_statement（经过验证的 Lean 4 语句）、source（非正式问题的来源）、topic_label（数学主题标签）、messages（聊天格式的对话）、model（生成轨迹所使用的模型）。数据集适用于数学自动形式化、形式化验证、推理等任务，也可用于训练文本生成模型。数据可通过 Hugging Face Datasets 库加载，许可证为 Apache 2.0。
FormalVerse is a verified Lean 4 auto-formalization dataset, released with the paper MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement. The dataset is generated by the MathForm pipeline, which retrieves relevant Mathlib knowledge before generation, and refines each candidate using Lean compiler diagnostics and semantic consistency feedback, ultimately retaining only samples that pass compilation and semantic verification. The dataset contains approximately 100,000 to 1,000,000 samples, each in JSON format with the following fields: id (unique identifier), informal_statement (natural language problem), formal_statement (verified Lean 4 statement), source (source of the informal problem), topic_label (mathematical topic label), messages (dialogue in chat format), model (model used for generating the trajectory). The dataset is suitable for tasks such as mathematical auto-formalization, formal verification, and reasoning, and can also be used to train text generation models. The data can be loaded via the Hugging Face Datasets library, and is licensed under Apache 2.0.
数据集概述：FormalVerse
FormalVerse 是一个经过验证的 Lean 4 自动形式化（autoformalization）数据集，由论文 MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement 发布。该数据集中的所有样本均由 MathForm 流水线生成，该流水线在生成前检索相关的 Mathlib 知识，并使用 Lean 编译器诊断和语义一致性反馈对每个候选进行优化，最终仅保留通过编译和语义验证的样本。
- 许可证：Apache License 2.0
- 任务类别：文本生成（text-generation）
- 语言：英语（en）
- 标签：arXiv:2608.14221、lean4、autoformalization、mathematics、formal-verification、reasoning
- 数据集规模：100K < n < 1M（即超过10万条样本）
- 配置信息：默认配置，数据文件位于
data/FormalVerse.jsonl，仅包含训练集（train）分割。
数据字段
每条数据是一个 JSON 对象，包含以下字段：
| 字段 | 类型 | 描述 |
|---|---|---|
id |
string | 样本的唯一标识符 |
informal_statement |
string | 自然语言形式的问题描述 |
formal_statement |
string | 经过验证的 Lean 4 形式化命题 |
source |
string | 非形式化问题的来源 |
topic_label |
string | 问题的数学主题 |
messages |
list | 对话格式的交互记录 |
model |
string | 用于生成轨迹的模型 |
数据示例
示例样本包含以下内容：
- 非形式化问题："求整除表达式 (13^4 - 11^4) 的 2 的最高次幂。将答案表示为单个整数。证明答案为 32。"
- 形式化命题：Lean 4 代码，使用
import Mathlib.Data.Nat.Basic等 import 语句，并定义了定理my_favorite_theorem。 - 来源：AceReason-Math
- 主题标签：数论（Number Theory）
- 对话记录：包含用户请求将非形式化数学问题转换为 Lean 4 形式化命题的消息，以及助手模型的推理过程（
reasoning_content）和最终代码答案（content）。 - 生成模型：gpt-oss-120b
使用方式
可通过 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"])
致谢与来源
部分非形式化问题源自以下公开数据集：
引用
如需引用该数据集，请参照 README 中提供的 BibTeX 引用信息（arXiv:2608.14221）。
其他资源
- 论文：arXiv:2608.14221
- 代码库：MathForm GitHub 仓库
- 模型：MathForm-8B
图示说明
README 中包含两张示意图：
- MathForm 数据构建与训练流水线概览：展示系统如何结合 Mathlib 知识检索、编译与语义验证、迭代优化来生成可靠的形式化数据，并进行轨迹重构和 MathForm-8B 训练。
- FormalVerse 的来源分布与主题分布：分别展示问题来源和数学主题的分布情况。
注：上述图片链接均为相对路径（如
./assets/data-pipeline.png），无法转换为绝对地址。数据集页面本身位于 FormalVerse 数据集主页。
