GamePad: A Learning Environment for Theorem Proving

TL;DR

GamePad is a novel learning environment designed for theorem proving in Coq, enabling the training of machine learning models on proof synthesis, step prediction, and tactic prediction tasks, with applications to algebraic and complex theorems.

Contribution

Introduces GamePad, a system for applying machine learning to interactive theorem proving, facilitating proof synthesis and prediction tasks in Coq.

Findings

Successfully synthesized proofs for algebraic rewrite problems

Trained baseline models for the Feit-Thompson theorem formalization

Addressed position and tactic prediction tasks in theorem proving

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.