TacTok: Semantics-Aware Proof Synthesis
by Emily First, Yuriy Brun, Arjun Guha
Abstract:
Formally verifying software correctness is a highly manual process. However, because verification proofs often share structure, it is possible to learn from existing proofs to fully automate some formal verification. The goal of this paper is to improve proof synthesis and enable fully automating more verification. Interactive theorem provers, such as the Coq proof assistant, allow programmers to write partial proofs, 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 synthesis by modeling proofs using both the partial proof written thus far and the semantics of the proof state. Thus, TacTok more completely models the information the programmer has access to when writing proofs manually. TacTok is open-source. We evaluate TacTok on a benchmark of 26 software projects in Coq, consisting of over 10 thousand theorems. We compare our approach to two tools, CoqHammer, the state-of-the-art proof synthesis technique, and ASTactic, a proof synthesis technique that models proof state. We find that TacTok is complementary to CoqHammer and ASTactic: for 24 out of the 26 projects, TacTok can synthesize proofs for some theorems 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 and proof state semantics, together, provide useful information for proof modeling.
Citation:
Emily First, Yuriy Brun, and Arjun Guha, TacTok: Semantics-Aware Proof Synthesis, Conditionally accepted to the Proceedings of the ACM on Programming Languages (PACMPL) Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) issue, November 2020.
Bibtex:
@article{First20oopsla,
  author = {Emily First and Yuriy Brun and Arjun Guha},
  title =
  {\href{http://people.cs.umass.edu/brun/pubs/pubs/First20oopsla.pdf}{{TacTok}: {Semantics}-Aware Proof Synthesis}},
  journal = {Conditionally accepted to the Proceedings of the ACM on
  Programming Languages (PACMPL) Object-Oriented Programming, Systems,
  Languages, and Applications (OOPSLA) issue},
  venue = {OOPSLA},
  address = {Chicago, IL, USA},
  month = {November},
  date = {15--20},
  year = {2020},

  accept = {$\frac{109}{302} \approx 36\%$},

  abstract = {Formally verifying software correctness is a highly manual process. However,
  because verification proofs often share structure, it is possible to learn
  from existing proofs to fully automate some formal verification. The goal of
  this paper is to improve proof synthesis and enable fully automating more
  verification. Interactive theorem provers, such as the Coq proof assistant,
  allow programmers to write partial proofs, 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 synthesis by modeling
  proofs using both the partial proof written thus far and the semantics of the
  proof state. Thus, TacTok more completely models the information the
  programmer has access to when writing proofs manually. TacTok is
  open-source. We evaluate TacTok on a benchmark of 26 software projects in
  Coq, consisting of over 10 thousand theorems. We compare our approach to two
  tools, CoqHammer, the state-of-the-art proof synthesis technique, and
  ASTactic, a proof synthesis technique that models proof state. We find that
  TacTok is complementary to CoqHammer and ASTactic: for 24 out of the 26
  projects, TacTok can synthesize proofs for some theorems 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 and proof
  state semantics, together, provide useful information for proof modeling.},
}