WIXLIB

TacTok: Semantics-Aware Proof Synthesis231:3alone [Hellendoorn et al. 2018] only consider distinct sides of the conversation. In this paper, weshow that by carefully modeling and combining the partial proof script already written and theproof assistant’s feedback, we can automatically prove different theorems than models that onlyuse one source of input.We present TacTok, an open-source implementation of our approach to proof script synthesis Ðavailable at https://github.com/LASER-UMASS/TacTok Ð that incorporates both proof state andthe partial proof script already written. We apply our approach to a benchmark of 122 open-sourcesoftware projects in Coq, with over 68K theorems. We demonstrate that the inclusion of both proofstate and the partial proof script in a proof synthesis model can improve its effectiveness and allowit to synthesize different proof scripts than other tools.We compare our approach to five approaches, two existing tools, CoqHammer and ASTactic, andthree new ones we create, SeqOnly, WeightedRandom, and WeightedGreedy. CoqHammer [Czajkaand Kaliszyk 2018] is a state-of-the-art proof synthesis technique and ASTactic [Yang and Deng 2019]is a proof script synthesis technique that models only proof state. SeqOnly is a proof script synthesistechnique that models only the partial proof script and the initial theorem, and WeightedRandomand WeightedGreedy are proof script synthesis techniques that attempt to construct a proof scriptvia metaheuristic search biased by using the frequency distribution of tactics as they appear in thetraining data.All of the above techniques, except CoqHammer, are metaheuristic search techniques [Harman2007] that search through the proof-script space using a model that biases the search toward thelikely proof script steps. TacTok’s model is built by training on a set of existing, successful proofscripts, and models proof state and the partial proof script already written. ASTactic [Yang andDeng 2019], an existing technique, uses a similar metaheuristic search strategy, but its model onlymodels the proof state. We develop three other novel metaheuristic search techniques for proofsynthesis generation: SeqOnly, whose model accounts for the partial proof state so far and thetarget theorem being proven, and WeightedRandom and WeightedGreedy, whose models accountfor the frequency with which proof script tactics occur in the existing successful proof scripts, withWeightedRandom selecting randomly adhering to the observed distribution, and WeightedGreedyalways selecting the most frequently observed candidates.Evaluated on a benchmark of 26 software projects in Coq with 10,782 theorems, we find that eachof these techniques can successfully generate proof scripts that prove theorems, which is strongevidence for the success of metaheuristic search in proof script synthesis. TacTok can automaticallyprove more theorems than ASTactic (12.9% versus 12.3%). Both techniques outperform SeqOnly,which can only prove 10.0% of the theorems. Even without explicitly modeling the theorem beingproven, WeightedRandom proves 6.2% of the theorems and WeightedGreedy proves 9.7% of thetheorems. Importantly, TacTok is complementary to prior tools. When used together with ASTactic,TacTok can prove 20% more theorems than ASTactic alone. CoqHammer, a very different approach,is able to synthesize proofs for more theorems than TacTok (26.6%), but TacTok and CoqHammertogether can prove 11.5% more theorems than CoqHammer alone.Overall, our experiments show that there is promise to using metaheuristic search and modelingthe partial proof scripts and proof state, together, for synthesizing proof scripts for formal verification. We investigate the effect of using various kinds of information encoded in the partial proofscript on verification efficacy and produce guiding information for improving future proof scriptsynthesis tools.Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 231. Publication date: November 2020.

231:4Emily First, Yuriy Brun, and Arjun GuhaThe main contributions of this work are: A novel automated proof script synthesis technique, TacTok, that, unlike prior work, modelsthe combination of the partial proof script already written and the proof state to automateproof script synthesis and formal verification. TacTok is open-source. Three other new metaheuristic search proof script synthesis techniques, SeqOnly, WeightedRandom, and WeightedGreedy. An application of ASTactic, a state-of-the-art proof script synthesis tool, independentlyreproducing prior evaluation results [Yang and Deng 2019]. An evaluation of the value added by using both the partial proof script and proof state overusing each one alone, and a comparison to two state-of-the-art proof synthesis tools and threenew tools, showing that TacTok proves theorems no prior tool can prove. A public releaseof TacTok Ð https://github.com/LASER-UMASS/TacTok Ð and our experimental scripts anddata [First et al. 2020]. An exploration of the information TacTok models to improve verification efficacy.The rest of this paper is structured as follows. Section 2 illustrates our approach on a simpleexample. Section 3 details our TacTok approach, Section 4 describes the state of the art of formalverification and the three other proof script synthesis approaches we create, and Section 5 evaluatesall these approaches. Finally, Section 6 places our work in the context of related research, andSection 7 summarizes our contributions.2 ILLUSTRATIVE EXAMPLETo illustrate our approach, Section 2.1 introduces a small Coq program for adding two numbersand proves that the function is associative, and Section 2.2 shows how TacTok would generatesuch a proof script automatically. Section 2.3 introduces a more complex theorem expressed inhigher-order logic that TacTok is able to prove, whereas prior tools do not.2.1Using Coq to Prove Addition Is AssociativeWe demonstrate Coq’s use with a small, simple example. We define the natural numbers and thenprove that addition is associative.1 We define the natural numbers (nat) using a unary encoding(Figure 1, lines 1ś3), where Z is the natural number 0, and the rest are defined using the successoroperator (S n).Lines 5ś9 in Figure 1 define a recursive function to add two numbers (add m n). Line 10 definesthe notation m n as a shorthand for add m n. The function itself maps the answer to m if n 0(line 7), and otherwise to S (add p m), where S p n (line 8). In other words, the recursive stepreturns the successor of the sum of m and the number whose successor is n.The assoc Theorem (lines 1ś3) defines the associativity property, n (m p) (n m) p,for all n, m, p.To prove this property, Coq needs help. Coq maintains an internal proof state, which includes thegoals that Coq wants to prove and a list of assumptions. When starting to prove a theorem, Coq’sproof state is a single goal: the theorem itself (shown in Figure 2a). Coq manipulates the proof state(with the help of proof tactics, described next) until the goal is proven and can be removed fromthe proof state. These manipulations are enabled by proof tactics. Some tactics create new subgoals(e.g., induction) and other tactics manipulate the current goal in various ways (e.g., simpl, whichsimplifies complex terms in the goal, and rewrite, which transforms a term in the goal into anequivalent term). The search space of goal manipulation is too large, and a human helps Coq by1 WhileCoq’s standard library already includes these definitions, this basic example is simple enough to effectively demonstrate our approach.Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 231. Publication date: November 2020.

TacTok: Semantics-Aware Proof Synthesis231:5writing a sequence of proof tactics that help Coq manage the exploration. Lines 14ś21 are thehuman-written sequence of tactics, one per line, that help Coq prove associativity.To write down the appropriate sequence of tactics, the programmer needs to understand Coq’sinternal proof state. The interactive proof assistant checks that a partially-complete proof scriptis valid and shows the current proof state to the programmer. This makes it possible for theprogrammer to incrementally develop a proof script, instead of writing a complete proof script in asingle step. The programmer can choose a tactic, examine the output from the proof assistant, choosethe next tactic, and so on. If the programmer chooses an invalid tactic, the proof assistant displaysan error. (For example, the induction tactic signals an error if its argument is not inductivelydefined.) If the programmer chooses tactics that are valid, but do not make progress, they can usethe proof assistant to backtrack to an earlier proof state and try a different approach.We now step through the proof script of associativity and discuss both the proof tactic enteredby the programmer and the proof state displayed by the proof assistant. At the start of the proofscript, the proof state has a single goal, which is the theorem itself (Figure 2a). Since the goal isa statement that should hold forall naturals n, m, and p, the natural next step is to assume theexistence of some arbitrary n, m, and p. The intros tactic eliminates the forall quantifier andintroduces three new variables as assumptions (line 5 in Figure 2b). Since add is inductively defined,it is natural to perform induction on one of these variables (e.g., induction n), which leads to twosubgoals, one for the base case and the other for the inductive case (Figure 2c). Coq first focuses onproving the base case (line 11 in Figure 2c) by labeling it subgoal 1 of 2 (line 10) and only presentingassumptions (line 9) relevant for the base case. Note that in the base case, n is no longer in the listof assumptions, and has been replaced with the value O in the subgoal (line 11 in Figure 2c). Thereflexivity tactic does some basic simplification and solves the base case, since both sides areessentially identical. Therefore, the next proof state has just one goal, which is the inductive case(Figure 2d). In this state, n has been replaced with S n, and the proof assistant shows the inductiveInductive nat : Set : O : nat3 S : nat - nat.124Fixpoint add (n : nat) (m : nat) : nat : match n with7 O - m8 S p - S (add p m)9end10where "n m" : (add n m) : nat scope.5611Theorem assoc : forall n m p : nat,n (m p) (n m) p.14 Proof.15intros.16induction n.17reflexivity.18simpl.19rewrite - IHn.20reflexivity.21 Qed.1213Fig. 1. The definition of the natural numbers (lines 1ś3), the function to add unary natural numbers (lines 5ś10), a theorem that the function is associative (lines 12ś13), and a proof script of that theorem (lines 14ś21).Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 231. Publication date: November 2020.

231:6Emily First, Yuriy Brun, and Arjun Guha1 subgoal(1/1)3 forall n m p : nat, n (m p) n m p12(a) Proof state at the start of the proof script (after line 14 in Figure 1).1 subgoaln, m, p : nat6 (1/1)7 n (m p) n m p45(b) Proof state after line 15 in Figure 1 (intros tactic).2 subgoalsm, p : nat10 (1/2)11 0 (m p) 0 m p12 (2/2)13 S n (m p) S n m p89(c) Proof state after line 16 in Figure 1 (induction n tactic).1 subgoaln, m, p : nat16 IHn : n (m p) n m p17 (1/1)18 S n (m p) S n m p1415(d) Proof state after line 17 in Figure 1 (reflexivity tactic).1 subgoaln, m, p : nat21 IHn : n (m p) n m p22 (1/1)23 S (n (m p)) S (n m p)1920(e) Proof state after line 18 in Figure 1 (simpl tactic).1 subgoaln, m, p : nat26 IHn : n (m p) n m p27 (1/1)28 S (n m p) S (n m p)2425(f) Proof state after line 19 in Figure 1 (rewrite - IHn tactic).Fig. 2. The proof state after the execution of each tactic of the add function’s associativity proof script. Forexample, in (a), at the start of the proof script, there is 1 subgoal, which is the theorem itself, line 3, and in (c),after the induction n tactic, there are 2 subgoals, one for the base case (line 11) and one for the inductivecase (line 13).assumption (IHn). However, IHn is not immediately applicable because it contains n instead of S n,and so trying to use it will produce an error. Instead, the simpl tactic tries to simplify the goal whilekeeping it readable (though many Coq users find that simpl is a complicated tactic that producesunpredictable results [The Coq Development Team 2017]). After choosing simpl, the left-handProc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 231. Publication date: November 2020.

TacTok: Semantics-Aware Proof Synthesis231:7side of the goal has an expression that is identical to the left-hand side of the inductive assumption(Figure 2e). Therefore, the rewrite tactic can replace that expression with the right-hand side ofthe inductive assumption (Figure 2f), which leads to a trivial equality that reflexivity can solve.Finally, the proof assistant prints no more subgoals and Qed completes the proof script.2.2Proving Associativity with TacTokNote that the proof script (lines 15ś20 of Figure 1) is almost unintelligible without examining theinternal proof state, for several reasons:(1) Some tactics generate new variable names (e.g., induction), which subsequent tactics (e.g.,rewrite) use. The programmer needs to know these names to use them in the proof script.(2) Some tactics apply heuristics that are hard to predict. In the example in Figure 1, simpl(line 18) uses heuristics to produce readable output. Without looking at the resulting proofstate in Figure 2e, the programmer would not know what form the goal is transformed intoand whether IHn can be invoked without an error.(3) When a proof script has multiple goals, it may not be obvious where one goal ends andthe next goal begins. In the example in Figure 1, the base case is addressed by the tactic inline 17, while the inductive case is addressed by the tactics in lines 18ś20. However, withoutexamining the proof state Figure 2d, it would not be clear that reflexivity completelysolved the base case.(4) After a few steps of the proof script, the current goal to prove has likely evolved significantlyfrom the original goal (the theorem). In the example in Figure 2, the programmer is tryingto prove the theorem Figure 2a line 3. After three steps in the proof script, the programmermust now prove Figure 2d line 18 using assumptions lines 15ś16. The goal has changedsignificantly and there are now assumptions that didn’t exist at the start. Knowing the newgoal and the assumption IHn are helpful to the programmer at this point in deciding the nexttactic: the programmer sees that the goal needs to be transformed using simpl to apply theassumption. Without being able to see the current proof state in Figure 2d, the programmerwould be proving blindly.Since the programmer needs to examine the proof state to choose the next tactic, it is a goodidea to consider whether models of next tactic prediction might also need and benefit from havingaccess to information in the proof state. However, since proof scripts, like programs, build uponthe commands executed thus far [Hellendoorn et al. 2018; Hindle et al. 2016, 2012], a model of nexttactic prediction may also benefit from having access to the previous tactics in the proof script.TacTok builds a model of next-tactic prediction for Coq. The model is learnt using a corpus ofexisting proof scripts. TacTok decomposes each of the existing proof scripts by stepping throughthem, one tactic at a time, and computing the resulting intermediate proof states. The modelautomatically learns an embedding of the proof states and the partially written proof script andmaps these to an abstract syntax tree (AST) of the next line in the proof script. Thus, the model’sinputs are the partially written proof script and the proof state. For example, one input to the modelis the intermediate proof state in Figure 2d and the partial proof script [intros, induction n,reflexivity] that achieved that proof state. The model’s output is an AST that TacTok decodes tothe next predicted tactic and its arguments.Given a model trained on existing proof scripts (Section 3.2.4 presents the training process),TacTok automatically generates the proof script of associativity (lines 14ś21). To start, TacToktakes as input the proof state in Figure 2a and the partially written proof script, which is only[Proof]. For the sake of illustration, suppose the model correctly predicts intros as the next tactic.TacTok executes this partial proof script using the Coq interactive proof assistant, and checks forProc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 231. Publication date: November 2020.

231:8Emily First, Yuriy Brun, and Arjun Guhatwo things. First, that executing the partial proof script with the new tactic does not return an error.And second, that the new returned proof state is different from the prior observed proof statesin this partial proof script, meaning the tactic had an affect and produced something new. Here,TacTok will see no error and the updated proof state is that in Figure 2b. TacTok will next exploregrowing the proof script further. TacTok’s next input to the model is the proof state in Figure 2band the partial proof script [Proof, intros]. Suppose, again, the model correctly predicts the nexttactic and argument is induction n; there is no error adding this tactic to the partial proof scriptand the new proof state is that in Figure 2c.If TacTok proceeds in this way to produce the partial proof script [Proof, intros, induction n,reflexivity] and the proof state in Figure 2d, but as the next tactic and arguments, TacTok predictsrewrite - IHn. Adding this tactic results in an error. TacTok goes back to the model and asks itfor the next most likely tactic and arguments (TacTok would do the same thing if there were noerror but the proof state was a duplicate of an earlier state). Suppose the model suggests simpl,which turns out to return no error and changes the state.TacTok will proceed in this way, performing a depth-first search through the space of proofscripts until, either, it reaches the proof state łno more subgoalsž (meaning the proof script iscompleted successfully) and adds Qed to the proof script, or it times out and fails to complete theproof script.Of course, TacTok can only be successful if its model is fairly accurate in its predictions.2.3Proving Higher-Order Logic TheoremsThe associativity theorem we just discussed is an example of a theorem expressed in first-orderlogic. Theorems expressed in higher-order logic are likely to be more complex, and so their proofscripts are more difficult to generate. One example of higher-order logic in Coq is the presence of anested forall. Figure 3 defines the function prod n f, which calculates 1 · f (0) · · · · · f (n 1). Thesame figure defines the sameProd theorem, which states an intuitive property: for functions f andд, if f (m) д(m) for all m n, then prod n f prod n д. TacTok is able to generate a proof scriptfor sameProd. CoqHammer [Czajka and Kaliszyk 2018] fails to find a proof in ten minutes, andASTactic [Yang and Deng 2019] cannot find a proof script either. Section 5.5 will further discusstheorems that TacTok proves that prior tools cannot.We next describe prior work on training language models and our improvements over the stateof the art.Definition prod : forall (n : nat) (f : nat - nat), nat.intros.3 induction n as [ n Hrecn].4 exact 1.5 exact (f n * Hrecn).6 Defined.127Lemma sameProd : forall (n : nat) (f g : nat - nat),(forall m : nat, m n - f m g m) - 10prod n f prod n g.89Fig. 3. Lines 1ś6 defines the function prod n f , which calculates 1 · f (0) · · · · · f (n 1). Lines 8ś10 define thesameProd theorem, which states that if f (m) д(m) for all m n, then prod n f prod n д.Proc. ACM Program. Lang., Vol. 4, No. OOPSLA, Article 231. Publication date: November 2020.

TacTok: Semantics-Aware Proof Synthesis231:93 THE TacTok APPROACHSection 3.1 describes language modeling methods and Section 3.2 details how TacTok builds onlanguage modeling approaches to generate proof scripts. Our TacTok implementation is publiclyavailable at https://github.com/LASER-UMASS/TacTok/.3.1 Language ModelingLanguage models estimate the probability of a particular instance in a language. For example,a language model can estimate the likelihood that the words łI went to thež are followed byłstorež. When applied to natural languages, these models have aided speech recognition, machinetranslation, spelling correction, and other natural language processing tasks [Brill and Moore 2000;Koehn et al. 2007; Stolcke 2002].While language models can be created in many ways, including manually, a typical approach isto train a language model on a large corpus of example sentences in a language. There are two mainclasses of language models widely used in modern natural language processing research. The firstconsists of statistical language models, often called n-gram language models. These count-basedmodels work on the Markov assumption that the conditional probability of a word is dependent o

proof state semantics is a signiicant aid. Recent research has shown that the proof state can help predict the next step. In this paper, we present TacTok, the irst 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.