Lean-Github

我们发布了Lean-Github和InternLM2-Step-Prover，这两个资源包括从100多个Lean 4仓库编译的29K定理，以及在Lean-Github和Lean-Workbook上微调的7B模型。该模型在MiniF2F-test、ProofNet和Putnam问题上展示了最先进的性能。

We release two resources, Lean-Github and InternLM2-Step-Prover. These resources comprise 29K theorems compiled from over 100 Lean 4 repositories, alongside a 7B-parameter model fine-tuned on Lean-Github and Lean-Workbook. This model achieves state-of-the-art performance on the MiniF2F-test, ProofNet, and Putnam problems.

原始信息汇总

数据集概述

数据集名称

Lean-Github

数据集描述

Lean-Github 包含从 100 多个 Lean 4 仓库编译的 29K 个定理。

数据集用途

用于训练和评估 7B 模型 InternLM2-Step-Prover，该模型在 MiniF2F-test（54.5%）、ProofNet（18.1%）和 Putnam（5 个问题）上具有最先进的性能。

数据集链接

• 🤗Dataset

相关模型

• 🤗Model

相关论文

• 📑 Paper

许可证

Apache-2.0

引用

@misc{wu2024leangithubcompilinggithublean, title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover}, author={Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen}, year={2024}, eprint={2407.17227}, archivePrefix={arXiv}, primaryClass={cs.AI}, url={https://arxiv.org/abs/2407.17227}, }

搜集汇总

数据集介绍

构建方式

Lean-Github数据集的构建基于100多个Lean 4代码库，通过编译这些代码库中的定理，生成了包含29,000个定理的数据集。该数据集的构建过程不仅涵盖了广泛的数学定理，还确保了数据的多样性和代表性。通过这种方式，数据集能够为形式化验证和自动定理证明提供丰富的训练资源。

特点

Lean-Github数据集的特点在于其广泛的覆盖范围和高质量的数据来源。数据集包含了从多个Lean 4代码库中提取的29,000个定理，涵盖了形式化验证领域的多个方面。此外，该数据集与InternLM2-Step-Prover模型的结合，使得在MiniF2F-test、ProofNet和Putnam等基准测试中取得了领先的性能表现。数据集的高质量和多样性为形式化验证研究提供了坚实的基础。

使用方法

Lean-Github数据集的使用方法主要围绕形式化验证和自动定理证明展开。研究人员可以利用该数据集训练和评估定理证明模型，特别是在Lean 4环境中进行形式化验证。数据集与InternLM2-Step-Prover模型的结合，使得用户可以直接在MiniF2F-test、ProofNet和Putnam等基准测试上进行模型性能的验证。通过这种方式，数据集不仅为理论研究提供了支持，也为实际应用中的定理证明提供了可靠的工具。

背景与挑战

背景概述

Lean-Github数据集由Zijian Wu、Jiayu Wang、Dahua Lin和Kai Chen等研究人员于2024年发布，旨在为形式化验证领域提供丰富的定理证明资源。该数据集从100多个Lean 4代码库中编译了29,000个定理，并结合InternLM2-Step-Prover模型，在MiniF2F-test、ProofNet和Putnam等基准测试中取得了显著成果。Lean-Github的发布不仅推动了自动定理证明技术的发展，还为形式化验证和数学推理领域的研究者提供了宝贵的实验数据，进一步促进了人工智能在数学领域的应用。

当前挑战

Lean-Github数据集在构建过程中面临了多方面的挑战。首先，从大量Lean 4代码库中提取和编译定理需要处理复杂的代码结构和依赖关系，这对数据集的构建提出了较高的技术要求。其次，定理的多样性和复杂性使得模型的训练和验证过程变得尤为困难，尤其是在处理高难度数学问题时。此外，如何确保数据集的覆盖范围和代表性，以支持不同领域的定理证明任务，也是构建过程中需要解决的关键问题。这些挑战不仅体现在数据集的构建上，也直接影响了模型在实际应用中的性能和泛化能力。

常用场景

经典使用场景

Lean-Github数据集在自动定理证明领域具有广泛的应用，特别是在形式化验证和数学定理证明的场景中。该数据集通过整合来自100多个Lean 4仓库的29K定理，为研究人员提供了一个丰富的资源库，用于训练和评估自动定理证明模型。其经典使用场景包括在MiniF2F-test、ProofNet和Putnam等基准测试中进行模型性能评估，帮助研究人员验证和改进自动证明系统的能力。

解决学术问题

Lean-Github数据集解决了自动定理证明领域中的多个关键学术问题。首先，它通过提供大规模的定理数据集，填补了形式化验证领域数据稀缺的空白。其次，该数据集支持研究人员开发更高效的自动证明算法，特别是在处理复杂数学定理时表现出色。此外，Lean-Github还为模型在MiniF2F-test、ProofNet和Putnam等基准测试中的性能提升提供了数据支持，推动了自动定理证明技术的进步。

衍生相关工作

Lean-Github数据集衍生了一系列经典研究工作，特别是在自动定理证明和形式化验证领域。基于该数据集，研究人员开发了InternLM2-Step-Prover模型，该模型在多个基准测试中取得了显著性能提升。此外，该数据集还激发了更多关于大规模定理数据集构建和自动证明算法优化的研究，推动了形式化验证技术的进一步发展。相关研究论文和技术报告在学术界和工业界均产生了广泛影响。