一句话：为证明合成模型的标识符引入类别词汇索引、子词序列建模与路径细化三种编码，自动证明的定理数最多提升 29%–45%。
形式化验证虽能有效提升系统质量，但人工证明成本高昂，基于证明语料库学习的自动证明合成工具因此受到关注。现有工作多聚焦于模型架构，而忽视了证明数据本身的丰富性。本文系统探索如何利用证明数据中的一个关键方面——标识符，提出 Passport 方法，为现有证明合成工具所用的 Coq 预测模型引入三种标识符编码机制：类别词汇索引、子词序列建模和路径细化。作者在 ASTactic、Tac 和 Tok 三个基线上评估该增强效果。直接对比中，Passport 增强后表现最好的工具自动证明的定理数比原最好基线多 29%；将三个增强工具组合后，证明数比组合三个基线多 38%；基线与增强版本全部合并后，证明数比仅组合基线多 45%。结果表明，对标识符建模可显著改进证明合成，从而助力更高质量的软件。
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 article 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{paperbot2129,
title = {Passport: Improving Automated Formal Verification Using Identifiers},
author = {Alex Sanchez-Stern and Emily First and Timothy Zhou and Zhanna Kaufman and Yuriy Brun and Talia Ringer},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {2},
year = {2023},
doi = {10.1145/3593374}
}