IsarStep: a Benchmark for High-level Mathematical Reasoning
Wenda Li University of Cambridge、Lei Yu DeepMind、Yuhuai Wu University of Toronto, Vector Institute、Lawrence C. Paulson University of Cambridge
Abstract
A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. We build a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover. The dataset has a broad coverage of undergraduate and research-level mathematical and computer science theorems. In our defined task, a model is required to fill in a missing intermediate proposition given surrounding proofs. This task provides a starting point for the long-term goal of having machines generate human-readable proofs automatically. Our experiments and analysis reveal that while the task is challenging, neural models can capture non-trivial mathematical reasoning. We further design a hierarchical transformer that outperforms the transformer baseline. The dataset and models are available from: https://github.com/Wenda302/IsarStep.
中文速览
用机器自动生成数学证明中缺失的中间命题，是迈向自动定理证明的关键一步，但目前缺乏真实、高水准的数据集与评测基准。研究者从 Isabelle 定理证明器的大型形式化证明库中挖掘数据，构建了 IsarStep 数据集（82 万训练样例、词表约 3 万），任务设定为：给定证明中某一步骤前后的命题，要求模型补全中间命题。在此基础上，他们评测了带注意力机制的序列到序列模型和标准 Transformer，并提出了一种分层 Transformer（Hierarchical Transformer，HAT）——先在命题内部建模 token 关系，再在命题之间建模推理关联——在所有模型中表现最优，能正确解决约 15–25% 的测试样例。分析表明，神经模型确实学到了有意义的数学结构，如集合与子集的关系，甚至能完成人类都觉得有难度的多步推理，为将来实现自动生成完整可读证明奠定了重要基础。
原文 arXiv:2006.09265;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2006.09265v2