reasoning_data

reasoning_data 是一个用于 Lean 4 定理证明的数据集，包含非正式推理轨迹（proof_plan）以及每个提示/答案对的编译器反馈注释版本。数据集分为训练集和测试集：训练集（70,451 个样本）包含已解决的问题，每行带有已验证的证明、反馈注释变体和证明计划；测试集（66,593 个样本）包含未解决的问题池，仅提供提示，适合用于评估或生成。数据集字段包括 uuid、data_source、question、answer、question_feedback、answer_feedback 等。其中 question 和 answer 是用于阶段二监督微调（SFT）的文本，要求模型在给出 Lean 证明前先提供非正式解决方案，并将证明计划嵌入在证明之前。source_* 字段保留阶段一指令的原始文本，用于对比。proof_plan 字段包含推理段列表，非修复行仅包含一个段，包含问题重述、有用观察、推理路径、关键推导、证明类型、形式锚点和最终解决方案等部分；修复行则包含多个段，每个段对应一次尝试，并包含错误分析、修订推理和更新证明计划。valid 表示证明是否编译通过，proof_repair 表示是否为多轮修复会话。此外还包含 token_count、tactic_count、lean_score、lean_rank 等统计信息。该数据集适用于训练大语言模型进行 Lean 4 定理证明，特别是结合非正式推理和编译器反馈的训练。reasoning_data is a dataset for Lean 4 theorem proving, containing informal reasoning traces (proof_plan) and compiler feedback annotated versions of each prompt/answer pair. The dataset is divided into training and test sets: the training set (70,451 samples) contains solved problems with verified proofs, feedback annotation variants, and proof plans; the test set (66,593 samples) contains an unsolved problem pool with only prompts, suitable for evaluation or generation. Dataset fields include uuid, data_source, question, answer, question_feedback, answer_feedback, etc. The question and answer are texts used for stage two supervised fine-tuning (SFT), requiring the model to provide an informal solution before giving a Lean proof and embed the proof plan before the proof. The source_* fields retain the original text of stage one instructions for comparison. The proof_plan field contains a list of reasoning segments; non-repair rows contain only one segment with problem restatement, useful observations, reasoning path, key derivation, proof type, formal anchor, and final solution; repair rows contain multiple segments, each corresponding to one attempt, including error analysis, revised reasoning, and updated proof plan. valid indicates whether the proof compiles, and proof_repair indicates whether it is a multi-turn repair session. Additionally, there are statistics such as token_count, tactic_count, lean_score, lean_rank. This dataset is suitable for training large language models in Lean 4 theorem proving, particularly combining informal reasoning and compiler feedback.

原始信息汇总

数据集概述

数据集名称：reasoning_data
发布方：formalmathatepfl（EPFL 形式数学团队）
数据类型：Lean 4 定理证明数据，附带非形式化推理轨迹（proof_plan）及编译器反馈标注的提示/答案对。
许可与访问：通过 Hugging Face 平台托管，地址为 https://huggingface.co/datasets/formalmathatepfl/reasoning_data。

---

数据集结构

数据划分（Splits）

• train（训练集）：包含已解决的问题，共 70,451 个样本，每个样本均带有验证过的证明、带反馈标注的变体以及推理计划。其中 proof_repair == True 的行代表多次尝试的修复会话。
• test（测试集）：包含未解决的问题池，共 66,593 个样本，仅包含题目（answer 为空，answer_feedback/valid 为 null，proof_plan 为 []）。

数据规模

• 下载大小：约 1.27 GB（1,274,545,789 字节）
• 数据集总大小：约 3.51 GB（3,507,847,653 字节）
• 训练集大小：约 3.25 GB（3,247,622,250 字节）
• 测试集大小：约 260 MB（260,225,403 字节）

---

数据字段说明

字段名	类型	内容描述
uuid	string	源数据集的标识符（不同形式化可能重复，如来自 NuminaMath-LEAN）
data_source	string	来源数据集名称
question	string	替换为阶段二指令的源问题；修复行中每个失败尝试前附带其计划片段
answer	string	计划片段（修复行为最后一个）+ 空行 + source_answer
question_feedback	string	source_question_feedback 替换为阶段二指令；修复行每个失败尝试前附带计划片段
answer_feedback	string	直接行：计划 + 空行 + source_answer_feedback；修复行：最后错误块 + 最后计划片段 + 修正后的反馈标注证明
source_question	string	与 formalmathatepfl/sft_classic 完全一致的提示文本
source_answer	string	与 formalmathatepfl/sft_classic 完全一致的答案文本
source_question_feedback	string	与 formalmathatepfl/feedback_data_training 完全一致的提示文本
source_answer_feedback	string	与 formalmathatepfl/feedback_data_training 完全一致的反馈标注证明
proof_plan	list[string]	推理分段列表；非修复行：一个分段含 [问题重述]、[有用观察]、[推理路径]、[关键推导]、[证明类型]、[形式锚点]、[最终解答]；修复行：每个尝试一个分段，首段含上述章节，后续含 [错误分析]、[修订推理]、[更新证明计划]
valid	bool	该证明是否通过编译（未被重新验证时为 null）
proof_repair	bool	该行是否为修复会话（多次尝试）
lean_code	string	已验证的证明（不含反馈块）
token_count	float64	证明统计信息（源池中缺失时为 null）
tactic_count	float64	证明统计信息（源池中缺失时为 null）
lean_score	float64	证明统计信息（源池中缺失时为 null）
lean_rank	float64	证明统计信息（源池中缺失时为 null）

---

提示指令说明

• 阶段二（SFT 阶段 2）指令：
  “Replace every sorry statement with an appropriate proof. Before writing any Lean code, give an informal solution with the sections [Problem Restatement], [Useful Observations], [Reasoning Path], [Key Derivation], [Proof Type], [Formal Anchors] and [Final Solution]. Then provide the complete solution in the lean4 code block. If a previous attempt failed, first give [Error Analysis], [Revised Reasoning] and [Updated Proof Plan], then provide the corrected solution.”
  question_feedback 在此基础上增加要求：在适当位置以 /- <feedback> ... </feedback> -/ 形式插入 Lean 4 编译器反馈块。

• 阶段一（SFT 阶段 1）指令（即 source_* 列中的文本）：
  与 formalmathatepfl/sft_classic 及 formalmathatepfl/feedback_data_training 完全一致的提示格式。

---

用途与背景

该数据集用于训练语言模型进行 Lean 4 定理证明，重点提升模型在 形式化证明生成 及 编译器反馈理解与修复 方面的能力。其特色在于每个问题/答案对都包含非形式化的推理计划（proof_plan）以及带有编译器反馈标注的变体（*_feedback 列），支持两阶段监督微调（Phase-1 SFT 与 Phase-2 SFT）以及错误修复（proof repair）场景的训练。

搜集汇总

数据集介绍

构建方式

该数据集立足于Lean 4定理证明这一形式化数学的前沿阵地，其构建深度依托于既有形式化数学语料库（如NuminaMath-LEAN与formalmathatepfl系列数据）的系统性整合与再加工。构建过程以已获验证的Lean 4证明为起点，通过程序化方式将非形式化的推理轨迹（proof_plan）嵌入原始问答对，从而生成兼具自然语言推理与形式化代码的复合训练样本。针对多轮修复场景，构建流程保留了每一次失败尝试及其对应的编译器反馈信息，并依照证明修复的实际时间顺序组织推理片段。每条数据均附带proof_plan、lean_code、验证状态及证明统计等多维标注，并通过train与test两个划分区分已解问题与待解问题池，形成了层次分明、用途明确的数据结构。

特点

该数据集的显著特征在于其将非形式化推理与形式化证明紧密耦合，每一问答对均配有结构化的推理计划（proof_plan），并针对编译器反馈进行了专门标注。数据集中区分了直接求解与多轮修复两类样本，修复样本完整保留了从错误分析到修正证明的全过程，使模型得以学习“错误—计划—修正证明”的渐进式推理模式。问答文本存在source_*与phase-2两种模板变体，前者与既有SFT数据字节级对齐，后者嵌入了推理计划并调整了指令措辞。数据集还提供了valid、proof_repair、token_count、tactic_count、lean_score与lean_rank等丰富元信息，为样本筛选、难度评估与训练策略设计提供了充分依据。

使用方法

在使用该数据集时，研究者应首先依据训练目标选择对应的文本列：若进行第二阶段监督微调，应以question/answer及question_feedback/answer_feedback作为训练文本，其中提示要求模型先给出包含[Problem Restatement]、[Useful Observations]、[Reasoning Path]等章节的非形式化解答，再输出完整的Lean 4代码块。对于涉及证明修复的样本，可将question_feedback与answer_feedback串联使用，使模型学习从编译器错误反馈到修正证明的映射关系。source_*列则适用于与既有第一阶段SFT数据保持一致的训练场景。测试划分仅提供提示文本，可用于评估模型在无参考答案条件下的定理证明能力。通过proof_plan字段，还可将推理计划作为中间监督信号嵌入训练流程，或用于分析模型的推理路径质量。

背景与挑战

背景概述

自动定理证明长期被视为人工智能的试金石，其形式化验证的严苛性要求机器同时具备逻辑推演与代码生成能力。近年来，Lean 4 凭借其依赖类型系统和活跃的数学库社区，已成为形式化数学研究的主流工具。然而，公开的 Lean 4 证明数据大多仅包含最终验证通过的代码，缺失人类可读的推理轨迹与编译器反馈的迭代信息。reasoning_data 数据集于上述背景下构建，汇集了来自 NuminaMath-LEAN 等来源的七万余条已解问题与六万余条未解问题，由 formalmathatepfl 团队发布。该数据集的核心贡献在于为每个问题配对提供了非形式化推理规划（proof_plan）以及编译器反馈标注的变体，旨在推动模型学习从错误中修复证明的能力。其影响力体现在为 Lean 4 证明生成任务提供了稀缺的“过程级”监督信号，有望促进更鲁棒、可解释的定理证明器发展。

当前挑战

该数据集所应对的领域问题——Lean 4 定理证明——本身即面临多重挑战：形式化证明的搜索空间巨大，正确证明往往需要长程依赖与创造性策略；编译器反馈虽能定位错误，但将自然语言推理规划与 Lean 4 语法及策略语义精确对齐极为困难。在数据集构建过程中，主要挑战包括：从多个来源汇集并统一不同模板的提示与答案格式，确保 source 列与 phase-1 数据字节级一致；为修复会话（proof_repair）生成连贯的多轮错误分析、修订推理与更新证明规划，需人工或半自动地标注每轮尝试的反馈块；验证所有训练样本的 Lean 4 代码是否类型检查通过，并处理未解问题池中答案与反馈的空值。这些挑战共同决定了数据集在支撑模型学习迭代修复与规划嵌入时，仍需持续优化标注一致性与覆盖范围。

常用场景

经典使用场景

在形式化数学与自动定理证明领域，reasoning_data数据集最经典的使用场景是训练Lean 4定理证明模型执行非形式化推理与形式化验证的联合生成任务。模型需先输出包含[Problem Restatement]、[Useful Observations]、[Reasoning Path]等结构化节段的非形式化证明规划，再生成完整的Lean 4代码。该数据集特别支持编译器反馈驱动的证明修复训练，要求模型在首轮尝试失败后，依据Lean 4编译器错误信息进行错误分析、修订推理路径并输出修正后的证明，从而模拟人类数学家在证明助手辅助下的迭代调试过程。

解决学术问题

该数据集直面形式化数学研究中长期存在的核心难题：非形式化数学直觉与形式化验证之间的鸿沟。传统方法将自然语言证明与Lean代码分离处理，导致模型缺乏对证明策略的深层理解，难以在编译失败时自主纠错。reasoning_data通过将证明规划、编译器反馈与验证证明组织为连贯的多轮修复会话，为研究“错误驱动的推理修订”提供了结构化监督信号。其意义在于推动定理证明从单次生成范式转向迭代精化范式，显著提升模型在复杂数学问题上的证明成功率与鲁棒性，为神经符号推理研究树立了新的数据基准。

衍生相关工作

reasoning_data的发布催生了一系列围绕形式化推理与反馈驱动学习的研究工作。基于其phase-1与phase-2指令模板，后续研究探索了多阶段监督微调策略在定理证明中的迁移效果，并对比了非形式化规划对形式化代码生成的增益。该数据集衍生的经典工作还包括：利用编译器反馈构建强化学习奖励信号的证明修复模型，以及将proof_plan作为中间推理链进行思维链蒸馏的轻量化证明器。在基准评测方面，其test划分的未解决问题池被广泛用于评估模型的零样本证明能力，推动了Lean 4定理证明排行榜的建立与迭代。