IsarStep

IsarStep数据集是由剑桥大学和DeepMind合作创建的，用于评估机器学习模型在高级数学推理能力上的表现。该数据集包含82万条训练样本，覆盖了本科和研究级别的数学及计算机科学定理，主要来源于人类专家在定理证明器中编写的最大证明库。数据集的任务要求模型填补给定证明周围的缺失中间命题，旨在推动机器自动生成人类可读证明的长期目标。IsarStep数据集的创建过程涉及从Achieve of Formal Proofs中挖掘非合成数据，并进行了预处理以减少序列长度和词汇量。该数据集的应用领域主要集中在提高定理证明器的自动化水平，以及解决复杂的数学推理问题。

The IsarStep dataset was collaboratively created by the University of Cambridge and DeepMind to evaluate the advanced mathematical reasoning capabilities of machine learning models. It contains 820,000 training samples covering undergraduate and research-level mathematics and computer science theorems, primarily sourced from the largest proof library compiled by human experts in theorem provers. The core task of this dataset requires models to fill in the missing intermediate propositions surrounding a given proof, with the aim of advancing the long-term goal of automatically generating human-readable proofs by machines. The development of IsarStep involved mining non-synthetic data from the Archive of Formal Proofs, followed by preprocessing to reduce sequence length and vocabulary size. The main application areas of this dataset focus on enhancing the automation level of theorem provers and solving complex mathematical reasoning problems.