FineLeanCorpus

FineLeanCorpus 是一个包含超过 28.5 万个数学问题的数据集，涵盖了广泛的数学领域和难度等级。该数据集经过严格的人类评估，保证了其高正确性。FineLeanCorpus 的创建基于 CriticLean 框架，旨在评估模型区分语义正确和错误形式化的能力。数据集的多样性、难度分布和严格的语义验证，使其成为一个结构平衡的训练环境，有助于解决数学自动形式化中的挑战。FineLeanCorpus is a dataset containing over 285,000 mathematical problems, covering a wide range of mathematical fields and difficulty levels. This dataset has undergone rigorous human evaluation to ensure its high correctness. FineLeanCorpus is developed based on the CriticLean framework, aiming to evaluate a model's ability to distinguish between semantically correct and incorrect formalizations. The diversity, difficulty distribution, and strict semantic verification of the dataset make it a structurally balanced training environment that helps address the challenges in automated mathematical formalization.

原始信息汇总

CriticLean 数据集概述

1. 数据集简介

• 名称: CriticLean
• 目的: 通过批评者引导的强化学习框架解决数学陈述形式化问题
• 核心组件:
  • CriticLeanGPT: 基于强化学习的模型
  • CriticLeanBench: 评估基准
  • FineLeanCorpus: 已验证的Lean 4语句数据集

2. 主要数据集

2.1 CriticLeanInstruct

• CriticLean_12K: 全部批评者数据
• CriticLean_4K: 种子数据，用于强化学习
• CriticLean_Mix_48K: 混合数据集，包含12K批评者数据+18K数学数据+18K代码数据
• CriticLean_Mix_16K: 混合数据集，包含4K批评者数据+6K数学数据+6K代码数据

2.2 CriticLeanBench

• 规模: 500对自然语言和Lean 4语句(250正确,250错误)
• 特点:
  • 双焦点: 批评能力和Lean 4形式验证
  • 多样化覆盖: 不同数学领域和难度级别
  • 结构化错误: 常见错误模式设计
  • 人工验证: 所有样本经过严格验证
• 评估指标: ACC/TPR/FPR/TNR/FNR

2.3 FineLeanCorpus

• 规模: 285,957条已验证Lean 4语句
• 特点:
  • 规模大: 显著超过现有Lean 4问题集
  • 高质量: 84%准确率
  • 多样化: 覆盖多个数学领域和难度级别
  • 严格验证: 通过Lean编译器和CriticLean模型验证

3. 模型变体

基础模型	SFT应用	SFT数据	RL应用	RL数据	模型名称
Qwen2.5-Instruct	是	CriticLean_4K	否	*	Qwen2.5-Instruct-SFT(Critic Only)
Qwen2.5-Instruct	是	CriticLean_Mix_16K	否	*	Qwen2.5-Instruct-SFT(16K)
Qwen2.5-Instruct	是	CriticLean_Mix_48K	否	*	Qwen2.5-Instruct-SFT
Qwen2.5-Instruct	是	CriticLean_Mix_48K	是	CriticLean_4K	Qwen2.5-Instruct-SFT-RL
Qwen2.5-Instruct	否	*	是	CriticLean_4K	Qwen2.5-Instruct-RL
Qwen3	否	*	是	CriticLean_4K	Qwen3-RL

4. 数据来源

• AOPs
• DeepMath-103k
• NuminaMath-TIR
• DeepTheorem
• DeepScaleR
• DAPO-Math-17k
• Omni-Math
• InwqMath
• BlueMO
• TAL-SCQ5K
• OnlineMathContest
• Multi-Source Math Competition

5. 许可信息

• 许可证: Apache-2.0 license

6. 引用信息

bibtex @misc{peng2025criticleancriticguidedreinforcementlearning, title={CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization}, author={Zhongyuan Peng and Yifan Yao and Kaijing Ma and Shuyue Guo and Yizhe Li and Yichi Zhang and Chenchen Zhang and Yifan Zhang and Zhouliang Yu and Luming Li and Minghao Liu and Yihang Xia and Jiawei Shen and Yuchen Wu and Yixin Cao and Zhaoxiang Zhang and Wenhao Huang and Jiaheng Liu and Ge Zhang}, year={2025}, eprint={2507.06181}, archivePrefix={arXiv}, primaryClass={cs.CL}, url={https://arxiv.org/abs/2507.06181}, }

搜集汇总

数据集介绍

构建方式

在数学自动形式化领域，FineLeanCorpus数据集的构建采用了CriticLean框架的严格验证流程。研究团队首先从多元数学资源（如奥赛题库、本科数学问题集等）收集自然语言数学问题，通过Kimina-Autoformalizer-7B模型生成初始Lean4形式化代码。随后采用双重验证机制：先通过Lean4编译器进行语法校验，再经由强化学习优化的CriticLeanGPT模型进行语义一致性评估。该流程采用迭代式生成-验证策略，对未通过验证的样本进行多轮重构（最高200次尝试），最终仅保留同时通过编译检查和语义验证的样本。整个流程产出28.6万条经双重验证的形式化问题，并额外精选3.6万条高难度问题构成Diamond子集。

特点

FineLeanCorpus在数学形式化数据集领域展现出三大核心特征：领域覆盖方面，其问题均匀分布于代数、几何、数论等16个主要数学分支，其中不等式（75,339条）、积分（18,761条）等子领域数量尤为丰富；难度谱系上，数据集呈现多峰分布，既包含基础训练所需的中低难度问题（1-4级），又涵盖占比11.1%的顶级难题（≥6级），最高难度达9.5级；质量管控维度，通过CriticLean框架的语义验证使形式化准确率达84%，较单纯编译检查提升30个百分点。与同类数据集Lean-Workbook相比，其问题数量翻倍且高难度样本比例提高42%。

使用方法

该数据集支持三种典型应用范式：监督学习场景下，可直接使用问题-形式化对进行端到端训练，建议配合CriticLeanInstruct的1:3数学-代码混合比例优化模型推理能力；强化学习应用中，可将编译错误和语义批判作为奖励信号，通过GRPO等算法微调模型；评估基准构建时，建议按6:2:2划分训练/验证/测试集，对高难度任务优先采用Diamond子集。使用时应特别注意：自然语言陈述平均长度78.4词，需调整模型上下文窗口；形式化代码平均87.8个token，建议采用Qwen2.5等支持32k上下文的模型进行处理。

背景与挑战

背景概述

FineLeanCorpus是由字节跳动与南京大学的研究团队于2025年7月8日联合发布的大规模数学形式化数据集，旨在解决自然语言数学陈述向Lean 4形式化代码转换的核心挑战。该数据集包含28.5万条经过严格验证的数学问题，覆盖从高中奥赛到本科高等数学的广泛难度谱系，其创新性在于通过CriticLean框架实现了语义保真度的强化验证，将传统形式化流程中的被动校验升级为主动学习环节。作为首个融合领域多样性、难度平衡性和语义一致性的开源Lean 4数据集，FineLeanCorpus显著推动了自动定理证明领域的发展，相关成果发表在强化学习与形式化方法交叉领域的顶级会议上。

当前挑战

FineLeanCorpus面临双重挑战：在领域问题层面，数学陈述的语义精确形式化要求模型同时具备深度的数学理解力和严格的逻辑表达能力，现有方法在复杂命题的语义对齐（如高阶组合问题的不变式保持）和跨领域泛化（如几何命题的拓扑约束转换）上仍有显著差距；在构建过程中，数据质量保障需克服编译通过但语义偏离的'假阳性'样本筛选难题，其多阶段验证流程（包括编译器检查、CriticLeanGPT模型评估及人工复核）虽将准确率提升至84%，但代价是每个样本平均需5次迭代生成，导致构建效率与覆盖度的权衡困境。此外，数据集的领域平衡性要求对稀疏子领域（如图论中的树结构问题）进行针对性增强，这对源数据的广度和标注专家的领域专长提出极高要求。

常用场景

经典使用场景

FineLeanCorpus数据集在数学自动形式化领域具有广泛的应用场景，特别是在将自然语言数学问题转换为Lean 4形式化代码的过程中。该数据集通过其丰富的数学领域多样性和难度覆盖，为研究者提供了一个可靠的基准，用于评估和优化形式化模型的性能。其经典使用场景包括训练和评估CriticLeanGPT等模型，以确保生成的代码不仅在语法上正确，而且在语义上准确反映原始问题的意图。

衍生相关工作

FineLeanCorpus的推出催生了一系列相关研究工作。例如，基于该数据集开发的CriticLean框架和CriticLeanGPT模型，显著提升了数学形式化的语义准确性。此外，该数据集还启发了其他研究团队开发类似的高质量形式化数据集，如LeanWorkBook的改进版本。这些衍生工作进一步推动了数学自动形式化领域的发展，并为未来的研究提供了丰富的资源和灵感。

数据集最近研究

最新研究方向

FineLeanCorpus数据集的最新研究方向聚焦于数学自动形式化领域，特别是通过CriticLean框架优化批评阶段，以提升自然语言数学问题向Lean 4形式化代码转换的语义保真度。该数据集凭借其丰富的领域多样性、广泛的难度覆盖以及严格的人工验证，为数学推理的上层研究提供了坚实基础。CriticLeanGPT模型的引入，通过监督微调和强化学习的结合，显著提升了模型在区分语义正确与错误形式化方面的能力，为自动定理证明领域开辟了新路径。

相关研究论文

• CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization

  字节跳动种子南京大学 · 2025年