paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling

通过元分析引导的洞填充进行归纳程序合成
POPL 10(POPL)2026匹配度 3/10 · 论文核心是用抽象解释元分析指导归纳程序合成中的洞填充顺序,属于传统程序综合与抽象解释的交叉,涉及的抽象解释技术虽与用户关注的静态分析沾边,但既未涉及 LLM/Agent,也并非对浮点或贝叶斯程序分析的交叉研究,方向与用户画像的几个核心问题仅弱相关。引用 0 inbox
Doyoon Lee, Woosuk Lee, Kwangkeun Yi
crossref: 2026-09-10

AI 速览

一句话:提出用抽象解释元分析预测最佳洞填充顺序,以提升归纳程序合成中自上而下搜索效率。

归纳程序合成常从含洞的不完整程序出发进行自上而下搜索,并用抽象化剪枝缩小空间;但洞的填充顺序会显著影响效率,却少有研究。本文提出一种元分析引导的洞填充策略:对底层抽象解释器的剪枝行为进行过近似,据此预测下一个最值得填充的洞,从而更早剪除不可行候选。作者将该方法实例化到位向量和字符串域,并在已有基准(含 SyGuS)上评估,表明借助抽象解释技术,其效率显著优于现有最先进方法。

问题
在自上而下归纳程序合成中,洞填充顺序对抽象剪枝效果和搜索效率影响巨大,但现有方法大多未系统处理该选择。
方法
提出元分析引导的洞填充策略,对用于剪枝的底层抽象解释器行为进行过近似,以预测并优先填充最有希望的洞;在位向量和字符串域实现。
评估
在先前工作基准(包括 SyGuS)上与最先进方法比较,显示效率显著提升。
原文摘要(Abstract)

A popular approach to inductive program synthesis is to construct a target program via top-down search, starting from an incomplete program with holes and gradually filling these holes until a solution is found. During the search, abstraction-based pruning is used to eliminate infeasible candidate programs, significantly reducing the search space. Because of this pruning, the order in which holes are filled can drastically affect search efficiency: a wise choice can prune large swaths of the search space early, while a poor choice might explore many dead-ends. However, the choice of hole-filling order is largely unattended in program synthesis literature. In this paper, we propose a novel hole-filling strategy that leverages abstract interpretation to guide the order of hole-filling in program synthesis. Our approach overapproximates the behavior of the underlying abstract interpreter for pruning, enabling it to predict the most promising hole to fill next. We instantiate our approach to the domains of bitvectors and strings, which are commonly used in program synthesis tasks. We evaluate our approach on a set of benchmarks from the prior work, including SyGuS benchmarks, and show that it significantly outperforms the state-of-the-art approaches in terms of efficiency thanks to the abstract abstract interpretation techniques.

链接与引用

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

BibTeX
@article{LeeLY26,
  title = {Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling},
  author = {Doyoon Lee and Woosuk Lee and Kwangkeun Yi},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776694}
}