IsarStep：一个面向高层数学推理的基准

一个定义良好的基准对于衡量和加速机器学习模型的研究进展至关重要。在本文中，我们提出了一个面向高层数学推理的基准，并研究了神经序列到序列模型的推理能力。我们从由人类专家在定理证明器中写下的最大证明仓库构建了一个非合成数据集。该数据集广泛覆盖了本科与研究水平的数学与计算机科学定理。在我们定义的任务中，模型需要在给定周围证明的情况下填补一个缺失的中间命题。该任务为让机器自动生成人类可读证明这一长期目标提供了起点。我们的实验与分析揭示，尽管任务具有挑战性，神经模型能够捕捉非平凡的数学推理。我们进一步设计了一个分层 transformer，其性能优于 transformer 基线。