Learning to Prove Theorems via Interacting with Proof Assistants

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.

arXiv commentAccepted to ICML 2019

Cited by in corpus (16)

• MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
• Tactic Learning and Proving for the Coq Proof Assistant
• The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
• NaturalProofs: Mathematical Theorem Proving in Natural Language
• Mathematical Reasoning via Self-supervised Skip-tree Training
• Learning Symbolic Rules for Reasoning in Quasi-Natural Language
• INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
• Learning to Prove from Synthetic Theorems
• LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
• Learning to Prove Theorems by Learning to Generate Theorems
• TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
• From Shallow to Deep Interactions Between Knowledge Representation, Reasoning and Machine Learning (Kay R. Amel group)
• Training a First-Order Theorem Prover from Synthetic Data
• BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
• Faster Smarter Induction in Isabelle/HOL
• Graph Contrastive Pre-training for Effective Theorem Reasoning