Counterexample-Driven Genetic Programming: Heuristic Program Synthesis from Formal Specifications

Area of Science:

• Computer Science
• Artificial Intelligence
• Software Engineering

Background:

• Conventional genetic programming (GP) relies on input-output examples, offering limited guarantees of program correctness.
• Formal specification-based program synthesis typically employs exact, non-heuristic algorithms.
• Counterexample-Based Genetic Programming (CDGP) is an evolutionary heuristic for synthesizing programs from formal specifications.

Purpose of the Study:

• To extend and improve the Counterexample-Based Genetic Programming (CDGP) heuristic.
• To enhance the formal verification and fitness calculation mechanisms within CDGP.
• To evaluate the effectiveness of the improved CDGP on linear integer arithmetic (LIA) and string manipulation (SLIA) benchmarks.

Main Methods:

• Utilizing a Satisfiability Modulo Theory (SMT) solver for formal verification of candidate programs.
• Transforming counterexamples generated by the SMT solver into test cases for fitness evaluation.
• Implementing a fitness threshold parameter to guide the verification process.
• Introducing a more rigorous method for converting counterexamples into tests.

Main Results:

• The enhanced CDGP reliably synthesizes provably correct programs across 24 benchmarks in LIA and SLIA domains.
• CDGP demonstrates effectiveness in generating correct programs compared to state-of-the-art exact synthesis methods.
• The approach shows a trade-off between synthesis time and resulting program size, favoring smaller programs with longer computation.

Conclusions:

• The improved CDGP is a robust evolutionary heuristic for synthesizing provably correct programs from formal specifications.
• CDGP offers a viable alternative to exact methods, particularly when program correctness and size are critical.
• The study validates CDGP's capability in complex domains like LIA and SLIA, paving the way for further research in evolutionary program synthesis.