一句话:MARS 将输入输出样例、文本描述和部分代码构成的多层规约归约为 Max-SMT,并用 LSTM 与关联规则学习用户意图。
基于输入输出样例的合成常因样例不完备而生成符合样例却不符合用户意图的程序。本文提出 MARS,其规约由输入输出样例、文本描述和部分代码片段共同组成。为从含噪且歧义的描述中捕获用户意图,作者提出结合 LSTM 序列到序列模型与 apriori 关联规则挖掘的混合模型。进而将多层规约合成归约为 Max-SMT:硬约束编码良类型具体程序,软约束编码学到的用户意图。论文在数据整理领域实例化,并与 Morpheus 对比。实验表明,MARS 在运行时间和求解基准上优于 Morpheus;在困难基准上,候选排序好一个数量级,运行速度快 15 倍。
There has been a significant interest in applying programming-by-example to automate repetitive and tedious tasks. However, due to the incomplete nature of input-output examples, a synthesizer may generate programs that pass the examples but do not match the user intent. In this paper, we propose MARS, a novel synthesis framework that takes as input a multi-layer specification composed by input-output examples, textual description, and partial code snippets that capture the user intent. To accurately capture the user intent from the noisy and ambiguous description, we propose a hybrid model that combines the power of an LSTM-based sequence-to-sequence model with the apriori algorithm for mining association rules through unsupervised learning. We reduce the problem of solving a multi-layer specification synthesis to a Max-SMT problem, where hard constraints encode well-typed concrete programs and soft constraints encode the user intent learned by the hybrid model. We instantiate our hybrid model to the data wrangling domain and compare its performance against Morpheus, a state-of-the-art synthesizer for data wrangling tasks. Our experiments demonstrate that our approach outperforms MORPHEUS in terms of running time and solved benchmarks. For challenging benchmarks, our approach can suggest candidates with rankings that are an order of magnitude better than MORPHEUS which leads to running times that are 15x faster than MORPHEUS.