## TacTok: semantics-aware proof synthesis

Emily First, Yuriy Brun, and Arjun Guha

*ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA)*, 2020

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.

PDF