Han, Jesse Michael
(2023)
Contributions to Neural Theorem Proving.
Doctoral Dissertation, University of Pittsburgh.
(Unpublished)
Abstract
In this dissertation we present several contributions to the nascent field of neural theorem proving, deep learning-driven automated theorem proving over large libraries of formalized mathematics. We work primarily with the Lean theorem prover along with its standard mathematical library, mathlib. We focus on addressing the issue of data scarcity for training autoregressive language models to perform high-level reasoning steps at the same level of abstraction as humans. Labeled data for imitation learning of human proof steps is extremely scarce as formal mathematics libraries require years of concentrated effort by human specialists to be built. We show that this paucity of data can be addressed by (1) extracting data from mathlib's low-level proof artifacts, (2) synthesizing those low-level proof artifacts from a language model, and (3) creating new training data from autonomous proof attempts in an expert iteration loop. We demonstrate an application of these kinds of techniques to achieve state-of-the-art performance on solving formalized Olympiad-level mathematics problems.
Share
| Citation/Export: |
|
| Social Networking: |
|
Details
| Item Type: |
University of Pittsburgh ETD
|
| Status: |
Unpublished |
| Creators/Authors: |
|
| ETD Committee: |
|
| Date: |
11 May 2023 |
| Date Type: |
Publication |
| Defense Date: |
8 December 2022 |
| Approval Date: |
11 May 2023 |
| Submission Date: |
9 December 2022 |
| Access Restriction: |
No restriction; Release the ETD for access worldwide immediately. |
| Number of Pages: |
128 |
| Institution: |
University of Pittsburgh |
| Schools and Programs: |
Dietrich School of Arts and Sciences > Mathematics |
| Degree: |
PhD - Doctor of Philosophy |
| Thesis Type: |
Doctoral Dissertation |
| Refereed: |
Yes |
| Uncontrolled Keywords: |
neural theorem proving, formal math, machine learning, theorem proving, automated reasoning, Lean, mechanized math |
| Date Deposited: |
11 May 2023 14:36 |
| Last Modified: |
11 May 2023 14:36 |
| URI: |
http://d-scholarship.pitt.edu/id/eprint/43969 |
Metrics
Monthly Views for the past 3 years
Plum Analytics
Actions (login required)
 |
View Item |
![[feed]](/images/feed-icon-32x32.png){kind=icon}