Program Recognition in Synthesis

Date:

Program synthesizers take some specification and produce one or more programs that likely implement it. However, there is a last-mile problem in this task, to actually determine if the output of the synthesizer accomplishes the input task. This task is program recognition. It asks, “does this program actually solve the task at hand?” This this work I run a formative study observing 4 Haskell programmers as they perform recognition tasks. I come away with a set of takeaways future work in synthesizers should deploy to make their tools more useful. I then discuss possible future tool directions, especially in the context of neural-guided synthesizers.

Download slides here