Synthesis through Unification Genetic Programming

Welsch, Thomas and Kurlin, Vitaliy ORCID: 0000-0001-5328-5351 (2020) Synthesis through Unification Genetic Programming. In: GECCO '20: Genetic and Evolutionary Computation Conference, 2020-7-8 - 2020-7-12.

Text Synthesis-through-Unification-Genetic-Programming.pdf - Author Accepted Manuscript Download (424kB) | Preview

Abstract

We present a new method, Synthesis through Unification Genetic Programming (STUN GP), which synthesizes provably correct programs using a Divide and Conquer approach. This method first splits the input space by undergoing a discovery phase that uses Counterexample-Driven Genetic Programming (CDGP) to identify a set of programs that are provably correct under unknown unification constraints. The STUN GP method then computes these restraints by synthesizing predicates with CDGP that strictly map inputs to programs where the output will be correct. This method builds on previous work towards applying Genetic Programming (GP) to Syntax Guided Synthesis (SyGus) problems that seek to synthesize programs adhering to a formal specification rather than a fixed set of input-output examples. We show that our method is more scalable than previous CDGP variants, solving several benchmarks from the SyGus Competition that cannot be solved by CDGP. STUN GP significantly cuts into the gap between GP and state-of-the-art SyGus solvers and further demonstrates Genetic Programming's potential for Program Synthesis.

Item Type:	Conference or Workshop Item (Unspecified)
Uncontrolled Keywords:	Genetic programming, Search Based Program Synthesis, Divide and Conquer
Depositing User:	Symplectic Admin
Date Deposited:	22 May 2020 08:17
Last Modified:	18 Jan 2023 23:51
DOI:	10.1145/3377930.3390208
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3088318