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