Sampling for Bayesian Program Learning
Towards learning programs from data, we introduce the problem of sampling programs from posterior distributions conditioned on that data. Within this setting, we propose an algorithm that uses a symbolic solver to efficiently sample programs. The proposal combines constraint-based program synthesis with sampling via random parity constraints. We give theoretical guarantees on how well the samples approximate the true posterior, and have empirical results showing the algorithm is efficient in practice, evaluating our approach on 22 program learning problems in the domains of text editing and computer-aided programming.
This paper describes an algorithm for sampling from the set of programs consistent with a given set of input-output training examples.  The programs come from a finite set of possible programs defined by a "sketch" (which seems to be essentially a grammar), with a description length prior.  The paper builds on the existing approach of program synthesis by constraint solving, where the possible programs are encoded as assignments to a set of Boolean variables, and a SAT solver is used to find programs consistent with the examples.  The advance in this paper is that rather than just finding a single most likely solution, the algorithm samples from the posterior.  The paper provides an error bound on the sampling probabilities that allows trading off time versus accuracy.
I found this paper interesting and well-written, but I have some significant questions and comments about the approach.   * Figure 5 (page 6) shows that the existing MDL approach of finding a single most likely program does slightly better than the proposed sampling approach in terms of average accuracy.  The paper argues that sampling is useful because we can find the C most frequently sampled programs and show them to a user.  As shown in Figure 6, there is more likely to be a correct program in the top 3 programs than in the top 1.  But if we want to show the top C programs, do we really need to perform sampling, which the paper says is complicated by the existence of many long and unlikely programs that match the training examples?  Why can't we simply find the MDL program and then run the solver again with length restrictions to find other consistent programs of the same length, or slightly longer lengths?  * Page 5, line 179 says that the paper "implicitly defined a description-length prior, where |x| is the number of bits required to specify x in the SAT encoding".  Looking at the constraints in Figure 2(c), it appears that if bits x_1, ..., x_k fully define a program, then bits x_{k+1}, ..., x_n end up unconstrained.  So is a program of length k represented by 2^{n-k} distinct assignments to the bits?  Is that what's meant by an implicitly defined prior?  If so, then it seems that the prior is uniform over bit assignments (although not over programs), and I don't see the point of mapping from a uniform distribution on a separate embedding space as discussed in Section 2.  * For string manipulation, the paper uses data sets of size 5, with 1-3 examples used for training.  This leaves only 2-4 examples for testing, which doesn't seem like enough to yield reliable results.  For list manipulation, I couldn't find a statement about the size of the test sets.  I assume correct programs for these example problems are known, so it should be straightforward to generate tests sets of at least size 100.  Using larger test sets would reduce the chance that some of the returned programs yield high test accuracy by accident.  == Update After Author Feedback == I appreciate the authors' responses to my comments.  I think I did misinterpret Figure 6; I understand now that it is referring to the top C most frequent combinations of program outputs, not the top C most frequent programs.  Still, it would be informative to compare explicitly to a K-best MDL approach, to demonstrate that integrating out the program really helps.  I'm still wondering about how the prior distribution over programs ends up being defined.  I asked in my review if a program of length k ended up being represented by 2^{n-k} distinct assignments to the bits in the SAT encoding, and the response seemed to agree that this was true.  But then why do we need to add auxiliary variables in the embedding space as described on page 4?  Isn't it enough to sampling from a uniform distribution over bit assignments?  If we start with a space where shorter programs already account for more assignments, and then we also add the auxiliary variables, don't we end up with a *squared* MDL prior?  I hope this can be clarified in the final version.