GamePad: A Learning Environment for Theorem Proving
arXiv:1806.00608
Abstract
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.
References in corpus (8)
- Regularizing and Optimizing LSTM Language Models
- Learning a SAT Solver from Single-Bit Supervision
- End-to-End Differentiable Proving
- Deep Learning with Dynamic Computation Graphs
- Machine Learning in Proof General: Interfacing Interfaces
- HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- PaMpeR: Proof Method Recommendation System for Isabelle/HOL
Cited by in corpus (25)
- On the Opportunities and Risks of Foundation Models
- Measuring Mathematical Problem Solving With the MATH Dataset
- Learning to Perform Local Rewriting for Combinatorial Optimization
- QED at Large: A Survey of Engineering of Formally Verified Software
- Generative Language Modeling for Automated Theorem Proving
- Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
- Tactic Learning and Proving for the Coq Proof Assistant
- Learning to Reason in Large Theories without Imitation
- NaturalProofs: Mathematical Theorem Proving in Natural Language
- A Formal Proof of PAC Learnability for Decision Stumps
- Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
- LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
- INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
- Learning Heuristics for Quantified Boolean Formulas through Deep Reinforcement Learning
- TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
- Guiding High-Performance SAT Solvers with Unsat-Core Predictions
- Gym-saturation: an OpenAI Gym environment for saturation provers
- Teaching Temporal Logics to Neural Networks
- Learning dynamic polynomial proofs
- On Learning to Prove
- BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
- Program synthesis performance constrained by non-linear spatial relations in Synthetic Visual Reasoning Test
- HolPy: Interactive Theorem Proving in Python
- Generating Symbolic Reasoning Problems with Transformer GANs