A Simple Inductive Synthesis Methodology and its Applications
Abstract
Given a high-level specification and a low-level programming
language, our goal is to automatically synthesize an
asymptotically optimal program that meets the specification.
In this paper, we present a new algorithm and methodology
for inductive synthesis that allows us to do this.
We use Second Order logic as our generic high level
specification logic. For our low-level languages we choose
small application-specific logics that can be immediately
translated into code that runs in expected linear time in the
worst case.
We explain our methodology and provide examples of the
synthesis of several graph classifiers, e.g, linear-time tests
of whether the input graph is connected, acyclic, etc. In another
set of applications we automatically derive many finite
differencing expressions equivalent to ones that Paige built
by hand in his thesis. Finally we describe directions
for automatically combining such automatically generated
building blocks to synthesize efficient code implementing
more complicated specifications.
The methods in this paper have been implemented in
Python using Z3 as the underlying checker. The tool is publically
available.