paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Maximal multi-layer specification synthesis

最大化多层规约合成
FSE Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2019匹配度 3/10 · 论文研究程序合成,结合Max-SMT与LSTM,属于PL与ML交叉,但与用户核心关注的静态分析、Agentic程序、浮点分析、贝叶斯程序分析均无直接关联;且所用机器学习模型为LSTM而非当前LLM/Agent,未建立在强模型之上。引用 31 inbox
Yanju Chen, Ruben Martins, Yu Feng
crossref: 2026-09-12

AI 速览

一句话:MARS 将输入输出样例、文本描述和部分代码构成的多层规约归约为 Max-SMT,并用 LSTM 与关联规则学习用户意图。

基于输入输出样例的合成常因样例不完备而生成符合样例却不符合用户意图的程序。本文提出 MARS,其规约由输入输出样例、文本描述和部分代码片段共同组成。为从含噪且歧义的描述中捕获用户意图,作者提出结合 LSTM 序列到序列模型与 apriori 关联规则挖掘的混合模型。进而将多层规约合成归约为 Max-SMT:硬约束编码良类型具体程序,软约束编码学到的用户意图。论文在数据整理领域实例化,并与 Morpheus 对比。实验表明,MARS 在运行时间和求解基准上优于 Morpheus;在困难基准上,候选排序好一个数量级,运行速度快 15 倍。

问题
基于输入输出样例的程序合成因样例不完备,可能生成通过样例但不符合用户意图的程序。
方法
提出 MARS,融合输入输出样例、文本描述与部分代码片段,用 LSTM 和 apriori 混合模型学习用户意图,并归约为 Max-SMT 求解。
评估
在数据整理任务上与 Morpheus 对比;运行时间与求解基准更优,困难基准上候选排序质量提升一个数量级且快 15 倍。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot5087,
  title = {Maximal multi-layer specification synthesis},
  author = {Yanju Chen and Ruben Martins and Yu Feng},
  booktitle = {FSE},
  year = {2019},
  doi = {10.1145/3338906.3338951}
}