Abstract: Formally verified correctness is one of the most desirable properties of software systems. Despite great progress made toward verification via interactive proof assistants, such as Coq, such verification remains one of the most effort-intensive (and often prohibitively difficult) software development activities. Recent work has created tools that automatically synthesize proofs either through reasoning using precomputed facts or using machine learning to model proofs and then perform biased search through the proof space. However, models in prior tools fail to capture the complete information the programmer has access to when writing proofs, variations in the learning process, the richness of the existing proof corpora, and advances in large language models.
In this dissertation, I develop tools to improve proof synthesis and to enable fully automating more verification. I first present TacTok, a proof-synthesis tool that models proofs using both the partial proof written thus far and the semantics of the proof state. I then present Diva, a
proof-synthesis tool that controls the learning process to produce a diverse set of models and, due to the unique nature of proof synthesis (the existence of the theorem prover, an oracle that infallibly judges a proof's correctness), efficiently combines these models to improve the overall proving power. I then present Passport, a proof-synthesis tool that systematically explores different ways of encoding identifiers in proofs to improve synthesis. Finally, I propose using transformer-based neural models to improve the architecture of proof synthesis modeling to more fully capture the available contextual information. This dissertation contributes new ideas for improving automated proof synthesis, and the work so far empirically demonstrates that the improvement is significant on a dataset of 68K theorems from 122 open-source software projects.
Advisor: Yuriy Brun