一句话:提出度量程序合成,将观测等价松弛为观测相似,用距离度量聚类程序并经修复缩小搜索空间。
归纳程序合成常通过自底向上枚举搜索来生成满足输入输出示例的程序,而现有方法多依赖观测等价,导致搜索空间庞大。本文提出度量程序合成(metric program synthesis),将观测等价松弛为更弱的观测相似概念:基于专家提供的距离度量将程序聚类为等价类,并构建紧凑表示“近似正确”程序的版本空间;随后从该空间采样“足够接近”的程序,再用距离引导的修复算法找到精确匹配示例的程序。作者实现了工具 SyMetric,并在先前工作涉及的三个领域上评估。实验表明,SyMetric 优于使用观测等价的领域无关合成器,且能与针对这些领域专门设计或训练的领域专用合成器取得相当的结果。
We present a new general-purpose synthesis technique for generating programs from input-output examples. Our method, called metric program synthesis, relaxes the observational equivalence idea (used widely in bottom-up enumerative synthesis) into a weaker notion of observational similarity, with the goal of reducing the search space that the synthesizer needs to explore. Our method clusters programs into equivalence classes based on an expert-provided distance metric and constructs a version space that compactly represents “approximately correct” programs. Then, given a “close enough” program sampled from this version space, our approach uses a distance-guided repair algorithm to find a program that exactly matches the given input-output examples. We have implemented our proposed metric program synthesis technique in a tool called SyMetric and evaluate it in three different domains considered in prior work. Our evaluation shows that SyMetric outperforms other domain-agnostic synthesizers that use observational equivalence and that it achieves results competitive with domain-specific synthesizers that are either designed for or trained on those domains.
@article{paperbot1899,
title = {Inductive Program Synthesis Guided by Observational Program Similarity},
author = {Jack Feser and Işıl Dillig and Armando Solar-Lezama},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622830}
}