We introduce the notion of property signatures, a representation for programs and
 program specifications meant for consumption by machine learning algorithms.
 Given a function with input type τ_in and output type τ_out, a property is a function
 of type: (τ_in, τ_out) → Bool that (informally) describes some simple property
 of the function under consideration. For instance, if τ_in and τ_out are both lists
 of the same type, one property might ask ‘is the input list the same length as the
 output list?’. If we have a list of such properties, we can evaluate them all for our
 function to get a list of outputs that we will call the property signature. Crucially,
 we can ‘guess’ the property signature for a function given only a set of input/output
 pairs meant to specify that function. We discuss several potential applications of
 property signatures and show experimentally that they can be used to improve
 over a baseline synthesizer so that it emits twice as many programs in less than
 one-tenth of the time. Program synthesis is a longstanding goal of computer science research (Manna & Waldinger, 1971; Waldinger et al., 1969; Summers, 1977; Shaw; Pnueli & Rosner, 1989; Manna & Waldinger, 1975) , arguably dating to the 1940s and 50s (Copeland, 2012; Backus et al., 1957) . Deep learning methods have shown promise at automatically generating programs from a small set of input-output examples (Balog et al., 2016; Devlin et al., 2017; Ellis et al., 2018b; 2019b) . In order to deliver on this promise, we believe it is important to represent programs and specifications in a way that supports learning. Just as computer vision methods benefit from the inductive bias inherent to convolutional neural networks (LeCun et al., 1989) , and likewise with LSTMs for natural language and other sequence data (Hochreiter & Schmidhuber, 1997) , it stands to reason that ML techniques for computer programs will benefit from architectures with a suitable inductive bias. We introduce a new representation for programs and their specifications, based on the principle that to represent a program, we can use a set of simpler programs. This leads us to introduce the concept of a property, which is a program that computes a boolean function of the input and output of another program. For example, consider the problem of synthesizing a program from a small set of input-output examples. Perhaps the synthesizer is given a few pairs of lists of integers, and the user hopes that the synthesizer will produce a sorting function. Then useful properties might include functions that check if the input and output lists have the same length, if the input list is a subset of the output, if element 0 of the output list is less than element 42, and so on. The outputs of a set of properties can be concatenated into a vector, yielding a representation that we call a property signature. Property signatures can then be used for consumption by machine learning algorithms, essentially serving as the first layer of a neural network. In this paper, we demonstrate the utility of property signatures for program synthesis, using them to perform a type of premise selection as in Balog et al. (2016) . More broadly, however, we envision that property signatures could be useful across a broad range of problems, including algorithm induction (Devlin et al., 2017) , improving code readability (Allamanis et al., 2014) , and program analysis (Heo et al., 2019) . More specifically, our contributions are: • We introduce the notion of property signatures, which are a general purpose way of featurizing both programs and program specifications (Section 3). • We demonstrate how to use property signatures within a machine-learning based synthesizer for a general-purpose programming language. This allows us to automatically learn a useful set of property signatures, rather than choosing them manually (Sections 3.2 and 4). • We show that a machine learning model can predict the signatures of individual functions given the signature of their composition, and describe several ways this could be used to improve existing synthesizers (Section 5). • We perform experiments on a new test set of 185 functional programs of varying difficulty, designed to be the sort of algorithmic problems that one would ask on an undergraduate computer science examination. We find that the use of property signatures leads to a dramatic improvement in the performance of the synthesizer, allowing it to synthesize over twice as many programs in less than one-tenth of the time (Section 4). An example of a complex program that was synthesized only by the property signatures method is shown in Listing 1. For our experiments, we created a specialized programming language, called Searcho 1 (Section 2), based on strongly-typed functional languages such as Standard ML and Haskell. Searcho is designed so that many similar programs can be executed rapidly, as is needed during a large-scale distributed search during synthesis. We release 2 the programming language, runtime environment, distributed search infrastructure, machine learning models, and training data from our experiments so that they can be used for future research. Listing 1: A program synthesized by our system, reformatted and with variables renamed for readability. This program returns the sub-list of all of the elements in a list that are distinct from their previous value in the list. In this work, we have introduced the idea of properties and property signatures. We have shown that property signatures allow us to synthesize programs that a baseline otherwise was not able to synthesize, and have sketched out other potential applications as well. Finally, we have open sourced all of our code, which we hope will accelerate future research into ML-guided program synthesis. The top-down synthesizer that we use as a baseline in this work. In a loop until a satisfying program is found or we run out of time, we pop the lowest-cost partial program from the queue of all partial programs, then we fill in the holes in all ways allowed by the type system, pushing each new partial program back onto the queue. If there are no holes to fill, the program is complete, and we check it against the spec. The cost of a partial program is the sum of the costs of its pool elements, plus a lower bound on the cost of filling each of its typed holes, plus the sum of the costs of a few special operations such as tuple construction and lambda abstraction.
We represent a computer program using a set of simpler programs and use this representation to improve program synthesis techniques.
{"src": "scitldr-AIC_train", "paper_id": "rylHspEKPr"}