Hi Everyone,
You are welcome to join the
Synthesis / SemGuS Reading Group, which meets Thursdays from 1 to 2 on Zoom:
https://uwmadison.zoom.us/j/96450343227?pwd=emtGcHROSVZoOWsyWEFhN2wyazA2Zz09
This week, I will be presenting on
Combining the top-down propagation and bottom-up enumeration for inductive program synthesis (Lee, 2021).
Abstract:
We present an effective method for scalable and general-purpose inductive program synthesis. There have been two main approaches for inductive synthesis: enumerative search, which
repeatedly enumerates possible candidate programs, and the top-down propagation (TDP), which recursively decomposes a given large synthesis problem into smaller subproblems. Enumerative search is generally applicable but limited in scalability, and the TDP
is efficient but only works for special grammars or applications. In this paper, we synergistically combine the two approaches. We generate small program subexpressions via enumerative search and put them together into the desired program by using the TDP.
Enumerative search enables to bring the power of TDP into arbitrary grammars, and the TDP helps to overcome the limited scalability of enumerative search. We apply our approach to a standard formulation, syntax-guided synthesis (SyGuS), thereby supporting
a broad class of inductive synthesis problems. We have implemented our approach in a tool called Duet and evaluate it on SyGuS benchmark problems from various domains. We show that Duet achieves significant performance gains over existing general-purpose as
well as domain-specific synthesizers.
âHomework Questionâ:
Inverse semantics operators (a.k.a.
witness functions) are used to deduce specifications on sub-terms of an operator, given an outer specification on that operator. For example, consider the term
Substring(str, start, len). Given a spec that this term must satisfy, the jobs of the witness functions are to deduce specs on
str,
start, and len.
For
Substring(str, start, len), think about how you can constrain
str from a spec on the entire term. These specs are typically given as input-output examples, so given that
Substring(str, start, len) must return a string
s when evaluated on an input state i, what might a witness function for
str look like?
-Keith