TacTok: semantics-aware proof synthesis
TacTok: semantics-aware proof synthesis
复制标题
DOI：
10.1145/3428299
复制
发表时间：
2020-11
影响因子：
--
通讯作者：
Yuriy Brun
中科院分区：
文献类型：
--
作者：
Yuriy Brun
形式化地验证软件正确性是一个高度手动的过程。然而，由于验证证明脚本通常共享结构，因此可以从现有证明脚本中学习以完全自动化一些正式验证。本文的目标是改进证明脚本的合成，使更多的验证能够完全自动化。交互式定理证明器，如CoQ证明助手，允许程序员编写部分证明脚本，观察到目前证明状态的语义，然后尝试更多进展。了解证明状态语义是很有帮助的。最近的研究表明，证明状态有助于预测下一步。在本文中，我们提出了TacTok，这是第一个试图通过使用到目前为止编写的部分证明脚本和证明状态的语义来建模证明脚本来完全自动化证明脚本合成的技术。因此，TacTok更完整地模拟了程序员在手动编写校样脚本时可以访问的信息。我们在Coq中26个软件项目的基准上对TacTok进行了评估，其中包含超过1万个定理。我们将我们的方法与五种工具进行了比较。之前的两项技术，CoqHammer，最先进的证明合成技术，以及ASTtic，一种模拟证明状态的证明脚本合成技术。和我们自己创建的三种新的证明脚本合成技术，SeqOnly，它只对部分证明脚本和被证明的初始定理进行建模，以及WeightedRandom和WeightedGreedy，它使用元启发式搜索，根据现有的成功证明脚本中的证明策略的频率而偏向。我们发现TacTok的性能优于WeightedRandom和WeightedGreedy，并且是对CoqHammer和ASTtic的补充：在26个项目中的24个项目中，TacTok可以为一些以前的工具不能合成的定理合成证明脚本。与单独使用CoqHammer相比，使用TacTok可以自动证明11.5%的定理，比单独使用ASTatic可以多证明20.0%的定理。与CoqHammer和ASTtic的组合相比，TacTok可以多证明3.6%的定理，证明了115个以前没有工具可以证明的定理。总之，我们的实验表明，部分证明脚本和证明状态语义共同为证明脚本建模提供了有用的信息，元启发式搜索是证明脚本合成的一个很有前途的方向。TacTok是开源的，我们公开了我们所有的数据和我们实验的复制包。
Formally verifying software correctness is a highly manual process. However, because verification proof scripts often share structure, it is possible to learn from existing proof scripts to fully automate some formal verification. The goal of this paper is to improve proof script synthesis and enable fully automating more verification. Interactive theorem provers, such as the Coq proof assistant, allow programmers to write partial proof scripts, observe the semantics of the proof state thus far, and then attempt more progress. Knowing the proof state semantics is a significant aid. Recent research has shown that the proof state can help predict the next step. In this paper, we present TacTok, the first technique that attempts to fully automate proof script synthesis by modeling proof scripts using both the partial proof script written thus far and the semantics of the proof state. Thus, TacTok more completely models the information the programmer has access to when writing proof scripts manually. We evaluate TacTok on a benchmark of 26 software projects in Coq, consisting of over 10 thousand theorems. We compare our approach to five tools. Two prior techniques, CoqHammer, the state-of-the-art proof synthesis technique, and ASTactic, a proof script synthesis technique that models proof state. And three new proof script synthesis technique we create ourselves, SeqOnly, which models only the partial proof script and the initial theorem being proven, and WeightedRandom and WeightedGreedy, which use metaheuristic search biased by frequencies of proof tactics in existing, successful proof scripts. We find that TacTok outperforms WeightedRandom and WeightedGreedy, and is complementary to CoqHammer and ASTactic: for 24 out of the 26 projects, TacTok can synthesize proof scripts for some theorems the prior tools cannot. Together with TacTok, 11.5% more theorems can be proven automatically than by CoqHammer alone, and 20.0% than by ASTactic alone. Compared to a combination of CoqHammer and ASTactic, TacTok can prove an additional 3.6% more theorems, proving 115 theorems no tool could previously prove. Overall, our experiments provide evidence that partial proof script and proof state semantics, together, provide useful information for proof script modeling, and that metaheuristic search is a promising direction for proof script synthesis. TacTok is open-source and we make public all our data and a replication package of our experiments.