Optimal Neural Program Synthesis from Multimodal Specifications (2021)

Abstract: Multimodal program synthesis, which leverages different types of user input to synthesize a desired program, is an attractive way to scale program synthesis to challenging settings; however, it requires integrating noisy signals from the user, like natural language, with hard constraints on the program’s behavior. This paper proposes an optimal neural synthesis approach where the goal is to find a program that satisfies user-provided constraints while also maximizing the program’s score with respect to a neural model. Specifically, we focus on multimodal synthesis tasks in which the user intent is expressed using a combination of natural language (NL) and input-output examples. At the core of our method is a top-down recurrent neural model that places distributions over abstract syntax trees conditioned on the NL input. This model not only allows for efficient search over the space of syntactically valid programs, but it allows us to leverage automated program analysis techniques for pruning the search space based on infeasibility of partial programs with respect to the user’s constraints. The experimental results on a multimodal synthesis dataset (StructuredRegex) show that our method substantially outperforms prior state-of-the-art techniques in terms of accuracy and efficiency, and finds model-optimal programs more frequently.

## introduction in recent years, there has been a revolution in machine learning-based program synthesis techniques for automatically generating programs from high-level expressions of user intent, such as inputoutput examples @xcite @xcite @xcite and natural language (yaghmazadeh et al., 2017; dong and lapata, 2016; rabinovich et al., 2017; yin and neu-1 code available: https://github.com/xiye17/opsynth strings of letters and digits tree-based model program analyzer score partial programs based on nl description prune partial programs based on i/o examples natural language i/o examples optimal program cat(rep(<let>,1+),rep(<num>,1+)) a01 + abc -top-down ordered search ⨉ □ 1.0 cat(□,□) .20 and(□,□) and(<let>,□) ... figure 1 : the framework of our multi-modal optimal synthesis approach. a tree-structured model scores partial programs based on the nl description and a program analyzer prunes the search space based on the i/o examples. our algorithm searches in a best-first fashion following the scores, and hence ensures the optimality of the output program with respect to the model. the core contribution of this paper is to formulate multimodal synthesis as an optimal synthesis task and propose an optimal synthesis algorithm to solve it. the goal of optimal synthesis is to generate a program that satisfies any hard constraints provided by the user while also maximizing the score under a learned neural network model that captures noisy information, like that from natural language. in practice, there are many programs that satisfy the hard constraints, so this maximization is crucial to finding the user's intended program: if our neural model is well-calibrated, a program that maximizes the score under the neural model is more likely to be what the user wants. in our setting (figure 1 ), we train a neural model to take natural language input that can be used to guide the search for a program consistent with user-provided examples. because our search procedure enumerates programs according to their score (values in blue in figure 1 ), the first enumerated program satisfying the examples is guaranteed to be optimal according to the model. a central feature of our approach is the use of a tree-structured neural model, namely the abstract syntax network (asn) @xcite , for constructing syntactically valid programs in a top-down manner. the structure of the asn model restricts search to programs that are syntactically correct, thereby avoiding the need to deal with program syntax errors @xcite , and it allows us to search over programs in a flexible way, without constraining a left-to-right generation order like seq2seq models do. more importantly, the use of top-down search allows us to more effectively leverage automated program analysis techniques for proving infeasibility of partial asts. as a result, our synthesizer can prune the search space more aggressively than prior work and significantly speed up search. while our network structure and pruning techique are adapted from prior work, we combine them and generalize them to this optimal neural synthesis setting in a new way, and we show that our general approach leads to substantial improvements over previous synthesis methods. we implement our method in a synthesizer called opsynth and evaluate it on the challenging structuredregex dataset @xcite for synthesizing regular expressions from linguistically diverse natural language descriptions and positive/negative examples. we compare our approach against a range of techniques from prior work and ablations of our own method. opsynth achieves substantial gain over past work by solving 60.8% (resp. 48.8%) of the programs of test (resp. test-e) set in structuredregex. these results represent a roughly 7-10% improvement over prior work with a roughly 3× speedup due to the improved pruning. ## problem formulation context-free grammar. in this work, we assume that the syntax of the target programming language l is specified as a context-free grammar @xmath0, σ, r, s 0 ) where v is a set of nonterminals, σ is the set of terminal symbols, r is a set of productions, and s 0 is the start symbol. we use the notation s to denote any symbol in v ∪ σ. the grammar in figure 2 has two nonterminals (s 0 and v 1 ) and three terminals (cat, <0>, @xmath1. to simplify presentation in the rest of the paper, we assume that each grammar production is of the form @xmath2, . . . , s n ) where f is a language construct (e.g., a constant like 0 or a built-in function/operator like cat, +, etc.). we represent programs in terms of their abstract syntax trees (ast). we assume that every node n in the tree is labeled with a grammar symbol s (denoted s(n)) and a production r (denoted r(n)) that indicates the cfg production that was used to assign the terminal symbol for that node (if applicable). figure 3 shows an ast representation of the program cat(cat(<0>, <1>), <0>) generated using the simple grammar shown in figure 2 . similar ast representations have been used in recent work on grammar-based program generation models @xcite @xcite . ## experimental setup we evaluate our synthesizer on the english struc-turedregex dataset for multimodal synthesis of regular expressions. this dataset contains 3520 labeled examples, including an nl description, positive/negative examples, and the target regex. we choose this dataset for our evaluation because (1) it is only the dataset containing both examples and nl where the nl description is written by humans, and (2) this dataset is quite challenging, with existing techniques achieving under 50% accuracy. implementation details as stated in section 3.1, our model is an abstract syntax network tailored to fit the regex dsl used in struc-turedregex. we train our neural model to maximize the log likelihood of generating ground truth regexes given the nl using the adam optimizer @xcite , stopping when the performance on dev set converges. more details are in the appendix. we implement the infeasibility checking procedure for our regex dsl by encoding the semantics of each operator in the theory of strings @xcite . since all existentially quantified variables in the resulting formula can be eliminated through substitution, the resulting constraints are of the form @xmath3. thus, we can check the satisfiability of these formulas using the bricks library @xcite . the appendix describes both the semantics of the dsl constructs as well as the rules used to generate the encoding a partial program, because of our infeasibility check, the order of expanding non-terminals can impact the efficiency of our search, as we want to prune any infeasible partial programs when they are less concrete. we experimented with several methods of selecting a leaf node to expand, including pre-order traversal, choosing high-level nodes first, and choosing lowest-entropy nodes first. pre-order traversal seemed to work best; details about the expansion order can be found in the supplementary. baselines we compare our method against three programming-by-example (pbe-only) baselines, alpharegex @xcite , deepcoder @xcite , and robustfill @xcite . alpharegex is an enumerative regex synthesizer that uses breadth-first search to find regexes that are consistent with the examples. both deepcoder and robustfill are neural program synthesis approaches. deepcoder places a distribution over constructs and terminals based on examples, and uses this distribution to carry out dfs search, whereas robustfill uses beam search to autoregressively build programs. we further compare our method against prior multimodal program synthesis techniques, sketch @xcite and treesearch @xcite against sketchadapt @xcite because it relies on the assumption that every program consistent with examples is the gold program, which does not hold in our setting. we also consider two nl-to-code models, seq2seq and tranx @xcite , which we modify to filter out partial programs that are inconsistent with the examples. specifically, we adapt these baselines in a similar way as proposed in @xcite by filtering the beam at every timestep during search. implementation details of all our baselines are in the appendix. we refer to our optimal synthesis approach as opsynth. we also show ablations: asn +p (asn with our pruning during beam search), and opsynth -p to further demonstrate the benefits of our approach over models like @xcite that do not use such pruning. finally, we also consider an extension denoted as opsynth +r , which extends opsynth with the attention a model from robustfill @xcite , which encodes the examples φ using another set of lstm layers. to combine these signals, we define the probability of applying rule r on n as: ## results and analysis in the following experiments, we evaluate our approach based on two criteria: (1) accuracy, measured by the fraction of solved synthesis tasks, and (2) efficiency, measured by the number of partial programs searched and the run time. ## conclusion in this paper, we presented a technique for optimal synthesis from multimodal specifications. on a benchmark of complex regex synthesis problems, we showed that this approach is substantially more accurate than past models, and our synthesis algorithm finds the model-optimal program more frequently compared to beam search. while we have evaluated this method on regular expressions, our technique is general and can be applied to other classic pbe domains on which powerful abstract interpretation techniques for feasibility checking are available, such as table transformations @xcite , tensor and string manipulations @xcite , and other data wrangling @xcite . our technique, especially the notion of optimality with respect to a model, can also be valuable for more general program synthesis @xcite if pruning techniques can be developed for the particular tasks to be performed. in particular, @xcite note that large language models are not good at modeling execution semantics of programs; we see our execution-guided pruning techniques as a path forward in this domain.