Program synthesis via unification in Lean: some first steps

Stream: general

[Rish Vaishnav]

Over the past month and a half, I've been experimenting a bit with possible approaches to verified program synthesis in Lean (using the new Std.Do library). I've discovered some interesting possibilities here, and wanted to share what I've done so far for anyone who may be interested in this topic.

The main idea I've been working with is to use Lean's unification algorithm to synthesize parts of Lean programs. For instance, in the following example, we can manually synthesize a "hole" in the definition of f, by proving the existence of a value to fill the hole to allow us to satisfy the spec. A metavar representing the hole is assigned through unification when we use the rfl tactic:

import Std.Do

-- `x` is a "hole" in the definition of the function `f`
def f (x : Nat) : Id Nat := do
  pure x

theorem f_spec :
    ∃ x,
   ⦃⌜True⌝⦄
   f x
   ⦃⇓ r => ⌜r = 0⌝⦄ := by
  -- Given an existential goal `∃ x : T, P x`, `exists? mvar` will create
  -- a new metavariable `?mvar : T` which is provided as the existential
  -- witness, leaving us with the goal `P ?mvar`. `?mvar` can then be
  -- assigned via unification during the proof.
  exists? mvar1
  -- ⊢ ⦃⌜True⌝⦄ f ?mvar1 ⦃⇓r => ⌜r = 0⌝⦄
  mintro -
  unfold f
  simp
  -- ⊢ ?mvar1 = 0
  rfl -- assigns `?mvar1 = 0`

I had to write the custom tactic exists? to get this to work, as well as a few more custom tactics that can be found in this file. These tactics allowed me to extend this experiment to a larger proof of the qpartition subroutine of the standard library's qsort quicksort function. I have incrementally eaten away at the original definition of the qpartition function by introducing holes to arrive at this program sketch, and I was able to write a proof of correctness that "synthesizes" the holes via unification. I was also able to synthesize parts of the loop invariant used in the proof.

As you can see, given the overall structure of the program, as well as some lemmas from a "specification theory" that can be found here, I was able to use just a few different tactics to synthesize a good number of the Nats from the original implementation (there's a few more in there that I haven't gotten around to trying yet; ignore the FIXMEs for now, that's where I noticed that some desired automation is currently lacking). This would seem to point to a particular strategy for program synthesis in Lean, in which we rely entirely on Lean's unification algorithm to fill in missing holes from programs during a proof of the existence of values filling the holes that allow the spec to be satisfied. The fact that I was able to do this with such a limited set of tactics suggests that it may be possible to arrive at such a proof via near-exhaustive search within a reasonable amount of time using a tool like Pantograph -- well, at least at this small scale. I imagine that scaling this form of synthesis up to larger programs with larger specification theories is where ML techniques may become relevant (reinforcement learning, in particular) to achieve more efficient search.

One technical issue here: due to small elimination, we can't extract the actual existential witnesses from the proof -- we need these to instantiate the holes to finally construct the verified program. This may be fairly trivial to solve, however, by having the tactic proof keep track of the metavar assignments to generate an auxiliary definition from.

The major question here is how we could possibly extend this approach to synthesize actual monadic program fragments. I was quite successful here synthesizing argument subexpressions of certain monadic function calls, but how do we synthesize the calls themselves? I don't think this can (or should) be achieved by unification -- however, given a "monadic hole" with unknown preconditions and postconditions, we can use unification to constrain what "overall shape" these pre- and postconditions should have, such that we narrow down which possible calls can fill these holes such that they "fit the mold" of the specification shape imposed by the subsequent proof. We'll also likely have to account for the interactions with mvcgen, since the verification conditions will change as we progressively flesh out a monadic hole's pre- and postconditions.

It seems like this might be a new approach to program synthesis, at least as far as I have read in Armando Solar-Lezama's lecture notes on the topic. What I've done so far seems most similar to Solar-Lezama's "Sketch" tool, which similarly allows the user to leave holes in programs that are synthesized. The difference is that it does so by using the holes to produce constraints that are passed to an SAT solver. The benefit of this approach could be that since we only rely on unification for synthesis, we aren't constrained by the capabilities of a SAT solver, but rather by the richness of our tactic DSL (which, once we have run through sufficiently many examples, should approach something that is fairly "fixed") and the user-provided specification theory.

I'll be burying my nose into writing my thesis over the next month or so, but in the meantime I just wanted to see what our initial thoughts are on this possible approach.

[Rish Vaishnav]

(I should probably mention that this approach is not to be confused with "Synthesis through Unification" (STUN) which is another approach to program synthesis that uses the word "unification" in quite a different sense)