Learning to Prove Theorems via Interacting with Proof Assistants

TL;DR

This paper introduces a machine learning approach that interacts with proof assistants to automate theorem proving, using a large dataset and a deep learning model to generate tactics as programs, enabling the proof of new theorems.

Contribution

The paper presents CoqGym, a large dataset for training proof automation models, and ASTactic, a deep learning model that generates tactics as abstract syntax trees for theorem proving.

Findings

ASTactic effectively generates tactics for proof automation.

Models trained on CoqGym can prove theorems previously unprovable by automated methods.

The approach advances automated theorem proving with machine learning.

Abstract

Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts have to construct proofs manually by entering tactics into the proof assistant. In this paper, we study the problem of using machine learning to automate the interaction with proof assistants. We construct CoqGym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. We develop ASTactic, a deep learning-based model that generates tactics as programs in the form of abstract syntax trees (ASTs). Experiments show that ASTactic trained on CoqGym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. Code is available at https://github.com/princeton-vl/CoqGym.