Learning to Represent Programs with Property Signatures

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 τ₈₍ and output type τ₎ₔₓ, a property is a function of type: (τ₈₍, τ₎ₔₓ) Bool that (informally) describes some simple property of the function under consideration. For instance, if τ₈₍ and τ₎ₔₓ 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.