Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs

1 Introduction

1.1 Program Synthesis

In program synthesis the aim is to generate (synthesize) a program in a defined programming language given the specification of its expected behavior. Most commonly, a specification defines an expected program behavior in terms of the return value of the program for some inputs. There are two types of such specifications:

Formal: The result of a program is constrained by a set of expressions in a certain logic. For example:

While checking if the program passes all test cases is relatively easy - it suffices to run a program for each input and compare outputs - in the case of formal specification a formal proof must be conducted for the generated program encoded in the same logic as the constraints.

1.2 Genetic Programming

Genetic Programming (GP) is a subtype of the evolutionary algorithm (EA) metaheuristic in which the entities to be evolved are programs, most often represented as expression trees. A population of candidate solutions is first initialized with random programs, and then maintained through the subsequent generations (iterations) of the algorithm. A fitness function assigns a score to the candidate programs based on the estimated proximity of their behavior to the expected one. At the beginning of each new generation, a selection function selects programs at random from the population, biased in favour of fitter programs, and recombines them by crossover (exchanging fragments between two programs) or mutation (randomly re-generating part of the program). The old population is discarded, and the selected and modified individuals constitute the new population.

1.3 Motivation

Genetic Programming (GP) proves effective for test-based synthesis of programs. There are numerous settings in which this approach proves useful, most of them involving GP as a machine learning tool within the learning-from-examples paradigm.

The main shortcoming of test-based synthesis is that generalization cannot be guaranteed: a program synthesized from a finite training sample cannot be expected to return the correct value for arbitrary admissible input. In GP, this shortcoming can be partially alleviated via ad-hoc techniques such as parsimony pressure, but (except specific areas like semantic GP) GP lacks a general formal theory of generalization.

Even if GP had such a theory, then as in the case of any other inductive learning approach, it would not guarantee perfect generalization. Assuring correct behavior for all admissible program inputs can be achieved only when synthesizing from formal specifications (spec-based synthesis in the following).

Crucially, a program produced by spec-based synthesis is guaranteed to adhere perfectly to the specification. In many areas, such guarantees are essential. Examples include security, transportation, safety-critical systems, and costly manufacturing. The list of potential application areas for such methods is growing rapidly, particularly given the increasing level of cyberthreats and degree of responsibility delegated to computer systems.

Given the effectiveness of GP on test-based problems and guarantees offered by programs synthesized from specification, it becomes natural to ask: can the evolutionary paradigm be adapted to solve spec-based synthesis problems? Preliminary attempts on specific classes of executable structures [Johnson, 2007] and programs [Katz and Peled, 2016], which we review in Section 4, suggest several possibilities. In this paper, we propose Counterexample-Driven Genetic Programming (CDGP), a novel variant of GP for solving spec-based synthesis problems.

2 Spec-based Synthesis and Verification

Spec-based program synthesis typically proceeds from a contract, given by a pair of logical formulas: a precondition Pre - the constraint imposed on program input, and a postcondition Post - a logical clause that should hold upon program completion. Let p denote a program and p(in) the output produced by p when applied to input in. Solving a synthesis task (Pre, Post) is equivalent to proving that

where Pre(in) is the precondition valuated for the input in, and Post(in, p(in)) is the postcondition valuated for the input in and the output produced by p for in. The proof has to be constructive, i.e. to produce such a p - merely determining whether or not p exists is not much use for synthesis.

Consider synthesizing a program that calculates the maximum of two integers x, y. For this synthesis task, the contract can be defined as follows:

In methods of spec-based synthesis, the content (code) of p is controlled by a set of variables. To determine the values of variables that cause p to be fulfilled (1) (called a model in propositional logic), the synthesis formula parameterized with these variables is passed to a SAT solver. The solver either produces a feasible set of variable assignments, and thus yields a correct-by-construction program that is guaranteed to meet the contract, or otherwise states that the specified program does not exist. In practice, the solver is equipped with an additional abstraction layer, a theory that enables reasoning in terms of, for instance, integer arithmetic. This leads to the concept of Satisfiability Modulo Theories (SMT) used in program synthesis [Jha et al., 2010; Gulwani et al., 2010; Srivastava et al., 2010].

In contrast, GP is a stochastic technique of test-based synthesis. The input to GP is a set of tests (fitness cases), i.e. pairs (in, out) ∈ T of program input in and the desired output out required to result from applying a correct program to in. A GP algorithm solving a synthesis task maintains a population of programs P. In every generation, each program p ∈ P is tested on every test (in, out) ∈ T, in which p is applied to in and returns an output p(in) that is confronted with out. If p produces the correct output for t, it is said to pass t; otherwise, we say that p fails t. The conventional GP fitness that rewards a program for the number of passed tests can be then written as

where [ ] is the Iverson bracket (returns 1 if the proposition is true, 0 otherwise).

In spec-based synthesis, tests are not available, and so neither is the conventional fitness function. To combine such synthesis with evolutionary search, one must resort to other means of program evaluation. The method presented in this paper relies on program verification which consists in proving that, for a given program p,

The practical difference with respect to spec-based synthesis (1) is that verification can be typically realized using conventional SMT solvers at much lower computational cost, because it is applied to an existing program. The result can be twofold: success when p meets (4), or failure otherwise. Crucially, the latter outcome is accompanied by a counterexample, i.e. an input in such that (4) does not hold. This characteristic is essential for our method, because we employ the collected counterexamples to compute the fitness according to, amongst others, equation (3).

3 Counterexample-Driven GP

Figure 1 presents the high-level diagram of CounterexampleDriven GP (CDGP). The top-level loop of CDGP proceeds in a similar manner to conventional GP, where in each generation parent programs are selected, modified, and evaluated. The main difference is that evaluation involves both formal verification and evaluation on a set of tests Tc, collected from

1: procedure CDEVAL(P, Tc, (Pre, Post)) 2: T ← ∅ ▷Working set of tests 3: for all p ∈ P do ▷ Evaluation loop 4: p.eval ← EVAL(p, Tc) 5: if p.eval = |Tc| then 6: c ←VERIFY(p, (Pre, Post)) 7: if c = ∅ then return p ▷ Perfect program 8: else 9: T ← T ∪ {c} 10: end if 11: end if 12: end for 13: return (P, Tc ∪ T ) 14: end procedure

verifications conducted in the previous generations. The evolutionary run starts with an empty Tc. Programs in the working population are evaluated on the tests in Tc in the conventional way, and the resulting fitness drives the search process.

The procedure CDEVAL presented in Algorithm 1 is launched once per generation. As in conventional GP, each program p in the current population is first evaluated on the tests currently available in Tc and assigned the conventional fitness (3). If it happens to pass all of them, it is subject to formal verification. A positive outcome of verification terminates search, with p returned as the resulting correct program. Otherwise, the counterexample resulting from verification extends the working set of tests T, which is maintained separately from Tc so that evaluation of successive programs in P remains unaffected. Once all programs have been processed, Tc is extended with the new tests from T . Since both Tc and T are sets, adding a test that has been already collected earlier in a run has no effect - duplicate tests are automatically discarded.

In the first generation Tc = ∅, so all programs in P receive zero fitness and the attendant selection of parent programs is completely random. Nevertheless, this first generation will typically discover a few counterexamples, which provide for some degree of discrimination of programs in the second generation. In this way, the verification outcomes supply CDGP with an increasingly finer-grained fitness function and more precise search gradient.

Algorithm 1 implements the 'conservative' variant of CDGP, where the time-costly verification is applied only to programs that pass all tests and is thus used sparingly. We also investigate a non-conservative variant, where line 5 in Algorithm 1 is skipped, so that each act of evaluating a program is followed by its verification and will produce a counterexample that may extend Tc (unless already present there).

4 RelatedWork

The application of formal methods to program synthesis precedes heuristically-informed stochastic methods such as GP by several decades [Cohen, 1994], and the literature for formal approaches to synthesis (and verification) is vast (for recent overviews, see Boca et al [Boca et al., 2009] and Almeida et al [Almeida et al., 2011]). However, we are aware of only few approaches which combine formal techniques with heuristic search.

In 2007, Johnson [Johnson, 2007] incorporated modelchecking (as specified via Computation Tree Logic) into the fitness measure of evolved finite state machines, and used this to learn a controller for a simple vending machine. From 2008, Katz and Peled authored a series of papers combining model-checking and GP [Katz and Peled, 2008; Katz and Peled, 2016] in which they progressively refine their MCGP tool based on Linear Temporal Logic. They use 'deep model checking' to impose a gradient on the fitness function, for which they report good fitness-distance correlation. The most recent development of their tool [Katz and Peled, 2016] applies a (µ+λ) evolutionary strategy to strongly-typed, treebased tree GP and gives example applications of program synthesis, program improvement and bug-repair.

The possibility of using coevolutionary GP to synthesize programs from formal specifications was researched by Arcuri and Yao [Arcuri and Yao, 2007]. In their approach, populations of both tests and programs are maintained in the competitive coevolution framework. Fitness of programs is calculated using a heuristic that estimates how close a postcondition is from being satisfied by the program's output for specific tests. The population of test cases is initialized randomly and then co-evolves with programs, guided by fitness function that rewards failing as many programs as possible.

Amongst the dozen or more well-known systems that perform synthesis under the heading of Inductive Logic Programming [Muggleton, 1994], IGOR II [Hofmann, 2010] is known to perform well on a range of problems. As extended by Katayama [Katayama, 2012], it combines an 'analytic' approach based on analysis of fitness cases with the generateand-test approach.

An alternative approach to spec-based synthesis is 'program sketching' [Solar-Lezama et al., 2006], a technique whereby a program contains 'holes' which are automatically filled in (e.g. using an SMT solver) with values satisfying an executable specification. More recently, Evolutionary Program Sketching (EPS) has been proposed [Bł ˛ adek and Krawiec, 2017]. EPS is a GP alternative that evolves partial programs, and then uses an SMT solver to complete them, attempting to maximize the number of passing test cases.

5 Experiment

5.1 Configuration

To assess the effectiveness of CDGP, we apply it to a range of spec-based synthesis benchmarks of varying difficulty, presented in Table 1, all of which belong to the theory of Linear Integer Arithmetic (LIA) [Barrett et al., 2015], where the set of available instructions comprises linear arithmetic, elementary Boolean logic and conditional statements. In all selected benchmarks, the task is to synthesize a certain function with a signature In →I, where n is function arity. Max, Search and Sum come from the repository maintained for the annual

'Syntax Guided Synthesis' competition [Alur et al., 2015]; the remaining benchmarks are of our own design.

In order to provide a frame of reference, we design a baseline setup called GP Random (GPR). GPR proceeds as CDGP, except for line 9 in Algorithm 1, where it adds to T a randomly generated test rather than the counterexample returned by the solver.

In order to appropriately handle the two available types (Int and Boolean), we use a typed variant of GP. The initialization operator (used to populate the initial population) recursively traverses the derivation tree from the starting symbol of the grammar (I) and randomly picks expressions from the right-hand sides of productions. The mutation operator picks a random node in a parent tree, and replaces the subtree rooted in that node with a subtree generated in the same way as for initialization. Crossover draws a random node in the first parent program, and swaps it with a type-compatible subtree selected at random from the second parent program. A program tree resulting from any of these search operators is considered feasible unless its height exceeds 12. Should that happen, the program is discarded and the search operator is queried again.

In both CDGP and GPR, the working set of tests Tc may grow slowly. With only a small number of tests, the fitness function can return just a few values and has little discriminatory power, which may hamper population diversity. To address this issue, in addition to the conservative and nonconservative CDGP and GPR, we consider two independent extensions: Lexicase selection [Helmuth et al., 2015] and steady-state workflow.

Communication with the solver is realized via the SMTLIB standard [Barrett et al., 2015], recognized by most contemporary SMT solvers. We employ the Microsoft Z3 SMT solver [de Moura and Bjørner, 2008], one of the most widelyused non-commercial solvers.

The source code of CDGP, along with specifications of problems, is available at https://github.com/kkrawiec/CDGP.

5.2 Results

The detailed results are presented in [Krawiec et al., 2017]. The key observations are: (i) Compared to GPR's baseline, CDGP offers on average greater likelihood (success rate) of synthesizing a correct program. However, the success rates on individual benchmarks are usually only slightly better for CDGP than for GPR, and on a few occasions GPR is better than the corresponding CDGP variant. (ii) Lexicase selection boosts the performance of all configurations and brings both CDGPLex and GPRLex close to each other. (iii) The conservative variants of CDGP are clearly worse than their non-conservative counterparts, which suggests that 'harvesting' new tests from candidate programs that are known to be incorrect is beneficial. (iv) Steady-state did not bring the anticipated benefits, neither when combined with tournament selection nor with Lexicase selection.

In the above experiment, we ignored the actual computational cost of synthesis. Although individual configurations were given the same limit on the number of evaluations (100,000), their runtimes vary heavily and are typically much higher for CDGP, mainly due to the significant computational overhead of SMT-based formal program verification. To address this issue, we conduct another experiment, where each configuration of CDGP and GPR is given the same time budget equal to the average runtime of successful runs of all configurations from the first experiment. This time, CDGP clearly proves more effective than GPR. The non-conservative variants of CDGP that use Lexicase selection have the lead again, though this time the generational variant is noticeably better.

The experimental outcomes corroborate our main hypothesis: the counterexamples collected from verification in CDGP prove more useful as tests than the inputs constructed at random in GPR. On one hand, this was expected - as opposed to counterexamples, random tests are not derived from the problem specification and are in this sense knowledge-free. On the other hand, this result is nontrivial, because counterexamples constructed by an SMT solver reflect its sophisticated search tactics, which are reportedly built on years of expert experience, and as such involve certain search biases. It is thus not obvious that counterexamples they identify should be effective when used as 'search drivers' [Krawiec, 2015] in a stochastic synthesis process.

6 Conclusion and FutureWork

We have presented CDGP, a method for specification-based program synthesis, via a hybrid of Genetic Programming and formal verification, in which the traditional evaluation phase of Genetic Programming is augmented using new test cases obtained via counterexamples generated from an SMT solver. Prospectively, this work may pave the way for effective hybridization of heuristic search methods like GP with specbased synthesis. We find this possibility promising, given the limitations of contemporary exact methods of program synthesis that struggle to scale well with the length of synthesized programs. SMT solvers support also verification in other domains, such as Reals, Strings or Lists, so there are no fundamental obstacles to use CDGP for spec-based synthesis therein.

Acknowledgements

KK and IB acknowledge support from grant 2014/15/B/ST6/05205 funded by the National Science Centre, Poland. JS acknowledges the support of the EU

H2020 SAFIRE project (Ref. 723634). JD acknowledges the support of the DAASE project (EP/J017515/1).