GamePad: A learning environment for theorem proving
Captured source
source ↗GamePad: A learning environment for theorem proving | OpenAI
June 2, 2018
Publication
GamePad: A learning environment for theorem proving
Read paper
Loading…
Share
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.
- Exploration & Games
Authors
Daniel Huang, Prafulla Dhariwal, Dawn Song, Ilya Sutskever
Related articles
View all
Embedding AI into developer softwareB2B StoryMar 21, 2024
Building a data-driven, efficient culture with AIB2B StoryMar 18, 2024
Reimagining the email experience with AIB2B StoryMar 18, 2024