Link to the University of Pittsburgh Homepage
Link to the University Library System Homepage Link to the Contact Us Form

Contributions to Neural Theorem Proving

Han, Jesse Michael (2023) Contributions to Neural Theorem Proving. Doctoral Dissertation, University of Pittsburgh. (Unpublished)

Primary Text

Download (1MB) | Preview


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.


Social Networking:
Share |


Item Type: University of Pittsburgh ETD
Status: Unpublished
CreatorsEmailPitt UsernameORCID
Han, Jesse Michaeljessemichaelhan@gmail.comjmh288
ETD Committee:
TitleMemberEmail AddressPitt UsernameORCID
Committee ChairHales,
Committee MemberAvigad,
Committee MemberKaveh,
Committee MemberIon,
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


Monthly Views for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item