Syntax-guided Synthesis

CS › Program Synthesis

updated on 2024-07-17: I implemented a mini sygus solver using Java

SyGuS

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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
; 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.

  1. Abstraction-based Enumeration

  2. Stochastic Enumeration

  3. Constraint-based Enumeration

  4. Learning-based Enumeration

2.2. Deductive Synthesis

3. Syntax of SyGuS

Intuitively the syntax seems very similar to Lisp. In fact the syntax of SyGuS is a superset of the syntax of the SMT-LIB standard. Here is the standard syntax of SyGuS.