GAMEPAD: A LEARNING ENVIRONMENT FOR THEO- REM PROVING
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.
Summary: This paper mixes automated theorem proving with machine learning models. The final goal, of course, is to be able to train a model that works in conjunction with an automated theorem proving system to efficiently prove theorems, and, ideally, in a way that resembles the way humans prove theorems. This is a distant goal, and the authors instead focus on several tractable tasks that are required for future progress in this direction. They start by integrating the Coq theorem proving environment with ML frameworks, allowing for the creation of models that perform various tasks related to theorem proving. In particular, they focus on two tasks. One is to estimate how many steps are left to complete the proof given a current proof state. The other is to determine what is a good choice of next step. Finally, they also consider issues surrounding representations of the various data structures involved in proofs (i.e., the proof tree, variables, etc.). They test various models on a synthetic nearly trivial logical expression proof, along with a more complicated (and meaningful real world) group theory result.
Strengths: This is a very important area. Automated theorem proving has a potentially very significant impact, and being able to take advantage of some of the recent successes in ML would be excellent. The main environment proposed here, integrating PyTorch with Coq could potentially be a very useful platform for future research in this area. The paper exposes many interesting questions, and I generally think we need more exploratory papers that open up an area (as opposed to seeking to finalize existing areas) 
Weaknesses: The paper is pretty tough to understand without a lot of background in all of the existing theorem proving work (which might be fine for a conference in this area, but for this venue it would be nice to be more self-contained). The organization could also use some work, since it's often tough to figure out what the authors actually did. The experimental results seem very preliminary---although it's hard to say, as there is no easy way to compare the results to anything else out there. In general a lot of details seem missing.
Verdict: The authors admit this is a preliminary work, and I agree with that. The paper certainly introduces many more questions than it answers. However, I think that in this case it's a good thing, and this type of paper has the potential to inspire a lot of new and exciting research, so I voted for acceptance.
Comments and questions:
- As mentioned, a lot of the terminology is introduced very quickly and could stand to be more self-contained, i.e., "tactics" could be defined as being simple transformations that are applied to a current proof state to obtain another proof state, and each language has a library of tactics available.
- Probably the major contribution of the work is the integration of the CoQ and Pytorch, so a bit more content describing how the Python data structures that wrap around Coq structures would be interesting here.
- I didn't really understand one of the major contributions: the embedding function for the M_i conditioned on the environment. How does the sampled Gaussian vector work here? In general this section is pretty confusing, it would be great to include a schematic to show how the different levels of embeddings for different structures work here.
- How does the real-world dataset work? Does the dataset contain one automated proof of the entire theorem, or several different proofs (ultimately produced by different user choices)? Are you measuring accuracy on the proofs of individual lemmas?