Program synthesis is a promising technique that automatically generates programs on behalf of
users. Users do not have to write any code, but only need to provide some high-level program
specifications. Over the years, research has shown program synthesis is applicable to many domains
such as text transformation and data extraction.
For example, to generate a program that only matches US phone numbers, the user can add some
positive and negative examples. The synthesizer will then generate a program like a regular
expression that matches the two positive examples and does not match with the negative example.
Like many machine learning models, existing synthesizers follow a black-box design.
As a result, there is no way to troubleshoot if a
synthesizer is behaving weirdly or if there is a synthesis failure.
In this work, we propose interpretable program synthesis, the first approach
that opens the black box and helps users understand the synthesis process,
so users can diagnose abnormal behaviors and guide the synthesizer to recover from those behaviors.
It’s very challenging to directly visualize or explain the runtime
behavior of a synthesizer to users. Because synthesizers are quite sophisticated.
Instead, we choose to visualize the explored program space. So users can understand in
what direction the synthesizer is searching and where the synthesizer is wasting a lot of time.
Our approach requires instrumenting a synthesizer,
so it will keep logging the programs it has tried during the synthesis process.
Then our approach visualizes these program candidates in three different ways.
Based on the insights from the visualization, the user can provide different kinds of
feedback to guide the synthesis process, such as prioritizing or eliminating a search direction.
In particular, we implemented an interpretable synthesizer for regular expressions.
We choose regular expressions because it’s widely used,
it’s hard to use, and it’s hard to synthesize.
After you add some examples and click the start button, you can monitor the synthesis process
through a live-updated line chart. This line chart shows the speed and the trend of the underlying
synthesis process. You can easily find out how many programs have been tried so far
and how many examples have been satisfied by each program candidate.
If you find something wield, like the line being zigzagging for a while,
you can make an early interruption and check what’s really going wrong.
After each synthesis iteration, you can use different sampling strategies to inspect concrete
program candidates from the explored program space. If you hover the mouse over a program
candidate, the input-output examples will be highlighted in different colors---green
means the example is satisfied by the program, and red means it is not satisfied by the program.
You can also look at the search directions a synthesizer has been through. This tree
visualization clusters all explored programs based on how they are derived from an
empty program step by step. The root of the tree is an empty program, and the internal
nodes are partial programs derived from the empty program. By expanding an internal node,
you can see how a partial program is further concretized during the synthesis process. Each
branch of the tree can be viewed as a search direction. You can prioritize a search direction
that looks promising to you or eliminate a search direction that looks unproductive. In this way,
you can manually prune the search space for the synthesizer and improve the search efficiency.
We did a within-subjects lab study with 18 students from Harvard SEAS. Each student
finished two randomly selected tasks in two conditions---one task using the interpretable
synthesizer and the other task using the same synthesizer without interpretability support.
We found that interpretable synthesis is most useful in challenging tasks.
Because the synthesizer often gets stuck in these challenging tasks and fails to generate any program
in a given time. When using a blackbox synthesizer, users can do nothing but just
tweaking their examples by guesswork. But with interpretable synthesis, they can troubleshoot
and figure out in which direction the synthesizer was wasting a lot of time.
Then they can prune the search space by removing the unproductive search path.
We also found that interpretability did not introduce more cognitive effort,
but users perceived much less frustration when using interpretable synthesis.
Please read our full paper to find more interesting results.