that exponentially many intermediate programs are explored during search, so the model needs to be both very fast and very accurate to yield wall-clock time speed-ups. We are allowed to incur some slowdown, because if the model is accurate enough, we can search many fewer values before finding solutions. However, executing a program is still orders of magnitude faster than performing inference on even a small machine learning model, so this problem is severe. We employ two techniques to deal with this: First, we arrange both the synthesizer and the model so that we can batch model prediction across hundreds of intermediate values. Second, we process intermediate expressions using property signatures [@SIGNATURES], which featurize program inputs using another set of programs.

A second big challenge is that neural networks require large amounts of data to train, but there is no available data source of intermediate expressions. We can generate programs at random to train the model following previous work [@DEEPCODER; @ROBUSTFILL], but models trained on random programs do not always transfer to human-written benchmarks [@shin2019-sv]. We show that our use of property signatures helps with this distribution mismatch problem as well.

In summary, this paper makes the following contributions:

-   