Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp014j03d298b
Title: Deep Learning for Automated Theorem Proving
Authors: Wang, Mingzhe
Advisors: Deng, Jia
Contributors: Computer Science Department
Keywords: Artificial intelligence
Automated theorem proving
Deep learning
Formal methods
Heuristics-based search
Subjects: Artificial intelligence
Issue Date: 2023
Publisher: Princeton, NJ : Princeton University
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.
URI: http://arks.princeton.edu/ark:/88435/dsp014j03d298b
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
Wang_princeton_0181D_14754.pdf2.13 MBAdobe PDFView/Download


Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.