Summary

Summary

• Enumerative strategy from [2] worked well, but does not scale
• input points + full specification are different
• counter-examples set is added to input points using full specification when a “correct” example (on input points) is found to be wrong
• EUsolver –> divide and conquer
  • solution is large, but individual parts are important
  • individual parts: terms + predicates (conditionals)
  • combine terms and predicates into the solution
• use learning decision trees [4, 18] to combine different parts of conditionals
  • input points of the conditional are samples
  • predicates are the attributes
  • terms are labels
  • a term is a valid label for a point if the term is correct on the point.

    for each point, following the edges corresponding to attribute values leads to a label which is correct for the point.

• tries to find more compact solutions
• eusolver requires a “conditional expression grammar”
  • conditional expression grammar is a pair of grammars \(G_T, P_T\)
  • \(G_T\) is the term grammar, \(G_P\) is the predicate grammar
• Decision Trees
  • model conditional expressions
  • traditional DT maps samples to labels
  • internal node of a DT has attributes which hold or not a sample.
  • each leaf contains a label

Summary

The paper introduces SyGuS problems and the traditional enumerative approach to solving the problems. One of the disadvantages of traditional enumerative solvers is the amount of time they take to find to find a result, and the fact that the expressions they generate are complex. The authors introduce a “divide-and-conquer” approach which can solve problems much faster than other SyGuS solvers by using simple solution and conditional grammars.

The EUSolver approach utilizes grammars that have conditional expressions. These conditional expressions allow the solution to have subexpressions with particular input points. The subexpressions tend to be simpler and smaller underneath each conditional statement, rather than if they were combined into one large expression. This means for the given set of input points we need to possibly only generate some small number of subexpressions which cover the input points, and then a tree of conditional statements with the expressions that cover the set of inputs.

Questions

• What are the restrictions that prevent EUSolver from solving “not plainly separable” problems?
• how expensive are the generated programs versus with EUSolver versus an expression generated by a simple enumerative algorithm?

Strengths

• Does a good job of introducing problem backgrounds and comparing to the “naive” way
• based on performance in the SyGuS competition, clearly able to outperform many other solvers in terms of how many solutions

Weaknesses

• discounts whole class of problems – “not plainly separable” (p.6)
• I feel the discussion of conditional grammars is too concise. The entire algorithm hinges on the availability of a conditional grammar but not much time is spent talking about how they are generated (automatically or not. This could be due to my lack of knowledge though.

Questions

• What does EUSolver use as behavioral constraints? Structural constraint? Search strategy?

Behavioral constraints - SyGuS specification \(\phi\) - conditional expression grammars Structural Constraints - needs a conditional grammars can be built from traditional SyGuS grammar Search Strategy - divide an conquer with decision trees terms+predicates - top-down approach

• What are the main two pruning/decomposition techniques EUSolver uses to speed up the search? What enables these techniques?
  • instead of trying to find a single expression that is correct for all terms, it maintains a set of candidate terms which are correct for a set of input points, so then one large expression from the non-conditional grammar doesn’t need to be found
  • To compute decision trees they use a heuristic to determine whether a predicate will result in an information gain by the decision tree. This helps choose predicates with a larger probability of moving towards a successful solution
  • the conditional grammars enable both of these techniques

• What would a naive alternative to decision tree learning be for synthesizing branch conditions? What are the disadvantages of this alternative?

  • you could have a map of input points to generated output expressions which generate the correct result. The problem is that for anything more than a simple function, the amount of generated expressions stored could be massive. The decision tree compresses the learned knowledge.