Synthesis with automatically generated inputs

One of the largest issues with program synthesis right now is that it requires a lot of knowledge of synthesis to be actually used.  Indeed, sometimes the synthesis will fail to give an answer due to underspecification, and only an advanced user with deep knowledge of the synthesis engine will understand where that underspecification lies.  For that advanced user, it is easy to identify the underspecification, provide the required spec, and watch synthesis succeed.  However, users who have the knowledge of that in general don’t need synthesis.  While they can use synthesis for some small helper functions (I recently used synthesis for the generation of a cartesian map), the majority of the time those users aren’t the ones who can benefit the most from synthesis.

However, the synthesis engine itself is aware of when it’s underspecified.  For example, during a case analysis, the synthesis engine can see that one of the cases is not hit through any of the examples.  Guessing randomly in this circumstance is very likely to fail, and will very likely require some more user input to work.  Then the user will need to go through the code, confirm that it was synthesized correctly or incorrectly, and think up the right example to specify that incorrect codepath.  After that, they will need to rerun the synthesis algorithm from the start again, creating and subsequently pruning large numbers of potential programs before finally getting to the same place as before, and being able to now progress further.

Indeed, one could even see a scenario, when attempting to verify whether a program is one of two potential synthesized programs, running some static analysis on them, and using that analysis to provide an example input where the two programs deviate, and providing a user with a multiple choice about which output should be created from the input.

Lastly, one could see the potential for the user taking even more interaction.  The synthesizer could provide examples of a general nature, for example, saying “consider running f on a::b, would you like to return a) a, b) f b, c) something else, d) depends on a, e) depends on b, f) depends on a and b.  In this way, the user doesn’t need to understand syntax or how to code, but they can direct the program into the correct answer through their knowledge of how the code works.  And it can direct through some of the hardest parts of synthesis, finding when case analysis needs to be applied.


An IDE tool for data structure changes

A few days ago I was writing some unit tests for my code, when I realized the data structure my code was based on was incorrect.  I had, as one of the variants of my data type, RegExBase char, where I wanted RegExBase string instead.  This is because I wanted to be able to express empty string as a valid regular expression (other strings can just be built up from RegExConcat (regex * regex)).

This change was a fairly minor one, and the only real code changes I needed to make were in the pretty printer… and in the unit tests.  The changes I needed to make for the unit tests were fairly easy (search and replace ‘ for “).  However, it did highlight a critical flaw that many people who are unwilling to adopt unit testing bring up.  Adding in unit tests increases development time, and makes refactoring more difficult.  Increasing development time is up for debate, I saw a recent study that showed that TDD increased initial development time by ~20%, but caused there to be ~20% fewer bugs (I could be wrong on those percentages).  Of course, unit tests aren’t merely for decreasing bugs right there, serve as documentation for future users about the intention of the code.  However, refactoring is certainly more difficult for a user who knows the codebase.  It makes refactoring easier for future developers, as they can understand the code, but for the original author of the code, who understands how everything fits together, the unit tests are merely a barrier in the way of refactoring.

However, the IDE has a wealth of information available to it during these transformations.  Not only does it see the before and after state of the data structure, it also sees how the actual code is changed to work with the new data structure, and it knows it wants all previously failing tests to continue failing, and all previously succeeding tests to continue succeeding.  The IDE can use this information to make (or give suggestions) at automated changes to the unit tests.

But it can go a step further.  While it can automatically synthesize new unit tests, perhaps it can go the reverse direction, and a user needs to change the unit tests, and the code already changes.  This then begins to look like a normal input-output synthesis problem, but with the additional information about how the code was changed in the unit tests.  And it can then go even further, where maybe just one or two unit tests are changed, and it tries to generalize to the normal code and the rest of the unit tests.  Or maybe only one function is changed, and it tries to generalize to the rest of the code and all the unit tests.  This could make refactoring significantly easier when there are simple changes like changing a character parameter to a string parameter, especially when working with a large codebase, where large amounts of time could be spent chasing where the build failures occur.

Changes in landscape causing changes in approaches

In computer science research, a trend I’ve noticed in research is the trend of creation of an area -> research into that area until most of that theory is solved -> work on the problem in slightly different contexts.

For example, in program synthesis, the creation of the area is first formalizations of computation (thanks Turing and Church!).  Finding a program that meets a general specification is an undecidable problem, but the programs themselves are recursively enumerable.  We can build some naive enumeration of the programs, and be done with it, saying “they are now recursively enumerable.”

Next, the problem stops being in the purely abstract, and starts being in the practical.  Processors have become faster, and SAT solvers have become insane, and program synthesis looks more possible.  Now, merely having an enumeration is not enough.  While all the programs are recursively enumerable, we want to know, is there a nice way we can enumerate.  Can we enumerate so that simpler programs are enumerated first, under the assumption that simpler programs are more likely to be the programs needed in practice.  This can be done for a while, and then certain abstractions can be made to hit a larger class of problems.  SyGuS gets developed and makes it so that those problems get solved.

Then, inevitably, new problems arise.  What about using synthesis on  probabilistic models.  This can fit into the problems SyGuS solves (although with the added complication of needing a slightly different metric for finding correct – correct meaning in this situation the best fitting non-overfit model), but it doesn’t in practicality without significant changes.  Merely searching through the models doesn’t work, as this problem is slightly different than the others, the search space of likely programs is smaller, but the programs take much more time to evaluate.  This causes a new problem, how do we handle this slow evaluation.  Are there ways to share computation of the evaluations between models?  Is a slightly differently oriented search space perhaps better for sharing evaluations than the standard approach?  By looking at finer grained problems, different optimizations can be put in place, providing new research opportunities.

EDIT: Originally this was intended to be looking at how looking at smaller things provides potentially very different problems, but after rereading, much of it seems to just be merely stealing Dave’s confluences speech.  Oh well, someday I’ll have a unique thought…