- author = "Krzysztof Krawiec and Iwo Bladek and Jerry Swan and John H. Drake",
- title = "Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs",
- booktitle = "Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)",
- year = "2018",
- editor = "Jerome Lang",
- pages = "5304--5308",
- address = "Stockholm",
- publisher_address = "Vienna University of Technology, Institute of Discrete Mathematics and Geometry, E104 Wiedner Hauptstr. 8-10, A-1040 Vienna, Austria",
- month = "13-19 " # jul,
- publisher = "International Joint Conferences on Artificial Intelligence",
- keywords = "genetic algorithms, genetic programming, Typed Genetic Programming, CDGP, Heuristic Search and Game Playing, Meta-Reasoning and Meta-heuristics, Agent-based and Multi-agent Systems, Formal Verification, Validation and Synthesis",
- isbn13 = "978-0-9992411-2-7",
-
URL = "
https://www.ijcai.org/proceedings/2018/742",
-
URL = "
https://www.ijcai.org/proceedings/2018/0742.pdf",
-
DOI = "
doi:10.24963/ijcai.2018/742",
- size = "5 pages",
- abstract = "Genetic programming is an effective technique for inductive synthesis of programs from tests, i.e. training examples of desired input-output behaviour. Programs synthesized in this way are not guaranteed to generalize beyond the training set, which is unacceptable in many applications. We present Counterexample-Driven Genetic Programming (CDGP) that employs evolutionary search to synthesize provably correct programs from formal specifications. CDGP employs a Satisfiability Modulo Theories (SMT) solver to formally verify programs in the evaluation phase. A failed verification produces counterexamples that are in turn used to calculate fitness and thereby drive the search process. When compared with a range of approaches on a suite of state-of-the-art specification-based synthesis benchmarks, CDGP systematically outperforms them, typically synthesising correct programs faster and using fewer tests.",
-
notes = "Lexicase selection. SAT solver, SMT solvers Microsoft
Z3.
Benchmarks: CountPos, IsSeries, IsSorted, Max, Median, Range, Search, Sum Max tree depth 12.
The source code of CDGP, along with specifications of problems, is available at https://github.com/kkrawiec/CDGP.
This paper is an abridged version of a paper titled Counterexample-Driven Genetic Programming \cite{Krawiec:2017:GECCOa} that won a best-paper award at the GECCO-2017 conference.",
