INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

By Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, Roger Baker Grosse. 2020

60 citations recorded by the source corpus.

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, specifically designed to test agents' generalization ability. INT is based on a procedure for generating theorems and proofs; this procedure's knobs allow us to measure 6 different types of generalization, each reflecting a distinct challenge characteristic to automated theorem proving. In addition, unlike prior benchmarks for learning-assisted theorem proving, INT provides a lightweight and user-friendly theorem proving environment with fast simulations, conducive to performing learning-based and search-based research. We introduce learning-based baselines and evaluate them across 6 dimensions of generalization with the benchmark. We then evaluate the same agents augmented with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help to prove new theorems.

Subfields: Artificial Intelligence, Evaluation & Benchmarks

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Evaluation & Benchmarks

Citations in the corpus

Generative Language Modeling for Automated Theorem Proving (2020, background): “2 Ring Algebra Our ring equalities generator is largely inspired by the INT inequality generator [45] .”
Autoformalization with Large Language Models (2022, background): “[50] have shown that training on synthetic formulas can be successful for temporal logics and inequalities.”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “To address the scarcity of formal proofs, previous studies have proposed to use synthetic data (Wu et al., 2021), self-supervision (Polu & Sutskever, 2020; Han et al., 2022), or reinforcement learning (Bansal et al., 2019a; Polu et al., 2022) to synthesize additional formal training data.”
Teaching Temporal Logics to Neural Networks (2020, background): “, 2018), interactive theorem provers (Kaliszyk et al., 2017; Bansal et al., 2019; Huang et al., 2018; Yang & Deng, 2019; Polu & Sutskever, 2020; Wu et al., 2020; Li et al., 2020; Lee et al., 2020; Urban & Jakubv, 2020; Rabe et al., 2020), symbolic mathematics (Lample & Charton, 2020), and mathematic”
LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning (2021, methodology): “Compared to other ITPs, MetaMath is a low-level proving system: each proof step makes only a small step towards the goal.”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “Recent work (Wu et al., 2021d; Krishna et al., 2021; Ri and Tsuruoka, 2022; Anderson and Farrell, 2022; Wu et al., 2022c) shows that pre-training on data that is fully synthetically generated—synthetic pre-training can actually provide substantial gains.”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, background): “[23] built a simplified formal proof environment INT with an associated synthetic inequality benchmark.”
LILA: A Unified Benchmark for Mathematical Reasoning (2022, background): “A separate line of work in mathematical reasoning includes datasets testing mathematical theorem proving (e.g., Li et al., 2021; Wu et al., 2021; Welleck et al., 2021; Zheng et al., 2021; Han et al., 2021).”