GamePad: A Learning Environment for Theorem Proving

By Daniel Huang, Prafulla Dhariwal, Dawn Song, Ilya Sutskever. 2018

127 citations recorded by the source corpus.

In this paper, we introduce a system called GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Interactive theorem provers such as Coq enable users to construct machine-checkable proofs in a step-by-step manner. Hence, they provide an opportunity to explore theorem proving with human supervision. We use GamePad to synthesize proofs for a simple algebraic rewrite problem and train baseline models for a formalization of the Feit-Thompson theorem. We address position evaluation (i.e., predict the number of proof steps left) and tactic prediction (i.e., predict the next proof step) tasks, which arise naturally in tactic-based theorem proving.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Reinforcement Learning, Program Analysis & Verification

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 Computational Theory and Mathematics

In Reinforcement Learning

In Program Analysis & Verification

Citations in the corpus

Measuring Mathematical Problem Solving With the MATH Dataset (2021, methodology): “Huang et al. (2019) use the Coq theorem proving environment to create a machine learning benchmark with 1 , 602 theorems and lemmas.”
Generative Language Modeling for Automated Theorem Proving (2020, methodology): “GamePad [33] and CoqGymn/ASTactic [34] introduce environments based on the Coq theorem prover.”
Formal Mathematics Statement Curriculum Learning (2022, background): “…and lem-mas but very few exercises), we hypothesized that if the difﬁculty of this set of statements was made varied enough, expert iteration could potentially leverage it to effectively shift our models’ distribution closer to miniF2F ’s, and in turn, improve their eventual performance on it.”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, methodology): “Datasets for Theorem Proving Some of the prior works on interaction with proof assistants come with datasets containing the formalization of mathematical theorems, including the Feit-Thompson theorem [11] and the Kepler Conjecture [1].”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “GamePad has very similar objectives to ours [10].”
Mathematical Reasoning via Self-supervised Skip-tree Training (2020, methodology): “There are other datasets which might be suitable for our approach as well, including proofs extracted from HOL4 [Gauthier et al., 2017], and from Coq [Huang et al., 2019, Yang and Deng, 2019, Sanchez-Stern et al., 2019].”
Teaching Temporal Logics to Neural Networks (2020, background): “, 2018; Selsam & Bjørner, 2019) or predicting individual proof steps (Loos et al., 2017; Gauthier et al., 2018; Bansal et al., 2019; Huang et al., 2018).”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “Other search-based techniques include Tactician [5], Proverbot9001 [74], and GamePad [30] for Coq; TacticToe [22] for HOL4; and DeepHOL [4, 61] for HOL Light.”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, unknown): “6K in GamePad [22]).”
Language Modeling for Formal Mathematics (2020, methodology): “There are other datasets which might be suitable for our approach as well, including proofs extracted from HOL4 [Gauthier et al., 2017], and from Coq [Huang et al., 2019, Yang and Deng, 2019, Sanchez-Stern et al., 2019].”
Learning dynamic polynomial proofs (2019, unknown): “Recent works have also studied machine learning strategies for automated theorem proving [BLR + 19, HDSS18, KUMO18, GKU + 18].”
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.”
IsarStep: a Benchmark for High-level Mathematical Reasoning (2021, methodology): “In the benchmarks for tactic synthesis (Huang et al., 2019; Bansal et al., 2019; Yang & Deng, 2019; Sanchez-Stern et al., 2019; Paliwal et al., 2019; Gauthier et al., 2017), an agent is asked to propose a sequence of tactics to solve the current goal.”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, background): “Existing tools and datasets can be divided by proof assistants: Coq has GamePad [51], CoqGym [9], and PRISM [52]; Isabelle has IsarStep [53] and PISA [15]; HOL Light has HOList [54] and HoLStep [55], and Lean has LeanStep [16] and lean-gym [19].”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, background): “While there exist environments and datasets for other formal mathematics libraries (Kaliszyk et al., 2017; Li et al., 2021; Huang et al., 2019; Kaliszyk & Urban, 2015a), L EAN S TEP is the ﬁrst and only tactic proof dataset for the Lean theorem prover.”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “Prior work has limited ﬂexibility because they generate tactics by copying from a ﬁxed, predetermined set (Gransden et al., 2015; Gauthier et al., 2018; Huang et al., 2019; Bansal et al., 2019), and are thus unable to generate out-of-vocabulary tactics unseen in the training data.”
Learning to Perform Local Rewriting for Combinatorial Optimization (2018, methodology): “Our approach is tested on multiple domains with extensive ablation studies, and could also be extended to other closely related tasks such as code optimization [41, 12], theorem proving [25, 30, 4, 24], text simplification [14, 37, 18], and classical combinatorial optimization problems beyond routin”