Syntax-guided Synthesis

$$\Huge\textbf{Syntax-guided Synthesis} $$

1. Intro to SyGuS

Syntax-guided Synthesis (SyGuS) is a recent effort towards formalizing program synthesis where the logical specification is supplemented with a user-provided syntactic template to constrain the hypothesis space of possible programs.

The input $\mathcal I$ of SyGuS can be formalized as

$$\mathcal I=(T,\mathcal G,\phi) $$

where:

• $T$ is the vocabulary and interpretation of function and relation symbols,
• $\mathcal G$ is the syntactic set of candidate implementations
• $\phi$ is a semantic correctness specification for the desired program

Observe that

• $\mathcal G$ is used to constrain the program space
• and $\phi$ is to clarify user’s intent

The idea is very natural

An clear example is as follows.

; set the background theory to LIA 
(set-logic LIA) 

; grammar for max2 candidate implementations 
(synth-fun max2 ((x Int) (y Int)) Int 
           ((Start Int (x y 0 1 
                          (+ Start Start) 
                          (- Start Start) 
                          (ite StartBool Start Start))) 
             (StartBool Bool ((and StartBool StartBool) 
                              (or StartBool StartBool) 
                              (not StartBool) 
                              (<= Start Start) 
                              (= Start Start) 
                              (>= Start Start))))) 

; universally quantified input variables x and y 
(declare-var x Int)
(declare-var y Int) 

; correctness constraints on the max2 function 
(constraint (>= (max2 x y) x)) 
(constraint (>= (max2 x y) y)) 
(constraint (or (= x (max2 x y)) (= y (max2 x y)))) 

; synthesize command 
(check-synth)

2. Classification

The SyGuS community usually categorizes synthesis techniques into two classes:

1. Enumerative Synthesis: which systematically enumerates possible implementations of the function to be synthesized and checks if it satisfies the desired specification;
2. Deductive Synthesis: which tries to reduce the specification to a desired program, purely symbolically by applying a series of deductive rules.

2.1. Enumerative Synthesis

1. From smaller-sized to larger sized candidates

The simplest strategy begins the search from smaller-sized candidates and moves toward larger-sized candidates. This naive strategy guarantees to produce the smallest possible program, and is proven efficient for a wide spectrum of syntax-guided synthesis tasks.

2. Abstraction-based Enumeration

3. Stochastic Enumeration

4. Constraint-based Enumeration

5. Learning-based Enumeration

2.2. Deductive Synthesis

3. Syntax of SyGuS

Intuitively the syntax seems very similar to Lisp.