paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Inductive Program Synthesis Guided by Observational Program Similarity

由观测程序相似性引导的归纳程序合成
OOPSLA 7(OOPSLA2)2023匹配度 2/10 · 该论文属于归纳程序合成,核心是将观测等价松弛为观测相似并用于缩小搜索空间,与用户关注的静态分析、浮点/贝叶斯程序分析以及 LLM/Agent 与程序分析的交叉均无直接关联;仅在广义程序语言方法层面有较弱相关性。引用 6 inbox
Jack Feser, Işıl Dillig, Armando Solar-Lezama
crossref: 2026-09-10

AI 速览

一句话:提出度量程序合成,将观测等价松弛为观测相似,用距离度量聚类程序并经修复缩小搜索空间。

归纳程序合成常通过自底向上枚举搜索来生成满足输入输出示例的程序,而现有方法多依赖观测等价,导致搜索空间庞大。本文提出度量程序合成(metric program synthesis),将观测等价松弛为更弱的观测相似概念:基于专家提供的距离度量将程序聚类为等价类,并构建紧凑表示“近似正确”程序的版本空间;随后从该空间采样“足够接近”的程序,再用距离引导的修复算法找到精确匹配示例的程序。作者实现了工具 SyMetric,并在先前工作涉及的三个领域上评估。实验表明,SyMetric 优于使用观测等价的领域无关合成器,且能与针对这些领域专门设计或训练的领域专用合成器取得相当的结果。

问题
如何在自底向上枚举式的归纳程序合成中,减少因严格观测等价而导致的巨大搜索空间。
方法
将观测等价松弛为观测相似,基于专家距离度量对程序聚类并构建版本空间,从空间采样近似正确程序后,通过距离引导的修复算法得到精确满足输入输出示例的程序。
评估
实现 SyMetric,在先前工作使用的三个不同领域上进行评估,并与领域无关及领域专用合成器比较。
原文摘要(Abstract)

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.

链接与引用

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

BibTeX
@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}
}