Review: Syntax-Guided Synthesis

I was describing my idea from last week to automatically optimize programs to Colin, who pointed me towards Syntax-Guided Synthesis by Alur et al.

Syntax-Guided Synthesis is the idea that free-range program synthesis is really hard, so instead, let’s constrain the search space with a grammar of allowable programs. We can then enumerate those possible programs, attempting to find one that satisfies some constraints. The idea is quite straightforward when you see it, but that’s not to say it’s unimpressive; the paper has lots of quantitative results about exactly how well this approach does.

The idea is we want to find programs with type I O, that satisfy some specification. We’ll do that by picking some Language of syntax, and trying to build our programs there.

All of this is sorta moot, because we assume we have some oracle which can tell us if our program satisfies the spec. But the oracle is probably some SMT solver, and is thus expensive to call, so we’d like to try hard not to call it if possible.

Let’s take an example, and say that we’d like to synthesize the max of two Nats. There are lots of ways of doing that! But we’d like to find a function that satisfies the following:

data MaxSpec (f :  ×   ) :  ×   Set where
  is-max : {x y : }
          x  f (x , y)
          y  f (x , y)
          ((f (x , y)  x)  (f (x , y)  y))
          MaxSpec f (x , y)

If we can successfully produce an element of MaxSpec f, we have a proof that f is an implementation of max. Of course, actually producing such a thing is rather tricky; it’s equivalent to determining if MaxSpec f is Decidable for the given input.

In the first three cases, we have some conflicting piece of information, so we are unable to produce a MaxSpec:

decideMax : (f :  ×   )  (i :  × )  Dec (MaxSpec f i)
decideMax f i@(x , y) with f i | inspect f i
... | o | [ fi≡o ] with x ≤? o | y ≤? o
... | no ¬x≤o | _ = no λ { (is-max x≤o _ _) 
        contradiction (≤-trans x≤o (≤-reflexive fi≡o)) ¬x≤o }
... | yes _ | no ¬y≤o = no λ { (is-max x y≤o x₂) 
        contradiction (≤-trans y≤o (≤-reflexive fi≡o)) ¬y≤o }
... | yes x≤o | yes y≤o with o  x | o  y
... | no x≠o | no y≠o =
        no λ { (is-max x x₁ (inj₁ x₂)) 
                  contradiction (trans (sym fi≡o) x₂) x≠o
             ; (is-max x x₁ (inj₂ y)) 
                  contradiction (trans (sym fi≡o) y) y≠o

Otherwise, we have a proof that o is equal to either y or x:

... | no proof | yes o≡y = yes
        (is-max (≤-trans x≤o (≤-reflexive (sym fi≡o)))
                (≤-trans y≤o (≤-reflexive (sym fi≡o)))
                (inj₂ (trans fi≡o o≡y)))
... | yes o≡x | _ = yes
        (is-max (≤-trans x≤o (≤-reflexive (sym fi≡o)))
                (≤-trans y≤o (≤-reflexive (sym fi≡o)))
                (inj₁ (trans fi≡o o≡x)))

MaxSpec is a proof that our function is an implementation of max, and decideMax is a proof that “we’d know one if we saw one.” So that’s the specification taken care of. The next step is to define the syntax we’d like to guard our search.

The paper presents this syntax as a BNF grammar, but my thought is why use a grammar when we could instead use a type system? Our syntax is a tiny little branching calculus, capable of representing Terms and branching Conditionals:

  data Term : Set where
    var-x : Term
    var-y : Term
    const :   Term
    if-then-else : Cond  Term  Term  Term

  data Cond : Set where
    leq : Term  Term  Cond
    and : Cond  Cond  Cond
    invert : Cond  Cond

All that’s left for our example is the ability to “compile” a Term down to a candidate function. Just pattern match on the constructors and push the inputs around until we’re done:

  eval : Term   ×   
  eval var-x (x , y) = x
  eval var-y (x , y) = y
  eval (const c) (x , y) = c
  eval (if-then-else c t f) i =
    if evalCond c i then eval t i else eval f i

  evalCond : Cond   ×   Bool
  evalCond (leq m n) i   = Dec.does (eval m i ≤? eval n i)
  evalCond (and c1 c2) i = evalCond c1 i  evalCond c2 i
  evalCond (invert c) i  = not (evalCond c i)

So that’s most of the idea; we’ve specified what we’re looking for, via MaxSpec, what our syntax is, via Term, and a way of compiling our syntax into functions, via eval. This is the gist of the technique; the rest is just algorithms.

The paper presents several algorithms and evaluates their performances. But one is clearly better than the others in the included benchmarks, so we’ll just go through that one.

Our algorithm to synthesize code corresponding to the specification takes a few parameters. We’ve seen the first few:

module Solver
    {Lang I O : Set}
    (spec : (I  O)  I  Set)
    (decide : (f : I  O)  (i : I)  Dec (spec f i))
    (compile : Lang  I  O)

However, we also need a way of synthesizing terms in our Language. For that, we’ll use enumerate, which maps a natural number to a term:

    (enumerate :   Lang)

Although it’s not necessary for the algorithm, we should be able to implement exhaustive over enumerate, which states every Lang is eventually produced by enumerate:

    (exhaustive : (x : Lang)  Σ[ n   ] (enumerate n  x))

Finally, we need an oracle capable of telling us if our solution is correct. This might sound a bit like cheating, but behind the scenes it’s just a magic SMT solver. The idea is that SMT can either confirm that our program is correct, or produce a counterexample that violates the spec. The type here is a bit crazy, so we’ll take it one step at a time.

An oracle is a function that takes a Lang

      : (exp : Lang)

and either gives back a function that can produce a spec (compile exp) for every input:

         ((i : I)  spec (compile exp) i)

or gives back some input which is not a spec (compile exp):

         Σ[ i  I ] ¬ spec (compile exp) i)

The algorithm here is actually quite clever. The idea is that to try each enumerated value in order, attempting to minimize the number of calls we make to the oracle, because they’re expensive. So instead, well keep a list of every counterexample we’ve seen so far, and ensure that our synthesized function passes all of them before sending it off to the oracle. First, we’ll need a data structure to store our search progress:

  record SearchState : Set where
      iteration : 
      cases : List I
  open SearchState

The initial search state is one in which we start at the beginning, and have no counterexamples:

  start : SearchState
  iteration start = 0
  cases start = []

We can try a function by testing every counterexample:

  try : (I  O)  List I  Bool
  try f = all (Dec.does  decide f)

and finally, can now attempt to synthesize some code. Our function check takes a SearchState, and either gives back the next step of the search, or some program, and a proof that it’s what we’re looking for.

      : SearchState
           (Σ[ exp  Lang ] ((i : I)  spec (compile exp) i))
  check ss

We begin by getting and compiling the next enumerated term:

           with enumerate (iteration ss)
  ... | exp with compile exp

check if it passes all the previous counterexamples:

  ... | f with try f (cases ss)

if it doesn’t, just fail with the next iteration:

  ... | false = inj₁ (record { iteration = suc (iteration ss)
                             ; cases = cases ss

Otherwise, our proposed function might just be the thing we’re looking for, so it’s time to consult the oracle:

  ... | true with oracle exp

which either gives a counterexample that we need to record:

  ... | inj₂ (y , _) =
          inj₁ (record { iteration = suc (iteration ss)
                       ; cases = y  cases ss

or it confirms that our function satisfies the specification, and thus that were done:

  ... | inj₁ x = inj₂ (exp , x)

Pretty cool! The paper gives an optimization that caches the result of every counterexample on every synthesized program, and reuses these whenever that program appears as a subprogram of a larger one. The idea is that we can trade storage so we only ever need to evaluate each subprogram once — important for expensive computations.

Of course, pumping check by hand is annoying, so we can instead package it up as solve which takes a search depth, and iterates check until it runs out of gas or gets the right answer:

       Maybe (Σ[ exp  Lang ] ((i : I)  spec (compile exp) i))
  solve = go start
          : SearchState
              (Σ Lang  exp  (i : I)  spec (compile exp) i))
      go ss zero = nothing
      go ss (suc n) with check ss
      ... | inj₁ x = go ss n
      ... | inj₂ y = just y