INT

INT数据集是一个专为评估定理证明代理泛化能力而设计的基准。它由一个定理生成器支持，该生成器能够产生理论上无限数量的定理和证明，特别适用于测试代理在面对训练时未见过的定理时的表现。INT数据集允许调整问题分布的六个维度，以便深入探究自动定理证明中的多种泛化挑战。此外，INT还提供了一个快速的定理证明环境，支持基于序列和图形的接口，便于进行基于学习的研究。

The INT dataset is a benchmark specifically designed for evaluating the generalization capabilities of theorem-proving agents. It is powered by a theorem generator that can generate a theoretically infinite number of theorems and their corresponding proofs, making it particularly suitable for testing agents' performance when faced with theorems unseen during training. The INT dataset allows adjustment of six dimensions of the problem distribution, enabling in-depth exploration of various generalization challenges in automated theorem proving. Additionally, INT provides a fast theorem proving environment that supports both sequence-based and graph-based interfaces, facilitating learning-based research.