STP dataset

包含从mathlib4提取的示例、LeanWorkbook声明的正确证明，以及模型在自我玩耍训练期间提出的猜想证明的数据集。

This dataset comprises examples extracted from mathlib4, correct proofs of declarations specified by LeanWorkbook, and proofs of conjectures proposed by the model during self-play training.

原始信息汇总

数据集概述

数据集名称

Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

数据集描述

该数据集是论文《Beyond Limited Data: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving》的官方实现，基于levanter和DeepSeek-Prover-V1.5代码库。数据集包含从mathlib4中提取的示例、LeanWorkbook中的正确证明以及模型在自我博弈训练期间提出的猜测的正确证明。

评价指标

在miniF2F-test和ProofNet-test上的pass@3200性能表现。

模型与数据集

• 模型下载链接：kfdong/STP_model_Lean
• 数据集下载链接：kfdong/STP_Lean

数据集包含：

• 从mathlib4中提取的示例
• LeanWorkbook中的正确证明
• 模型在自我博弈训练期间提出的猜测的正确证明

最终模型是基于DeepSeek-Prover-V1.5-SFT使用本数据集进行1个epoch的微调。

使用环境

实验主要在TPU VMs上运行。

许可

• 代码：本项目遵循MIT许可证。levanter/目录下的代码遵循Apache License 2.0。
• 模型：模型源自DeepSeek，遵循DeepSeek许可协议。

搜集汇总

数据集介绍

构建方式

STP dataset 旨在促进自博弈定理证明器的研究，其构建基于数学库 mathlib4 的提取示例、LeanWorkbook 中的正确证明，以及模型在自博弈训练期间提出的猜想正确证明。该数据集通过从 DeepSeek-Prover-V1.5-SFT 模型进行微调，并利用所述来源的数据进行一个周期的训练，从而形成了最终的数据集。

特点

该数据集的特点在于它结合了数学库的现有数据、工作簿中的证明以及模型自身在训练过程中生成的猜想证明，形成了一个综合性的训练资源。它不仅包含定理证明的标准数据，还整合了自博弈过程中产生的动态数据，为定理证明领域的研究提供了新的视角。

使用方法

使用该数据集时，用户需先在 TPU VM 上配置环境，包括安装必要的依赖如 Levanter、vLLM、Lean4 和 mathlib4。之后，通过执行一系列脚本来准备数据集、初始化模型、进行自博弈训练以及最终的模型重训练。整个过程涉及到多个训练阶段，包括模型初始化、自博弈训练和最终的重训练，以稳定训练效果。

背景与挑战

背景概述

STP dataset是由Dong Kefan和Ma Tengyu于2025年创建，关联于论文《Beyond Limited Data: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving》的官方实现。该数据集及其相关模型主要致力于解决有限数据条件下的定理证明问题，通过自我对弈的方式进行假设和证明。数据集包含了从mathlib4中提取的例子、LeanWorkbook中语句的正确证明，以及模型在自我对弈训练期间提出的假设的正确证明。STP dataset的发布，为定理证明领域提供了新的视角和工具，对相关研究产生了显著影响。

当前挑战

该数据集在构建过程中遇到的挑战主要包括：如何通过自我对弈产生有效的假设和证明，以及如何将这些假设和证明整合到训练数据中，进而提升模型的定理证明能力。此外，数据集在处理数学证明的多样性和复杂性方面也面临挑战。在领域问题上，STP dataset所解决的挑战是如何在有限数据的基础上，实现高效的定理证明，尤其是在miniF2F-test和ProofNet-test这两个测试集上，模型性能的提升和优化是当前研究的重要课题。

常用场景

经典使用场景

STP dataset，作为自博弈定理证明器的官方实现，其经典使用场景在于对数学定理的自动证明。该数据集包含了从mathlib4中提取的示例、LeanWorkbook中语句的正确证明，以及模型在自博弈训练期间提出的猜想的确切证明。这些数据为定理证明领域的研究提供了丰富的实验材料，使得研究者能够深入探索自博弈算法在数学证明中的应用。

解决学术问题

该数据集解决了定理证明中数据不足的难题，通过自博弈的方式生成新的训练数据，增强了模型的泛化能力。这对于提高自动定理证明的准确性和效率具有重要意义，为数学领域的自动化研究提供了新的途径。

衍生相关工作

基于STP dataset的研究衍生出了多个相关工作，包括对自博弈算法的改进、定理证明系统的优化，以及在不同数学分支中的应用探索。这些工作进一步拓展了自动定理证明的边界，推动了相关领域的学术进步和技术发展。