GamePad: A Learning Environment for Theorem Proving
This work addresses theorem proving for users of interactive proof assistants like Coq, but it is incremental as it builds on existing methods in a new domain.
The paper tackles the problem of applying machine learning to theorem proving in Coq by introducing GamePad, a learning environment, and uses it to synthesize proofs for algebraic rewrite problems and train baseline models for the Feit-Thompson theorem, addressing tasks like position evaluation and tactic prediction.
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.