Title: LEARNING TO SELECT EXAMPLES FOR PROGRAM SYNTHESIS Anonymous authors Paper under double-blind review

Abstract: Program synthesis is a class of regression problems where one seeks a solution, in the form of a source-code program, that maps the inputs to their corresponding outputs exactly. Due to its precise and combinatorial nature, it is commonly formulated as a constraint satisfaction problem, where input-output examples are encoded as constraints and solved with a constraint solver. A key challenge of this formulation is scalability: while constraint solvers work well with few wellchosen examples, constraining on the entire set of examples incurs significant overhead in both time and memory. In this paper we address this challenge by constructing a representative subset of examples that is both small and able to constrain the solver sufficiently. We build the subset one example at a time, using a trained discriminator to predict the probability of unchosen input-output examples conditioned on the chosen input-output examples, adding the least probable example to the subset. Experiment on a diagram drawing domain shows our approach produces subsets of examples that are small and representative for the constraint solver.

1. INTRODUCTION:

Program synthesis (or synthesis for short) is a special class of regression problems where rather than minimizing the error on an example dataset, one seeks an exact fit of the examples in the form of a program. Applications include synthesizing database relations (Singh et al. (2017) ), inferring excelformulas (Gulwani et al. (2012) ), and compilation (Phothilimthana et al. (2016) ). In these domains, the synthesizer was able to come up with complex programs consisting of branches, loops, and other programming constructs. Recent efforts (Ellis et al. (2015) ; Singh et al. (2017) ) show an interest in applying the synthesis technique to large sets of examples, but scalability remains an open problem. In this paper we present a technique to select from a large dataset of examples a representative subset that is sufficient to synthesize a correct program, yet small enough to solve efficiently.

There are two key ingredients to a synthesis problem: a domain specific language (DSL for short) and a specification. The DSL defines a space of candidate programs which serve as the model class. The specification is commonly expressed as a set of example input-output pairs which the candidate program needs to fit exactly. The DSL restricts the structure of the programs in such a way that it is difficult to fit the input-output examples in an ad-hoc fashion: This structure aids generalization to an unseen input despite "over" fitting the input-output examples during training.

Given the precise and combinatorial nature of a synthesis problem, gradient-descent based approaches perform poorly and an explicit search over the solution space is required (Gaunt et al. (2016) ). For this reason, synthesis is commonly casted as a constraint satisfaction problem (CSP) (Solar-Lezama (2013) ; Jha et al. (2010) ). In such a setting, the DSL and its execution can be thought of as a parametrized function F , which is encoded as a logical formula. Its free variables s ∈ S correspond to different parametrization within the DSL, and the input-output examples D are expressed as constraints which the instantiated program needs to satisfy, namely, producing the correct output on a given input.

∃s ∈ S.:

(xi,yi)∈D

F (x i ; s) = y i .

The encoded formula is then given to a constraint solver such as Z3 (de Moura & Bjørner (2008) ), which solves the constraint problem, producing a set of valid parameter values for s. These values are then used to instantiate the DSL into a concrete, executable program.

A key challenge of framing a synthesis problem as a CSP is that of scalability. While solvers have powerful built-in heuristics to efficiently prune and search the constrained search space, constructing and maintaining the symbolic formula over a large number of constraints constitute a significant overhead. For this reason, significant efforts were put into simplifying and re-writing the constraint formula for a compact representation ( Singh & Solar-Lezama (2016) ; Cadar et al. (2008) ). Without such optimizations, it is possible for a formula to exceed the computer's memory. If one wishes to apply program synthesis to a sufficiently large dataset, there needs to be a way to limit the number of examples expressed as constraints.

The standard procedure to limit the number of examples is counter example guided inductive synthesis, or CEGIS for short (Solar-Lezama et al. (2006) ). CEGIS solves the synthesis problem with two adversarial sub-routines, a synthesizer and a checker. The synthesizer solves the CSP with a subset of examples rather than the whole set, producing a candidate program. The checker takes the candidate program and produces an adversarial counter example that invalidates the candidate program. This adversarial example is then added to the subset of examples, prompting the synthesizer to improve. CEGIS successfully terminates when the checker fails to produce an adversarial example. By iteratively adding counter examples to the subset, CEGIS can drastically reduces the size of the constraint constructed by the synthesizer, making it scalable to large domains. The subset of examples are representative in a sense that, once a candidate program is found over this subset, it is also correct over all the examples. However, CEGIS has to repeatedly invoke the constraint solver in the synthesis sub-routine to construct the subset, solving a sequence of challenging CSP problems. Moreover, due to the phase transition Gent & Walsh (1994) property of SAT formulas, there may be instances in the sequence of CSP problems where there are enough constraints to make the problem non-trivial, but not enough constraints for the solver to properly prune the search space1 , causing the performance of CEGIS to become extremely volatile.

In this paper, we construct the representative subset in a different way. Rather than using the constraint solver as in CEGIS, we directly learn the relationships between the input-output examples with a neural network. Given a (potentially empty) subset of examples, the neural network computes the probability for other examples not in the subset, and grow the subset with the most "surprising" example (one with the smallest probability). The reason being if an input-output example has a low probability conditioned on the given subset, then it is the most constraining example that can maximally prune the search space once added. We greedily add examples until all the input-output examples in the dataset have a sufficiently high probability (no longer surprising). The resulting subset of examples is then given to the constraint solver. Experiments show that the trained neural network is capable of representing domain-specific relationships between the examples, and, while lacking the combinatorial precision of a constraint solver, can nonetheless finds subset of representative examples. Experiment shows that our approach constructs the sufficient subset at a much cheaper computational cost and shows improvement over CEGIS in both solution time and stability.

2. AN EXAMPLE SYNTHESIS PROBLEM:

To best illustrate the synthesis problem and the salient features of our approach, consider a diagram drawing DSL (Ellis et al., 2017) that allows a user to draw squares and lines. The DSL defines a draw(row, col) function, which maps a (row, col) pixel-coordinate to a boolean value indicating whether the specified pixel coordinate is contained within one of the shapes. By calling the draw function across a canvas, one obtains a rendering of the image where a pixel coordinate is colored white if it is contained in one of the shapes, and black otherwise. Figure 1 shows an example of a draw function and its generated rendering on a 32 by 32 pixel grid. The drawing DSL defines a set of parameters that allows the draw function to express different diagrams, some of which are underlined in Figure 1 (left). The synthesis problem is: Given a diagram rendered in pixels, discover the hidden parameter values in the draw function so that it can reproduce the same rendering. The synthesized drawing program is correct when its rendered image matches the target rendering exactly. Let Sdraw be the synthesized draw function and T arget be the target rendering:

correct(Sdraw) := ∀(row, col). Sdraw(row, col) = T arget[row][col]

Because of the many possible combinations of parameters for the program, this is a difficult combinatorial problem that requires the use of a constraint solver. Each of the pixel in the target render is encoded as an input-output pair ((row, col), bool), which can be used to generate a distinct constraint on all of the parameters. For the 32 by 32 pixel image, a total of 1024 distinct constraints are generated, which impose a significant encoding overhead for the constraint solver.

In this paper, we propose a algorithm that outputs a representative subset of input-output examples. This subset is small, which alleviates the expensive encoding overhead, yet remains representative of all the examples so that it is sufficient to constrain the parameter only on the subset. The algorithm constructs the representative subset iteratively. Starting with an empty subset, the algorithm uses a neural network model to compute the probability of all the examples conditioned on the chosen examples in the subset. It then adds to the subset the least probable example, the intuition being the example with the lowest probability would best restrict the space of possible solutions. The process stops when all the examples in the dataset are given a sufficiently high probability. In the context of the drawing DSL, the process stops when the neural network is sufficiently confident in its reconstruction of the target rendering given the chosen subset of pixels Figure 2 (middle). The rest of the paper elaborates the specifics of our approach.

3. EXAMPLES REDUCTION:

The crux of our algorithm is an example selection scheme, which takes in the set of examples and outputs a small subset of representative examples. Let D' ⊆ D be a subset of examples. Abusing notation, let us define the consistency constraint D'(s) := (xi,yi)∈D' F (x i ; s) = y i , that is to say, the parameter s is consistent with all examples in D'. We define the smallest sufficient subset as:

D * = argmin D'⊆D | D' | s.t. ∀s ∈ S. D'(s) ⇒ D(s).

D * is sufficient in a sense any parameter s satisfying the subset D * must also satisfy D. Finding the exact minimum sized D * is intractable in practice, thus we focus on finding a sufficient subset that is as close in size to D * as possible.

3.1. EXAMPLES REDUCTION WITH A COUNT ORACLE:

In this subsection we describe an approximate algorithm with a count oracle c, which counts the number of valid solutions to a subset of examples: c(D') := |{s ∈ S| D'(s)}|. This algorithm constructs the subset D' greedily, choosing the example that maximally restricts the solution space.

D' = {} while True do (x i , y i ) ← argmin xj ,yj c(D' ∪{(x j , y j )}) # selection criteria if c(D') = c(D' ∪{(x i , y i )}) then return: D' else D' ← D' ∪{(x i , y i )} end end

Algorithm 1: An example reducing algorithm with a count oracle Claim 1: Algorithm 1 produces a subset D' that is sufficient, i.e. ∀s D'(s) ⇒ D(s).

Proof 1: The termination condition for Algorithm 1 occurs when adding any example to D', the counts remain unchanged c(D') = c(D' ∪{(x, y)}), ∀(x, y) ∈ D. As D'(s) is defined as a conjunction of satisfying each example, c can only be monotonically decreasing with each additional example, as more solutions become invalidated: c(D') ≥ c(D' ∪{(x, y)}). At termination, equality occurs for every additional (x, y) ∈ D, where no more solutions are invalidated, thus we have the sufficiency condition ∀s. D'(s) ⇒ D(s).

Claim 2: Algorithm 1 produces a subset D' that is 1 -1 e optimal

Proof Gist: To show this, we need to show the count function c(D') is both monotonic and submodular (Nemhauser et al., 1978) . We have already shown monotonicity in the previous proof, for the sub-modularity proof see appendix.

To use Algorithm 1, one needs to solve the model counting problem (Gomes et al., 2008) for the count function c, which is impractical in practice. We now aim to resolve this issue by adopting an alternative selection criteria.

3.2. EXAMPLE SELECTION WITHOUT THE COUNT ORACLE:

The selection criteria in Algorithm 1 uses the count oracle c, which is impractical to compute in practice, in this sub-section, we develop an alternative selection criteria that can be approximated efficiently with a neural network. Let D' = {(x (1) , y (1) ) . . . (x (r) , y (r) )} where (x (j) , y (j) ) denotes the j th input-output example to be added to D'. We define the selection probability: 

3.3. APPROXIMATING SELECTION PROBABILITY WITH A NEURAL NETWORK:

We now describe how to model P r((x, y)| D') with a neural network. For the scope of this work, we assume there exists an uniform sampler s ∼ unif (S) for the possible parameters, and that the space of possible input and output values are finite and enumerable dom(x) = ẋ1 . . . ẋN , dom(y) = ẏ1 . . . ẏM . We will first describe a count-based approach to approximate P r((x, y)| D'), then describe how to model it with a neural network to achieve generalization properties.

For the count-based approximation, we sample a subset of input values X = {x (1) , . . . , x (r) }, and a particular input value x / ∈ X . We sample a parameter s ∈ S and evaluate the parameterized function, F (• ; s), on each of the input in X , obtaining output values F (x (1) ; s) = y (1) , . . . , F (x (r) ; s) = y (r) , we also evaluate the function on x, obtaining F (x; s) = y. Let ĉ denote the empirical count, we have, after sufficient number of samples: P r((x, y)| D') ≈ ĉ(F (x (1) ; s) = y (1) , . . . , F (x (r) ; s) = y (r) , F (x; s) = y) ĉ(F (x (1) ; s) = y (1) , . . . , F (x (r) ; s) = y (r) ) .

The issue with the count-based approach is that we need sufficient samples for any subset of inputs, with a total number of 2 N subsets where N = |dom(x)|. Therefore, we approximate P r((x, y)| D') with a neural network. (i) , F (x (i) ; s))|x (i) ∈ X }, the rest (where x / ∈ X ) are encoded as unknowns. This is similar to a data completion task in Boltzmann machines (Ackley et al., 1985) , with the difference that we directly compute the completion process rather than performing a gradient search for the most probable completion configuration.

Y i = F (x i , s) if x i ∈ X M + 1 otherwise Y i = F (x i , s)

During use time, given a subset of input-output examples D' = {(x (1) , y (1) ) . . . (x (r) , y (r) )}, we set for each x (i) its corresponding input neuron with value y (i) , and set the value unknown for neurons whose corresponding input values that do not occur in D'. The neural network then computes the softmax values for all the M classes in all the output neurons, obtaining P r((x, y)| D') for every possible input-output examples simultaneously.

3.4. TYING UP THE LOOSE ENDS WITH CEGIS:

In the previous subsections we described an examples reduction algorithm that builds the sufficient subset one example at a time by greedily selecting the lease likely input-output example given the examples in the subset. We also showed how one can approximate the selection probability P r((x, y)| D') by training an auto-encoder like neural network. The remaining problem lies in the approximate nature of the neural network: It cannot perfectly model the probability P r((x, y)| D'), and thus we need to use a different termination condition for our example reduction algorithm. Rather than terminating the algorithm when min (x,y) P r((x, y)| D') = 1, we adopt a weaker termination condition mean (x,y) P r((x, y)| D') ≥ β, terminating when the average probability of all the examples are greater than a certain threshold β.

By approximating the selection probability and relaxing the termination condition, one can no longer guarantee that the subset produced by our reduction algorithm is sufficient. That is to say, there may be solutions s which satisfies the subset D' yet fails to satisfy the entire set of examples D. We can remedy this problem by leveraging CEGIS, which guarantees a solution s that is correct on all the examples in D.

Like Algorithm 1, CEGIS also maintains a subset of examples D' and grows it one at a time. The difference being the selection criteria and termination condition. In CEGIS, two subroutines, synthesize and check, interacts in an adversarial manner to select the next example to add to the subset: The routine synthesize uses a constraint solver to produce a candidate parameter s that satisfies the current D'; The routine check checks the candidate s against all the examples in D, and finds a counter example (x counter , y counter ) that invalidates the candidate s. This counter example is added to D', prompting the synthesizer to improve its solution. CEGIS terminates when no counter example can be found. Clearly, when CEGIS terminates, the resulting solution s is correct on all the examples in D. By using a constraint solver in the synthesis step, and using the checker that checks against all the examples, CEGIS guarantees pruning of the solution space with each counter-example it adds to

D' = {} while True do s = synthesize(S, D') (x counter , y counter ) = check(s, D) if (x counter , y counter ) == None then return: D' else D' = D' ∪{(x counter , y counter )} end end

Algorithm 2: CEGIS the subset. The main drawback of CEGIS is that it requires repeated calls to the constraint solver in the synthesis step and no guarantees on how well the additional counter-example prunes the search space other than it invalidates the current candidate solution s.

Our synthesis algorithm combines the example selections and CEGIS. First, example selection is run until the mean selection probability reaches a certain threshold β, then the resulting set of sampled examples are given to CEGIS as the starting set of counter examples. CEGIS then repeatedly calls the constraint solver for candidate solutions, and checking each candidate solution against the entire example set D until a correct solution is found: 

# phase 1: examples selection D' = {} while mean (x,y)∈D P r((x, y)| D') ≤ β do (x, y) ← argmin x ,y P r((x , y )| D') # selection criteria D' ← D' ∪{(x i , y i )} end #

4. EXPERIMENTS:

We perform a set of experiments measuring the overall speed and stability of our synthesis algorithm, and the representativeness of the subset of examples produced by the selection process. We evaluate our algorithm against 400 randomly generated images. For the experiment, the drawing function contains parameters that can generate a total of 1.31 × 10 23 possible programs. For each randomly generated image, the following synthesis algorithms are run:

• full: all 1024 examples are added to the subset, solved once

• rand: 10% of all examples are added to the subset, solved once

• nn: the subset generated by our selection algorithm, solved once

• CEGIS: the CEGIS algorithm where the check function return counterexamples in order

• rCEGIS: the CEGIS algorithm where the check function return counterexamples at random

• rand+CEGIS: initialize CEGIS with a random subset of 10% examples

• ours: our synthesis algorithm described in Algorithm 3, initializing CEGIS with the subset produced by the selection algorithm Figure 4 shows the average time breakdown, the median and variance, and the number of examples selected for the different algorithms. Here, rand and nn are excluded because they are not guaranteed to synthesize a program that can perfectly reproduce the target render. On average, rand synthesizes a program that misses 10.1% of the pixels while nn misses 1.2%. For the average time plot in Figure 4 (top left), we measure the breakdown for the different kinds of times: grey denotes the overhead time in constructing the constraints, slanted-stripes denotes the solving time, and vertical stripes denotes the time taken by the example selection algorithm. On average, our algorithm finishes the fastest, with cegis a close second. We remark that we achieve a similar solve time as the full algorithm, indicating the subset returned by our algorithm constrained the solver to a similar degree as constraining all the examples at once. In comparison, all the other algorithms have significantly longer solving time and shorter building time, indicating that these algorithms tend to under-constrain the synthesis problem, making it more difficult to solve. The drawback of our approach is the time it takes to produce the representative subset, which is around 6 seconds. This constitute as another form of overhead cost, but as we can see compared to the overhead cost of constructing the constraint, it is justified.

For the median and variance plot in Figure 4 (top right) for average over-all time, we note cegis comes in first for smallest median time, while our algorithm is second place. However, we remark that our algorithm has a much smaller variance in over-all time, achieving higher stability than cegis. One salient feature of this plot is that although cegis and rcegis only differs by which counterexample is added to the subset (the "first" one versus a random one), this small difference results in a huge difference in the over-all time performance. We postulate that cegis is able to leverage the particular ordering of choosing the counter-examples are top-left to bottom-right, which tend to produce representative examples in the drawing DSL domain we have considered. By removing this particular ordering of choosing counter-examples, rcegis incurs a significant increase in solving time.

For the number of examples plot in Figure 4 (bottom), we measure the average number of examples in the selected subset. For this plot, solid grey measures the size of the initial subset of examples, and stripped measures additional examples chosen by the cegis algorithm. We note that rcegis on average was able to solve the synthesis problem with the least number of examples. However, rcegis also performs the worst in term of over-all solving time, suggesting that while it is possible to generate a valid solution from a small subset of examples, it is likely the case where that subset is not sufficiently constraining so the solver cannot efficiently prune the search space. By comparison, both cegis and our approach, the top two performing algorithms in overall-time, selects many more examples for the representative subset. We note that although rand+cegis selects roughly 70% of the examples as our approach, the subset it selected are not representative. This is evident in the high over-all solving time for rand+cegis, especially in solving time, indicating the examples it selected are not constraining the solver in a helpful way. By contrast, the subset selected by our selection algorithm is almost perfect, with only 1.5 additional counter-examples needed from CEGIS to arrive at a correct solution that matches all the pixels.

Overall, our algorithm provides a quick and stable solution over existing algorithms, and the subset that it provides is small and representative of the whole subset.

5. RELATED WORKS:

In recent years there have been an increased interest in program induction. Graves et al. (2014) , Reed & De Freitas (2015) , Neelakantan et al. (2015) assume a differentiable programming model and learn the operations of the program end-to-end using gradient descent. In contrast, in our work we assume a non-differentiable programming model, allowing us to use expressive program constructs without having to define their differentiable counter parts. Works such as (Reed & De Freitas, 2015) and (Cai et al., 2017) assume strong supervision in the form of complete execution traces, specifying a sequence of exact instructions to execute, while in our work we only assume labeled input-output pairs to the program, without any trace information. Parisotto et al. (2016) and Balog et al. (2016) learn relationships between the input-output examples and the syntactic structures of the program that generated these examples. When given a set of input-outputs, these approach use the learned relationships to prune the search space by restricting the syntactic forms of the candidate programs. In these approaches, the learned relationship is across the semantic domain (input-output) and the syntactic domain. In contrast, in our approach we learn a relationship between the input-output examples, a relationship entirely in the semantic domain. In this sense, these approaches are complimentary.

:

Imagine a mostly empty Sudoku puzzle, the first few numbers and the last few numbers are easy to fill, whereas the intermediate set of numbers are the most challenging

Figures and Tables:

Figure 1: Sketch of code to draw an image (left) and the generated image (right). Boxes are drawn around the many adjustable parameters in the code such as the number of iterations and offsets for the shapes.

Figure 2 (left) shows the selected subset of examples: white and black pixels indicate chosen examples, grey pixels indicate unchosen ones. As we can see, from a total of 1024 examples, only 15% are selected for the representative subset. The representative subset is then given to the constraint solver, recovering the hidden parameter values in Figure 2 (right).

Figure 2: The selected subset of pixel examples (left). The neural network's estimation of the image (middle). The recovered parameters from running the solver on the selected subset (right).

P r((x, y)| D') := P r(F (x; s) = y| D'(s))Note that P r((x, y)| D') is not a joint distribution on the input-output pair (x, y), but rather the probability for the event where the parameterized function F (• ; s) maps the input x to y, conditioned on the event where F (• ; s) is consistent with all the input-output examples in D'. We will now show that one can use P r((x, y)| D') as the selection criteria rather than the count oracle in Algorithm 1.Claim: Under a uniform distribution of parameters s ∼ unif (See appendix.To use argmin (x,y) P r((x, y)| D') as a selection criteria to grow the subset D', one needs a corresponding termination condition. It is easy to see the right termination condition should be min (x,y) P r((x, y)| D') = 1: when all the input-output examples are completely determined given D', the subset is sufficient.

Figure 3: Our neural network architecture resembles a feed-forward auto-encoder with explicitly enumerated input and output neurons

Figure 4: The average time taken for each step of the algorithm (upper left). The spread of total time taken for each algorithm (upper right). The number of examples used in each algorithm (bottom).

The neural network is set-up similarly to a feed-forward auto-encoder with N input neurons Y 1 . . . Y N and N output neurons Y' 1 . . . Y' N . That is to say, we enumerate over (the finite set of) distinct input values ẋ1 . . . ẋN , creating a corresponding input and output neuron each time. Each input neuron Y i can take on 1 + M different values where M = |dom(y)|, and each output neuron Y' i can take on M different values, both assume a 1-hot encoding. In this encoding, each input neuron Y i and output neuron Y' i can represent the value of running function F (• ; s) on the corresponding input value ẋi , F ( ẋi ; s). The value F ( ẋi ; s) ∈ dom(y) is represented as a distinct class in 1 . . . M . Input neuron Y i can also represent an additional class, M + 1, representing the unknown value. Figure blah shows our neural network architecture, note that we do not suggest a specific neural network architecture for the middle layers, one should select whichever architecture

Table content: <table/>

Synthesis with example selectionsBy initializing CEGIS with a set of representative examples, CEGIS will be able to find the correct solution with fewer calls to the constraint solver, saving both overhead time and solving time.

Table content: <table><tr><td>phase 2: CEGIS</td></tr><tr><td>while True do</td></tr><tr><td>s = synthesize(S, D')</td></tr><tr><td>(x counter , y counter ) = check(s, D)</td></tr><tr><td>if (x counter , y counter ) == None then return: s</td></tr><tr><td>else</td></tr><tr><td>D' = D' ∪{(x counter , y counter )}</td></tr><tr><td>end</td></tr><tr><td>end</td></tr><tr><td>Algorithm 3:</td></tr></table>

Peer review (iclr2018):
 The paper proposes a method for identifying representative examples for program synthesis to increase the scalability of existing constraint programming solutions. The authors present their approach and evaluate it empirically. The proposed approach is interesting, but I feel that the experimental section does not serve to show its merits for several reasons. First, it does not demonstrate increased scalability. Only 1024 examples are considered, which is by no means large. Even then, the authors approach selects the highest number of examples (figure 4). CEGIS both selects fewer examples and has a shorter median time for complete synthesis. Intuitively, the authors* method should scale better, but they fail to show this -- a missed opportunity to make the paper much more compelling. This is especially true as a more challenging benchmark could be created very easily by simply scaling up the image. Second, there is no analysis of the representativeness of the found sets of constraints. Given that the results are very close to other approaches, it remains unclear whether they are simply due to random variations, or whether the proposed approach actually achieves a non-random improvement. In addition to my concerns about the experimental evaluation, I have concerns about the general approach. It is unclear to me that machine learning is the best approach for modeling and solving this problem. In particular, the selection probability of any particular example could be estimated through a heuristic, for example by simply counting the number of neighbouring examples that have a different color, weighted by whether they are in the set of examples already, to assess its "borderness", with high values being more important to achieve a good program. The border pixels are probably sufficient to learn the program perfectly, and in fact this may be exactly what the neural net is learning. The above heuristic is obviously specific to the domain, but similar heuristics could be easily constructed for other domains. I feel that this is something the authors should at least compare to in the empirical evaluation. Another concern is that the authors* approach assumes that all parameters have the same effect. Even for the example the authors give in section 2, it is unclear that this would be true. The text says that rand+cegis selects 70% of examples of the proposed approach, but figure 4 seems to suggest that the numbers are very close -- is this initial examples only? Overall the paper appears rushed -- the acknowledgements section is left over from the template and there is a reference to figure "blah". There are typos and grammatical mistakes throughout the paper. The reference to "Model counting" is incomplete. In summary, I feel that the paper cannot be accepted in its current form.