Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications
By Iwo Bladek, Krzysztof Krawiec, Jerry Swan. 2018
14 citations recorded by the source corpus.
Conventional genetic programming (GP) can guarantee only that synthesized programs pass tests given by the provided input-output examples. The alternative to such a test-based approach is synthesizing programs by formal specification, typically realized with exact, nonheuristic algorithms. In this article, we build on our earlier study on Counterexample-Based Genetic Programming (CDGP), an evolutionary heuristic that synthesizes programs from formal specifications. The candidate programs in CDGP undergo formal verification with a Satisfiability Modulo Theory (SMT) solver, which results in counterexamples that are subsequently turned into tests and used to calculate fitness. The original CDGP is extended here with a fitness threshold parameter that decides which programs should be verified, a more rigorous mechanism for turning counterexamples into tests, and other conceptual and technical improvements. We apply it to 24 benchmarks representing two domains: the linear integer arithmetic (LIA) and the string manipulation (SLIA) problems, showing that CDGP can reliably synthesize provably correct programs in both domains. We also confront it with two state-of-the art exact program synthesis methods and demonstrate that CDGP effectively trades longer synthesis time for smaller program size.
Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software, Code Generation & Program Synthesis, Program Analysis & Verification
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Pamela Mishkin
- Gretchen Krueger
- Miles Brundage
- Jianfeng Gao
- Mohit Bansal
- Percy Liang
- Luke S. Zettlemoyer
- Yejin Choi
In Computational Theory and Mathematics
Citations in the corpus
- A Hazard Analysis Framework for Code Synthesis Large Language Models (2022, methodology): “However, using formal specifications as basis for synthesis methodologies is impractical, as is done in [6], if we wish to bring the power of synthesis and code generation to everyday development and productivity.”