- author = "Elizabeth Polgreen",
- title = "Synthesis without Syntactic Templates",
- school = "University of Oxford",
- year = "2019",
- address = "UK",
- keywords = "genetic algorithms, genetic programming",
-
URL = "
https://ora.ox.ac.uk/objects/uuid:3cd96a82-4a62-4a7f-a68e-5b37f7396b0e",
-
URL = "
https://ora.ox.ac.uk/objects/uuid:3cd96a82-4a62-4a7f-a68e-5b37f7396b0e/download_file?file_format=pdf&safe_filename=polgreen_thesis.pdf&type_of_work=Thesis",
-
URL = "https://polgreen.github.io/polgreen_thesis.pdf",
- size = "146 pages",
-
abstract = "Program synthesis is the mechanised construction of
software. One of the main difficulties is the efficient
exploration of the very large solution space, and tools
often require a user-provided syntactic restriction of
the search space. Writing such templates is often
challenging, particularly since any constants required
in the solution must be given in the template. In this
dissertation we explore the research hypothesis that
synthesis of programs without provision of such
syntactic templates is computationally feasible using
methods based on Counter Example Guided Inductive
Synthesis (CEGIS).
The key contribution of this dissertation is a new approach to program synthesis that combines the strengths of a counterexample-guided inductive synthesizer with those of a theory solver, exploring the solution space more efficiently without relying on user guidance. We call this approach CEGIS(T), where T is a first-order theory. Notably, since the publication of CEGIS(T), a variant of the algorithm has been implemented inside leading synthesis solver CVC4. CEGIS(T) is as complete (or incomplete) as CEGIS, and it does not affect worst-case run-time complexity considerations.
In combination with the development of CEGIS(T ), we introduced several algorithmic improvements that enhance both the performance of CEGIS(T ) and the baseline CEGIS algorithm. The first of these improvements is a significant change to the way we encode the synthesis problem for the SAT-based synthesis component of CEGIS in order to produce smaller formulae that can be more efficiently solved by SAT and SMT solvers. The second of these improvements is the use of incremental satisfiability solving in the synthesis component of CEGIS. Incremental satisfiability solving allows the SAT solver to re-use clauses learnt in previous CEGIS iterations, thus reducing the time per synthesis iteration.
We evaluate our contributions on a set of benchmarks taken from the Syntax Guided Synthesis Competition, and note that CEGIS(T ) is able to solve benchmarks which elude a standard implementation of CEGIS, specifically benchmarks that contain non-trivial constants. We find that the novel proposed encoding provides a substantial speed-up on all the benchmarks that require synthesising a program of length greater than one instruction. The use of incremental first-order solving in CEGIS decreases the solving time in some cases but not all, and we hypothesise that these are the benchmarks on which SAT-solver pre-processing is less important.",
-
notes = "p18 'CEGIS has been implemented using genetic
programming as a learning method within the CEGIS loop
[35].'
Supervisor: Alessandro Abate",
