Program Synthesis

The Syntax-Guided Synthesis (SyGuS) framework provides a unified format for describing program synthesis problems by specifying (1) logical specifications of desired functionalities and (2) the syntax allowed for the implementation. Given these two inputs, SyGuS tools search for a program within the set of programs allowed by the syntax that satisfies the specifications.

Definition (SyGuS Problem)

A SyGuS problem for an n-ary (first-order) function f in a background theory T includes:

  1. A set of syntactic restrictions given by a grammar \(\mathcal{R}\).

  2. A set of semantic restrictions, i.e., specifications, given by a T-formula of the form \(\exists f. \forall x. \varphi(f, \bar{x})\), where \(\varphi\) is typically a quantifier-free formula involving (second-order) variable f and first-order variables \(\bar{x} = (x_1, \ldots, x_n)\).

A grammar \(\mathcal{R}\) consists of an initial symbol \(s_0\), a set of non-terminal symbols S (where \(s_0 \in S\)), and a set of rules \(s \to t\), where \(s \in S\) and t is a term constructed from symbols in S, free variables, and symbols from the T signature, with the first two serving as terminal symbols. The rule set R defines the rewriting relation between terms s and t, denoted as \(\to\). If there exists \(s_0 \to^\star t\) where t does not contain symbols from S, term t is said to be generated by R.

For a function f, a solution is a closed lambda term \(\lambda \bar{y} . t\) of the same type, where t is generated by R and \(\forall \bar{x} . \varphi(\lambda \bar{y} . t, \bar{x})\) holds valid in T.

Programming by Examples

Synthesizing Inductive Invariants

Consider the following program. We require an inductive invariant that is strong enough to prove that the assertion at Line 6 always holds:

assume 0 <= n and 0 <=m <= n;
assume x = 0 and y = m;
while (x < n) {
    x = x + 1;
    if (x > m) { y = y + 1; }
}
assert y = n;

In the SyGuS setting, we need to synthesize a predicate \(I : \mathbb{Z}^4 \to \mathbb{B}\) defined on a symbolic state \(\sigma = \langle m, n, x, y \rangle\), which satisfies \(\forall \sigma . \varphi(I, \sigma)\) for the specification \(\varphi\):

  • \((0 \leq n \land 0 \leq m \leq n \land x = 0 \land y= m) \Rightarrow I(\sigma)\) (precondition)

  • \(\forall \sigma' . (I(\sigma) \land T(\sigma, \sigma')) \Rightarrow I(\sigma')\) (inductiveness)

  • \((x \geq n \land I(\sigma)) \Rightarrow y = n\) (postcondition)

where \(\sigma = \langle m', n', x', y' \rangle\) denotes that the new state after on iteration, and T is a transition relation that describes the loop body:

\[\begin{split}T(\sigma, \sigma') &\equiv (x < n) \land (x' = x + 1) \land (m' = m) \land (n' = n) \\ &\land [(x' \leq m \land y' = y) \lor (x' > m \land y' = y + 1)]\end{split}\]

References

[Gulwani2011]

Sumit Gulwani. “Automating String Processing in Spreadsheets using Input-Output Examples.” POPL, 2011.

[Gulwani2014]

Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. “Program Synthesis.” Foundations and Trends in Programming Languages, 2014.

[Alur2013]

Rajeev Alur, Dana Fisman, Rishabh Singh, and Armando Solar-Lezama. “SyGuS-Comp 2013: Results and Analysis.” Technical Report, University of Pennsylvania, 2013.