UC Berkeley

Program synthesis is the use of algorithms to derive programs that satisfy given specifications. These specifications are usually given in some form of computer-understandable logic. Specifications are usually much easier to write than the programs themselves. By ‘filling in the details’ given by the specification, program synthesis opens the possibility of creating simple programs to both lay people and non-programming domain experts.

Recent work in program synthesis has used techniques from ‘exact active learning’, where learning algorithms are able to pose queries to oracles. In the case of program synthesis, these oracles are implemented by checking potential programs against the given specification or asking a user for more inputs.

Another recent development in the field is Syntax-Guided Synthesis (SyGuS), where the space of potential programs is given by a tree-grammar (or context-free grammar). Specifications are given in the logic of SMT (satisfiability modulo theories) problems.

This thesis further develops the theory behind exact active learning, program synthesis, and their intersection. We provide upper and lower bounds, including undecidability results, for SyGuS problems defined on various SMT theories. We introduce the subject of actively learning equational theories and show how it can be used to learn constrained EUF formulas. We expand the problem of learning symbolic automata to use different types of symbolic counterexamples. We study the problem of exact active learning of concepts that are comprised of independent components, andshow when the knowledge that components work independently can significantly reduce learning complexity. Finally, we introduce new methods for SyGuS solving with respect to cost, where the goal is to find the minimal cost program satisfying a specification.