Deep Learning for Automated Theorem Proving

Abstract

Automated theorem proving is a fundamental AI task with broad applications to the formalization of mathematics, software and hardware verification, and program synthesis. Deep learning has emerged as a promising approach for guiding theorem provers. In this dissertation, we present our work on developing deep learning approaches for automated theorem proving. First, we propose FormulaNet, a deep learning-based approach to the problem of premise selection. FormulaNet represents a logical formula as a graph that is invariant to variable renaming and then embeds the graph into a vector via a novel graph embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%. Next, we propose MetaGen, a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. On real-world tasks, we demonstrate that synthetic data from our approach improves the theorem prover and advances the state of the art of automated theorem proving in Metamath. Finally, we extend our theorem generator to the interactive theorem prover Lean. We propose TermGen, a neural generator that automatically synthesizes theorems and proofs in Lean by directly constructing proof terms. We also propose a method of expert iteration for training TermGen to synthesize short theorems. At last, we present a case study of generating formal specifications of while-loop programs through a rule-based theorem generator.