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. Theorem proving is a challenging AI task that involves symbolic reasoning (e.g., SMT solvers BID2 ) and intuition guided search. Recent work BID7 Loos et al., 2017; has shown the promise of applying deep learning techniques in this domain, primarily on tasks useful for automated theorem provers (e.g., premise selection) which operate with little to no human supervision. In this work, we aim to move closer to learning on proofs constructed with human supervision.We look at theorem proving in the realm of formal proofs. A formal proof is systematically derived in a formal system, which makes it possible to algorithmically (i.e., with a computer) check these proofs for correctness. Thus, formal proofs provide perfect learning signal-theorem statements and proofs are unambiguous. Human mathematicians usually do not write proofs in this style, and instead, construct and communicate proofs in natural language. Although the form and level of detail involved in each kind of proof differ, the logical content is similar in both contexts.Our work focuses on interactive theorem provers (ITPs), which are software tools that enable human users to construct formal proofs. ITPs have at least two features that make them compelling environments for exploring the application of learning techniques to theorem proving. First and foremost, ITPs provide full-fledged programmable environments. Consequently, any machine learning infrastructure built for an ITP can be reused across any problem domain crafted to study an aspect of learning and theorem proving. Second, the proofs are constructed by humans, and thus, have the constraint that they must be relatively human-understandable. Hence, ITPs provide access to large amounts of supervised data (i.e., expert-constructed proofs of theorems that are mathematically interesting). For example, ITPs have been used to build and check the proofs of large mathematical theorems such as the Feit-Thompson theorem BID6 and provide provable guarantees on complex pieces of software such as the CompCert C compiler BID13 .We introduce a system called GamePad 1 that exposes parts of the Coq ITP to enable machine learning tasks and explore a few use cases. We focus on the Coq proof assistant for two reasons. First , Figure 1 : A proof script in Coq (left) and the resulting proof states, proof steps, and the complete proof tree (right). A proof state consists of a context (pink rectangles) and a goal (white rectangles). The initial proof state has as its goal the statement we are trying to prove and an empty context. The arrows indicate what tactic the prover used. The final states of the proof are indicated by the red circles and can be transitioned to only when the goal in the previous state is trivially true.Coq is a mature system with an active developer community that has been used to formalize nontrivial theorems, including Feit-Thompson and CompCert. Second, Coq supports the extraction of verified software. Consequently , one can prove that a program is correct and then run the verified program. The ease of extraction makes Coq a popular choice for program verification.Our contributions are the following. First, we introduce GamePad, which provides a structured Python representation of Coq proofs (Section 3), including all the proof states encountered in a proof, the steps taken, and expression abstract syntax trees (ASTs). The tool also enables lightweight interaction with Coq so that it can be used to dynamically build proofs (e.g., used as an environment for reinforcement learning). Tasks that can leverage this structured representation (Section 4) include position evaluation (i.e., predict the number of proof steps left) and tactic prediction (i.e., predict the next proof step to take). We also discuss how we can use the structured representation to embed proof states into R D (Section 5) . Second, we demonstrate the synthesis of Coq proof scripts that makes use of a tactic prediction model for a hand-crafted algebraic rewriting problem (Section 6). Third and finally, we apply baseline models for position evaluation and tactic prediction to the FeitThompson formalization using data extracted by GamePad (Section 7).The code for GamePad, as well as the associated data sets, models and results, are open source on GitHub at https://github.com/ml4tp/gamepad. In this work, we look at theorem proving problem through the lens of a system that enables learning with proofs constructed with human supervision. We highlight three key aspects of the problem at this level. The first concerns obtaining inputs to a learning algorithm that approximate the level of abstraction faced by a human prover. For this, we use an ITP, as it retains aspects of human supervision. GamePad preserves the structure of the proofs (e.g., annotations regarding implicit arguments) so they can be used for building models. The second involves building models that employ the game-like structure of ITP proofs. Here, we experiment with tactic prediction for toy and real world data sets. Finally, as a consequence of theorem proving at a higher-level (compared to SMT solvers), we will need to be careful to distinguish the syntax from the semantics of terms. Our current approach is to provide structured representations of terms so that more semantic structure can be exploited. While our results are preliminary, our hope is that GamePad provides an accessible starting point to explore the application of machine learning in the context of interactive theorem proving.
We introduce a system called GamePad to explore the application of machine learning methods to theorem proving in the Coq proof assistant. This paper describes a system for applying machine learning to interactive theorem proving, focuses on tasks of tactic prediction and position evaluation, and shows that a neural model outperforms an SVM on both tasks. Proposes that machine learning techniques be used to help build proof in the theorem prover Coq.