Passport: Improving Automated Formal Verification Using Identifiers

Tools that learn from proof corpora to suggest partial or complete proof scripts have just begun to show their promise. The powerful logical systems beneath proof assistants, together with the stylistic conventions followed by communities of proof developers, bring richness to the data in these corpora. But this richness remains little exploited, with most work thus far focusing on architecture rather than on how to make the most of the proof data. We develop Passport, a fully-automated proof-synthesis tool that encodes one additional aspect of that rich proof data: identifiers. In particular, Passport enriches a proof-synthesis model for Coq with information about local variables, global definitions, and inductive constructor names, encoding each of these identifier categories in three different ways. We compare Passport to three existing proof-synthesis tools which share similar architecture, ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29% more theorems than the best-performing of these prior tools. Combining the three prior tools enhanced with Passport's identifier information automatically proves 38% more theorems than without that information. Finally, together, these prior tools and Passport models enhanced with identifier information prove 45% more theorems than the prior tools alone. In the course of building Passport, we encountered and overcame significant challenges unique to building machine-learning-based proof synthesis tools. We discuss these challenges and suggest potential solutions to support other researchers building such tools. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software.