论文标题

公制程序综合

Metric Program Synthesis

论文作者

Feser, John, Dillig, Isil, Solar-Lezama, Armando

论文摘要

我们提出了一种新的域 - 不合Snostic合成技术,用于从输入输出示例中生成程序。我们的方法称为公制程序综合,放宽了众所周知的观察等效思想(在自下而上的枚举合成中广泛使用),以较弱的观察性相似性概念,目的是减少合成器需要探索的搜索空间。我们的方法基于距离度量标准将程序群集成等效类,并构造一个版本空间,该版本空间紧凑地表示“近似正确”的程序。然后,给定一个从此版本空间采样的“足够接近”程序,我们的方法使用距离引导的维修算法来找到与给定输入输出示例完全匹配的程序。我们已经在称为Symetric的工具中实现了建议的公制程序合成技术,并在先前工作中考虑的三个不同领域中进行了评估。我们的评估表明,Symetric的表现优于使用观察等效性的其他域 - 不合稳定合成器,并且它与在这些域上设计或训练的域特异性合成器具有竞争性的结果。

We present a new domain-agnostic synthesis technique for generating programs from input-output examples. Our method, called metric program synthesis, relaxes the well-known 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 a 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.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源