Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
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.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
16:10 - 17:25 | |||
16:10 25mTalk | Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages POPL Zhentao Ye Peking University, Ruyi Ji Peking University, Yingfei Xiong Peking University, Xin Zhang Peking University DOI | ||
16:35 25mTalk | Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling POPL Doyoon Lee Seoul National University, Woosuk Lee Hanyang University, Kwangkeun Yi Seoul National University DOI | ||
17:00 25mTalk | Oriented Metrics for Bottom-Up Enumerative Synthesis POPL DOI | ||