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 | Size | Format | |
---|---|---|---|---|
Wang_princeton_0181D_14754.pdf | 2.13 MB | Adobe PDF | View/Download |
Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.