Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs
Abstract
Genetic programming is an effective technique for inductive synthesis of programs from tests, i.e. training examples of desired input-output behavior. 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 synthesizing correct programs faster and using fewer tests.
Cite
Text
Krawiec et al. "Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs." International Joint Conference on Artificial Intelligence, 2018. doi:10.24963/IJCAI.2018/742Markdown
[Krawiec et al. "Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs." International Joint Conference on Artificial Intelligence, 2018.](https://mlanthology.org/ijcai/2018/krawiec2018ijcai-counterexample/) doi:10.24963/IJCAI.2018/742BibTeX
@inproceedings{krawiec2018ijcai-counterexample,
title = {{Counterexample-Driven Genetic Programming: Stochastic Synthesis of Provably Correct Programs}},
author = {Krawiec, Krzysztof and Bladek, Iwo and Swan, Jerry and Drake, John H.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2018},
pages = {5304-5308},
doi = {10.24963/IJCAI.2018/742},
url = {https://mlanthology.org/ijcai/2018/krawiec2018ijcai-counterexample/}
}