The benchmark generates synthetic inequality proofs from axioms and varies properties of training and test distributions so researchers can distinguish memorization-like success from different forms of out-of-distribution theorem-proving generalization.
INT introduced an inequality theorem-proving benchmark with a theoretically unbounded theorem-and-proof generator, six controlled generalization settings, and fast sequence- and graph-based interfaces for training and evaluating proof agents.
It supplied an early controlled testbed for a problem that remains central to learned theorem proving: whether a prover can transfer beyond theorem shapes and proof patterns seen during training.
Significance rationale: INT reframed theorem-proving evaluation around controlled generalization rather than only aggregate proof success, using a theorem generator to expose distinct distribution shifts and providing a lightweight environment for learning-based prover research.
—
—
The arXiv research record established the INT benchmark, theorem generator and reported generalization experiments.
The Chronicle linked the ICLR 2021 research record and the authors' public INT repository containing the proving environment, generator and training code. E3 denotes inspectable artifacts, not independent verification of benchmark conclusions.
No corrections recorded.
