Benjamin Caulfield

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2021-113

May 14, 2021

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-113.pdf

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 laypeople 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 study the problem of exact active learning of concepts that are comprised of independent components, and show 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.

Advisors: Sanjit A. Seshia and Stavros Tripakis

---

BibTeX citation:

@phdthesis{Caulfield:EECS-2021-113,
    Author= {Caulfield, Benjamin},
    Title= {Learning and Logic for Formal Synthesis},
    School= {EECS Department, University of California, Berkeley},
    Year= {2021},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-113.html},
    Number= {UCB/EECS-2021-113},
    Abstract= {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 laypeople 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 study the problem of exact active learning of concepts that are comprised of independent components, and show 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.},
}

EndNote citation:

%0 Thesis
%A Caulfield, Benjamin 
%T Learning and Logic for Formal Synthesis
%I EECS Department, University of California, Berkeley
%D 2021
%8 May 14
%@ UCB/EECS-2021-113
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2021/EECS-2021-113.html
%F Caulfield:EECS-2021-113