Counterexample-Driven Genetic Programming (CDGP) aims to close the gap between inductive program synthesis methods using heuristic search, more precisely genetic programming (GP), and (deductive) program synthesis from a formal specification of the problem. To ensure that a synthesized program meets the formal specification for all possible inputs, a logical proof must be conducted. In our implementation, for proving program correctnes we employ an external Satisfiability Modulo Theories (SMT) solver.
CDGP, similarly to the standard GP, utilizes evolutionary search to find the expected program. It starts with an empty set of test cases. After a new population is created and evaluated on the current set of tests, solutions are verified against the formal specification. If a program is correct, then the evolution ends and it is returned. If a program is incorrect, a counterexample input returned by an SMT solver is transformed to a test and added to the set of test cases. A parameter '--testsRatio' can be used to specify, what ratio of collected tests must be passed in order to apply verification.
Here is the conceptual diagram of CDGP, taken from the publication:
- FUEL - main evolution engine.
- SWIM - GP utilities for FUEL.
- SyGuS - parser for the format used by the SyGuS ('Syntax Guided Synthesis') competition.
You can create a project in an IDE such as Eclipse or IntelliJ IDEA, or use SBT to automatically download all dependencies and produce a jar file.
A path to the benchmark (i.e. problem specification) is specified with '--benchmark' option.
CDGP to run requires a path to the SMT solver, which must be provided using the '--solverPath' option. CDGP was tested for the following open source SMT solvers:
Because of slight differences between them and different required parameters, a type of the solver must be provided as an argument of the '--solverType' option. The accepted values are: 'z3' (default), 'cvc4', 'other'. With the '--moreArgs' option you can provide additional solver parameters, which will be prepended to those preset for the given solver.
K. Krawiec, I. Błądek, J. Swan, Counterexample-Driven Genetic Programming, Genetic and Evolutionary Computation Conference (GECCO), Berlin, July 17-19, 2017, DOI: http://dx.doi.org/10.1145/3071178.3071224.