Nemotron-Math-Proofs-v1

Nemotron-Math-Proofs-v1是一个大规模的数学推理数据集，包含约580k自然语言证明问题、约550k Lean 4定理陈述的形式化以及约900k模型生成的推理轨迹，最终形成Lean 4证明。该数据集整合了人类编写的问题与系统生成的形式化和解决方案轨迹。每个自然语言问题由gpt-oss-120b形式化为带有证明占位符的Lean 4定理陈述。推理轨迹和证明由Goedel-Prover-V2-32B尝试生成，并通过Lean 4编译器验证，错误会反馈并尝试自我纠正。该数据集适用于商业用途。

原始信息汇总

Nemotron-Math-Proofs-v1 数据集概述

数据集基本信息

• 数据集名称: Nemotron-Math-Proofs-v1
• 所有者: NVIDIA Corporation
• 创建日期: 2025年12月3日
• 最后修改日期: 2025年12月3日
• 许可证: Creative Commons Attribution-ShareAlike 4.0 International License (CC BY-SA 4.0)
• 语言: 英语
• 数据收集方法: 混合（自动化、合成）

数据集描述

Nemotron-Math-Proofs-v1 是一个大规模数学推理数据集，包含约58万个自然语言证明问题、约55万个Lean 4定理语句的形式化版本，以及约90万个模型生成的推理轨迹，最终形成Lean 4证明。该数据集整合了人工编写的问题与系统生成的形式化和解决方案轨迹。

数据集构成与生成

自然语言问题来源

问题收集自AoPS社区、Math StackExchange和MathOverflow，筛选出基于证明的问题以及可以表述为定理的问题。所有问题都进行了语义去重，并与流行基准进行了去污染处理，最终得到约58万个自然语言定理。

自动形式化

自然语言定理通过由gpt-oss-120b驱动的自动形式化流程，转化为Lean中的形式化语句。该流程包括初始形式化、Lean 4编译检查、回译与语义验证、迭代细化循环、自适应推理和忠实性过滤等阶段，最终得到约55万个形式化定理语句。

自动定理证明

使用Goedel-Prover-V2-32B作为证明器，对定理语句进行大规模推理，以获得推理轨迹和可编译的Lean代码块。证明器流程包括初始证明生成、Lean 4验证、错误增强反馈和迭代细化循环。在证明生成过程中，采用了多轮错误纠正/细化策略，并带有错误轮次删除机制。

数据集格式与量化

• 模态: 文本
• 格式: JSONL
• 结构: 文本 + 元数据
• 训练子集样本数: 239,445
• 总磁盘大小: 约6.2 GB

数据集字段

字段	类型	描述
uuid	str	唯一标识符
messages	list	已验证的证明尝试，作为聊天对话；每个条目生成正确的Lean 4代码
url	`str	null`
user_name	`str	null`
user_url	`str	null`
used_in	list	参考信息，指示哪些Nemotron模型在训练中包含了此样本
tools	list	工具定义

预期用途

• 训练LLMs执行结构化数学推理，特别是生成Lean 4形式化证明。
• 构建长上下文或多轨迹推理系统。
• 研究推理模式、错误模式和验证流程。

局限性

• 难度平衡: 除了筛选证明问题外，没有明确尝试对数据集中的问题进行归一化或平衡。各个阶段（自动形式化成功、证明尝试成功等）存在隐含的选择偏差。
• 令牌计数/长度归一化: 最终验证仅依赖于Lean 4编译器不包含错误。一些包含的解决方案包含许多关于多余生成行（如未使用的假设）的警告。
• 占位符/空洞定义: 观察到自动形式化器使用占位符平凡定义而不是mathlib的情况，例如def MyContinuous... Prop := True。这可以通过最终检查证明仅依赖于三个基础公理来检测。

训练结果

在Qwen3-8B SFT与专门为Lean定理证明训练的Goedel-Prover-V2-8B的比较中，该数据集上训练的模型性能与专门为Lean定理证明训练的模型相当。该数据集被用作Nemotron-Nano-3 SFT数据的一部分。

参考

• Agarwal, Sandhini, et al. gpt-oss-120b & gpt-oss-20b model card. arXiv preprint arXiv:2508.10925 (2025).
• Lin, Yong, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613 (2025).

重要说明

当前上传的数据是一个子集，与用于训练Nemotron-Nano-v3的数据完全匹配。它不包括下面描述的完整数据。我们将在2025年12月17日之前更新上传完整数据集以进行完整的实验复现。

搜集汇总

数据集介绍

构建方式

在数学定理证明领域，构建高质量的形式化数据集对于推动自动推理研究至关重要。Nemotron-Math-Proofs-v1 的构建过程融合了多源自然语言问题收集与自动化形式化转换。初始阶段从 AoPS 社区、Math StackExchange 及 MathOverflow 等平台筛选出约 58 万条证明类问题，经过语义去重和基准去污染处理。随后，通过基于 gpt-oss-120b 的自动形式化流水线，将自然语言定理转化为 Lean 4 形式语句，该流程包含初始形式化、Lean 4 编译检查、回译与语义验证以及迭代优化循环，最终生成约 55 万条形式化定理陈述。证明生成阶段则利用 Goedel-Prover-V2-32B 模型进行大规模推理，通过多轮错误反馈与自我修正机制，产生约 90 万条经过 Lean 4 编译器验证的证明轨迹，确保了形式化证明的严谨性与可靠性。

使用方法

该数据集适用于训练大型语言模型进行结构化数学推理，特别是生成 Lean 4 形式化证明。研究人员可将其用于构建长上下文或多轨迹推理系统，探索不同推理模式与验证流程的效能。使用前需加载 JSONL 格式的数据文件，其中每条记录包含唯一标识符、已验证的证明对话、原始问题来源等元数据。实践过程中，可依据数据集中提供的工具定义与对话结构，设计针对定理证明的微调或推理任务。数据集已用于 Nemotron-Nano-3 等模型的监督微调，在 miniF2F 等基准上展现出优异性能，为后续自动推理研究提供了可靠的基础资源。

背景与挑战

背景概述

Nemotron-Math-Proofs-v1 数据集由 NVIDIA 公司于 2025 年 12 月创建，旨在推动形式化数学与人工智能的交叉研究。该数据集聚焦于数学定理的自动形式化与证明生成这一核心问题，通过整合来自 AoPS 社区、Math StackExchange 和 MathOverflow 的自然语言证明问题，并利用大型语言模型将其转化为 Lean 4 形式化语句及验证通过的证明轨迹。其构建标志着在将自然语言数学推理转化为机器可验证代码的自动化流程上取得了重要进展，为训练具备结构化数学推理能力的大语言模型提供了大规模、高质量的语料资源，对自动定理证明和神经符号计算等领域产生了显著影响。

当前挑战

该数据集致力于解决数学定理自动形式化与证明生成这一领域的核心挑战，其难点在于确保自然语言问题到形式化语句的语义保真度，以及生成可通过 Lean 4 编译器严格验证的完整证明。在构建过程中，研究团队面临多重具体挑战：首先，数据源存在选择偏差，自动形式化与证明生成的成功率隐性地筛选了问题难度，导致数据集的难度分布未经过显式平衡。其次，自动化流程中出现了诸如使用占位符定义代替标准数学库定义等语义失真现象，需额外机制进行检测与过滤。此外，生成的解决方案可能包含大量无关假设或警告信息，对代码的简洁性与规范性构成挑战。

常用场景

经典使用场景

在形式化数学与自动定理证明领域，Nemotron-Math-Proofs-v1数据集为大型语言模型提供了结构化的训练资源。其核心应用场景在于训练模型生成经过Lean 4编译器验证的数学证明，通过约58万道自然语言证明问题及其对应的形式化定理陈述，结合模型生成的推理轨迹，系统性地提升了模型在严格数学逻辑下的推理与代码生成能力。

解决学术问题

该数据集有效应对了形式化数学中自然语言到形式语言的转换难题，以及定理自动证明的可靠性挑战。通过集成自动形式化与验证管道，它为解决数学知识的形式化表示、定理证明的自动化生成以及推理过程的迭代修正等核心学术问题提供了高质量、可验证的数据基础，推动了机器推理在严谨数学领域的实用化进展。

实际应用

在实际应用中，该数据集支撑了智能教育辅助系统的开发，能够为学生提供逐步的数学证明指导与验证。同时，它也为科研工具与软件开发赋能，例如辅助数学家进行形式化验证或集成到代码生成环境中，确保数学软件与算法实现的正确性，在需要高可靠性保证的学术与工业场景中具有重要价值。

数据集最近研究

最新研究方向

在形式化数学与自动定理证明领域，Nemotron-Math-Proofs-v1数据集正推动前沿研究聚焦于大规模语言模型与交互式证明助手的深度融合。该数据集通过集成自然语言问题、Lean 4形式化陈述及模型生成的推理轨迹，为构建具备自我纠错能力的多轮推理系统提供了关键训练资源。当前研究热点围绕如何提升自动形式化的语义保真度与证明生成的迭代效率，利用结构化错误反馈机制优化模型在编译环境中的自适应学习。这一方向不仅加速了可验证人工智能的发展，也为数学教育工具与高可靠性软件验证开辟了新路径，在学术界与工业界均产生了深远影响。