Leanabell-Prover 数据集

Leanabell-Prover数据集是由快手科技的研究团队创建，包含约152万条形式化语句，以及22万条带有详细非正式评论和验证证明的形式化语句。该数据集用于持续训练和强化学习，以提高自动化定理证明器在 Lean 4 语言中的性能。数据来源于多个项目，包括标准的 Lean 4 数学库Mathlib4、Lean Workbook、Goedel-Prover 和 STP 等合成定理，以及通过PromptCoT 框架合成的数学问题。数据集旨在解决自动化定理证明中形式化语言与自然语言之间的差距问题，推动数学证明生成领域的进展。

The Leanabell-Prover dataset was created by the research team from Kuaishou Technology. It contains approximately 1.52 million formal statements, as well as 220,000 formal statements with detailed informal comments and verified proofs. This dataset is designed for continuous training and reinforcement learning to improve the performance of automated theorem provers in the Lean 4 language. The data is sourced from multiple projects, including the standard Lean 4 mathematical library Mathlib4, Lean Workbook, synthetic theorems from Goedel-Prover and STP, as well as mathematical problems synthesized via the PromptCoT framework. The dataset aims to address the gap between formal languages and natural language in automated theorem proving, and promote advances in the field of mathematical proof generation.

搜集汇总

数据集介绍

构建方式

Leanabell-Prover数据集的构建采用了多阶段训练策略，旨在提升形式化推理能力。首先，研究人员通过混合数据集对现有自动定理证明（ATP）模型进行持续训练，该数据集包含大量陈述-证明对以及模拟人类推理和假设精炼的认知行为数据。随后，利用Lean 4编译器的反馈结果，采用强化学习（GRPO算法）进一步优化模型。这一过程不仅整合了公共和合成数据，还通过自动生成的合成CoT数据嵌入了自我反思能力，如回溯和验证机制，从而显著提升了模型在完整证明生成任务中的表现。

特点

Leanabell-Prover数据集的核心特点在于其专注于形式化推理领域，特别是利用Lean 4代码进行定理证明。该数据集包含1.52M形式化陈述和0.22M带有非正式CoT注释及已验证证明的陈述，覆盖了广泛的数学领域。其独特之处在于通过精心设计的认知行为模板（如Lean补全和重写策略），将自我反思能力整合到基础模型中，从而为后续的强化学习训练奠定了坚实基础。此外，数据集在MiniF2F基准测试中达到了59.8%的通过率（pass@32），展现了其在复杂数学问题求解中的卓越性能。

使用方法

Leanabell-Prover数据集的使用主要围绕形式化定理证明任务展开。研究人员可通过加载预训练模型（如DeepSeek-Prover-v1.5-SFT或Goedel-Prover-SFT）进行微调，利用数据集中的陈述-证明对和认知行为数据提升模型推理能力。对于强化学习阶段，用户需配置Lean 4编译器作为奖励监督，采用GRPO算法优化策略模型。该数据集特别适用于需要高可靠性验证的数学证明场景，用户可通过调整采样预算（如pass@32或pass@128）平衡探索能力与推理效率，同时利用内置的错误分析工具对失败案例进行诊断和改进。

背景与挑战

背景概述

Leanabell-Prover数据集由快手科技的研究团队于2025年提出，旨在推动形式化推理领域的发展。该数据集专注于自动化定理证明（ATP），利用Lean 4代码进行形式化推理。其主要研究人员包括Jingyuan Zhang、Qi Wang等，他们通过结合监督微调和强化学习技术，显著提升了现有定理证明模型的性能。该数据集的核心研究问题是解决自然语言与形式语言在定理证明中的模态差异，其影响力体现在MiniF2F基准测试上达到了59.8%的通过率（pass@32），为形式化推理领域设立了新的技术标准。

当前挑战

Leanabell-Prover数据集面临的挑战主要包括两方面：领域问题的复杂性和构建过程中的技术难题。在领域问题方面，形式化推理需要严格的逻辑验证，而自然语言与形式语言之间的模态差异增加了模型生成正确证明的难度。构建过程中的挑战则体现在数据收集与合成上，高质量的Lean 4代码需要专业数学知识，导致数据规模受限；此外，强化学习中的奖励设计也面临稀疏反馈问题，仅能依赖Lean 4编译器的终端验证结果，难以提供细粒度的训练信号。

常用场景

经典使用场景

Leanabell-Prover数据集在自动定理证明（ATP）领域具有广泛的应用场景，特别是在使用Lean 4代码进行形式化推理时。该数据集通过提供大量高质量的陈述-证明对，以及模拟人类推理行为的认知行为数据，显著提升了模型在形式化证明生成中的表现。其经典使用场景包括数学奥林匹克竞赛级别的定理证明，如MiniF2F测试集上的性能优化。通过结合监督微调（SFT）和强化学习（RL）策略，该数据集能够帮助模型生成完整的数学证明，并在形式化验证环境中获得高通过率。

衍生相关工作

Leanabell-Prover数据集衍生了一系列经典研究工作，特别是在自动定理证明和形式化推理领域。例如，基于该数据集的DeepSeek-Prover-v1.5和Goedel-Prover模型通过结合监督微调和强化学习策略，显著提升了证明生成的性能。此外，数据集还启发了对认知行为在形式化推理中作用的研究，如Gandhi等人的工作揭示了模型自反思能力的重要性。其他相关研究还包括LeanDojo和STP等项目，这些工作进一步扩展了数据集在形式化语言和自然语言推理中的应用范围。

数据集最近研究

最新研究方向

在形式化推理领域，Leanabell-Prover数据集的最新研究聚焦于通过后训练扩展技术提升自动定理证明（ATP）的性能。该研究通过结合监督微调（SFT）和强化学习（RL）策略，显著提升了模型在MiniF2F等数学基准测试中的表现。研究团队设计了一种混合数据集，包含大量形式化陈述-证明对以及模拟人类推理行为的合成数据，从而增强了模型的自我反思能力。此外，利用Lean 4编译器的反馈作为奖励信号，进一步优化了模型的推理能力。这一研究不仅推动了形式化推理领域的前沿发展，还为自然语言与形式语言之间的推理能力迁移提供了新的思路。

相关研究论文

• Leanabell-Prover: Posttraining Scaling in Formal Reasoning

  快手科技 · 2025年