护照: 使用标识符提高自动化形式验证
摘要：使用机器自动学习的方式来自动化形式验证，可以有效提高系统质量，但其高手动操作的要求使其变得难以承担。通过学习证明语料库来自动推荐证明的工具已经开始显示出其潜力。这些工具之所以有效，是因为证明语料库所包含的数据丰富性。这种丰富性来自于证明开发者社区遵循的风格惯例以及证明助手下的逻辑系统。然而，这种丰富性尚未得到充分利用，目前的大部分工作都集中在体系结构上，而非充分利用证明数据。 在本文中，我们开发了一个名为Passport的全自动证明综合工具，该工具系统地探索如何最有效地利用证明数据中的一个方面：标识符。Passport通过三种新的标识符编码机制（类别词汇索引、子串序列建模和路径扩展）来丰富一个预测性的Coq模型。我们将Passport与三个现有的基础工具进行比较，Passport可以增强这些基础工具，这些工具分别是ASTactic、Tac和Tok。在面对面的比较中，Passport能够自动证明比这些基础工具中表现最好的工具多29％的定理。将这三个经过Passport增强的工具结合在一起，能够自动证明比这三个基础工具加起来多38％的定理，而没有Passport的增强功能。最后，这些基础工具和经过Passport增强的工具共同证明的定理比没有Passport增强的基础工具多45％。总体而言，我们的研究结果表明，对标识符进行建模可以在提高证明综合的过程中起到重要作用，从而实现更高质量的软件。
作者：Alex Sanchez-Stern and Emily First and Timothy Zhou and Zhanna Kaufman and Yuriy Brun and Talia Ringer
论文ID：2204.10370
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-10