Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification by learning from proof corpora to synthesize proofs have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain. This richness comes from the stylistic conventions followed by communities of proof developers, together with the powerful logical systems beneath proof assistants. However, this richness remains underexploited, with most work thus far focusing on architecture rather than on how to make the most of the proof data. This paper systematically explores how to most effectively exploit one aspect of that proof data: identifiers.
We develop the Passport approach, a method for enriching the predictive Coq model used by an existing proof-synthesis tool with three new encoding mechanisms for identifiers: category vocabulary indexing, subword sequence modeling, and path elaboration. We evaluate our approach's enrichment effect on three existing base tools: ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29% more theorems than the best-performing of these base tools. Combining the three tools enhanced by the Passport approach automatically proves 38% more theorems than combining the three base tools. Finally, together, these base tools and their enhanced versions prove 45% more theorems than the combined base tools. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software.
@article{Sanchez-Stern23toplas,
author = {Alex Sanchez-Stern and Emily First and Timothy Zhou and Zhanna Kaufman and Yuriy Brun and Talia Ringer},
title = {\href{http://people.cs.umass.edu/brun/pubs/pubs/Sanchez-Stern23toplas.pdf}{Passport: {Improving} Automated Formal Verification Using Identifiers}},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
venue = {TOPLAS},
year = {2023},
doi = {10.1145/3593374},
issn = {0164-0925},
volume = {45},
number = {2},
month = {June},
articleno = {12},
pages = {12:1-12:30},
note = {\href{https://doi.org/10.1145/3593374}{DOI: 10.1145/3593374},
arXiv: \href{https://arxiv.org/abs/2204.10370}{abs/2204.10370}.
Presented as journal-first paper at PLDI 2023},
abstract = {<p>Formally verifying system properties is one of the most effective ways of
improving system quality, but its high manual effort requirements often
render it prohibitively expensive. Tools that automate formal verification by
learning from proof corpora to synthesize proofs have just begun to show
their promise. These tools are effective because of the richness of the data
the proof corpora contain. This richness comes from the stylistic conventions
followed by communities of proof developers, together with the powerful
logical systems beneath proof assistants. However, this richness remains
underexploited, with most work thus far focusing on architecture rather than
on how to make the most of the proof data. This paper systematically explores
how to most effectively exploit one aspect of that proof data: identifiers.</p>
<p>We develop the Passport approach, a method for enriching the predictive Coq
model used by an existing proof-synthesis tool with three new encoding
mechanisms for identifiers: category vocabulary indexing, subword sequence
modeling, and path elaboration. We evaluate our approach's enrichment effect
on three existing base tools: ASTactic, Tac, and Tok. In head-to-head
comparisons, Passport automatically proves 29% more theorems than the
best-performing of these base tools. Combining the three tools enhanced by
the Passport approach automatically proves 38% more theorems than combining
the three base tools. Finally, together, these base tools and their enhanced
versions prove 45% more theorems than the combined base tools. Overall, our
findings suggest that modeling identifiers can play a significant role in
improving proof synthesis, leading to higher-quality software.</p>},
fundedBy = {DARPA HR0011-22-9-0063, NSF CCF-2210243},
}