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.

搜集汇总

数据集介绍

构建方式

IsarStep数据集源自形式化证明的权威宝库——Archive of Formal Proofs (AFP) 与Isabelle/HOL标准库，共涵盖204K个经机器验证的引理。研究团队通过挖掘人类专家在定理证明器中撰写的声明式证明，构建了非合成的数据集。每个样本由五个部分组成：目标命题、推导目标所用的局部命题、由目标导出的局部命题、其他局部命题及库引理，以及可选的辅助引理集。经过自由变量归一化与冗余括号移除等预处理，最终获得820K训练样本、5K验证样本与5K测试样本，词汇量约30K。

特点

该数据集聚焦于高等数学推理，涵盖基础逻辑、高级分析、计算机代数与密码学等广泛主题，涉及本科至研究级别的数学与计算机科学定理。其核心任务为中间命题合成——模型需根据上下文填补证明步骤间的缺失环节，这要求模型理解数学概念间的深层关联（如集合、子集与成员关系），并能进行多步推理。实验表明，尽管任务具有挑战性，神经序列到序列模型可捕捉非平凡的数学逻辑，且层级化Transformer在长序列上表现尤为突出。

使用方法

IsarStep任务被形式化为序列到序列的预测问题：给定源命题序列（含类别标注），模型需生成目标命题的token序列。研究者提供了三种基线模型——带注意力的RNN、Transformer及层级化Transformer（HAT），其中HAT通过局部层建模命题内token关联、全局层建模命题间交互，更显式地捕捉推理结构。评估指标包括精确匹配准确率与BLEU分数，并设计了测试套件将生成命题回传至Isabelle环境，利用自动定理证明器验证其正确性。数据集与模型代码已开源，便于复现与拓展。

背景与挑战

背景概述

在数学推理领域，构建一个能够衡量机器学习模型高阶推理能力的基准测试至关重要。IsarStep数据集由剑桥大学的Wenda Li、Lawrence C. Paulson以及DeepMind的Lei Yu、多伦多大学的Yuhuai Wu于2021年共同创建，发表于ICLR 2021。该数据集源自Isabelle/HOL定理证明器中人类专家撰写的最大规模证明库（Archive of Formal Proofs），涵盖本科及研究级数学与计算机科学定理。核心研究问题在于评估神经序列到序列模型能否生成高层次的中间命题，以弥合证明步骤间的鸿沟。IsarStep的提出为自动化定理证明和机器生成可读证明奠定了重要基础，其非合成特性与30K词汇量显著区别于以往的小规模合成数据集，推动了数学推理领域的研究进展。

当前挑战

IsarStep面临的挑战首先在于领域问题的复杂性：任务要求模型从给定上下文预测缺失的中间命题，这需要理解数学概念（如线性代数中的行列式、复分析中的留数）及其逻辑关联，而非简单的模式匹配。搜索空间为Σ*，每一步需从30K个动作中抉择，且输出长度无预设上限。其次，数据集构建过程中存在显著挑战：原始数据包含冗长命题和大量唯一标记，需通过自由变量归一化和去除冗余括号等预处理技巧来降低序列长度与词汇量；同时需处理类型推断、去重及避免训练集与测试集同源，最终从120万数据点中筛选出82万训练样本、1万验证与测试样本。这些步骤对数据质量与模型性能构成双重考验。

常用场景

经典使用场景

IsarStep数据集最经典的使用场景是作为高阶数学推理的基准测试平台，用于评估序列到序列模型在非合成、真实世界数学证明中的推理能力。该任务要求模型根据给定的上下文证明步骤，填补缺失的中间命题，模拟人类数学家证明定理时提出关键中间步骤的思维过程。由于数据集涵盖从基础逻辑到高级分析、计算机代数等广泛学科，且证明步骤跨度大，无法通过简单模式匹配解决，因此成为检验模型是否真正理解数学概念及其逻辑关联的试金石。

衍生相关工作

IsarStep数据集衍生了一系列相关经典工作，包括分层Transformer（HAT）架构的提出，该模型通过局部层编码命题内部标记关系、全局层捕捉命题间关联，在长序列推理上性能显著优于标准Transformer。此外，该数据集催生了利用预训练语言模型（如GPT-2、GPT-3）进行数学猜想生成的研究，以及结合自动定理证明器验证生成命题正确性的测试套件。后续工作还探索了基于该数据集的类型推断、目标分类与排名任务，推动了机器学习与形式化验证交叉领域的发展。

数据集最近研究

最新研究方向

在高级数学推理领域，IsarStep数据集为评估神经序列到序列模型的推理能力提供了非合成、高难度的基准。当前前沿研究方向聚焦于利用层次化Transformer架构捕捉命题间的复杂逻辑关系，并通过中间命题生成任务推动定理证明自动化的突破。该数据集源于Isabelle/HOL形式化证明库，涵盖本科至研究级别的数学与计算机科学定理，其意义在于模拟人类数学推理中关键中间步骤的构想过程。相关热点事件包括神经模型在集合论、测度论及复分析等主题上展现的多步推理能力，例如模型能隐式调用反身性引理或整合子代数与测度空间定义。这一研究方向不仅揭示了神经网络在符号操作与概念映射上的潜力，也为构建可生成类人可读证明的自动化系统奠定了基石。

相关研究论文

• IsarStep: a Benchmark for High-level Mathematical Reasoning

  剑桥大学 · 2021年