INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
international conference on learning representations, 2021.
We introduce INT, a synthetic INequality Theorem proving benchmark, to tackle the data sparsity and out-of-distribution problems for theorem proving and benchmarked transformer-based and GNN-based agents' generalization performance.
In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time. In this paper, we introduce INT, an INequality Theorem proving benchmark designed to test agents’ generalization ability. INT is based on a theorem generator, which provides theoretically infinite data...More
PPT (Upload PPT)