一句话：提出基于抽象解释与A*搜索的最优程序合成框架，可证明最优并剪枝次优子树，提升可扩展性。
本文研究在给定 DSL 中合成带数值常数、并在一组输入输出示例上优化准确率等定量目标的程序。作者提出一个具有可证明最优性保证的通用最优合成框架：在通用搜索图中枚举程序，节点表示具体程序集合；结合 A* 搜索与基于抽象解释的启发式，该启发式给出搜索图子树取值的上界，从而剪掉可证明次优的子树以提升可扩展性。针对数据分类 DSL 中常见的单调语义，作者还提出构造抽象变换器的自然策略。在两个现有 DSL 上实现并评估，表明该算法比现有最优合成器更具可扩展性。
We consider the problem of synthesizing programs with numerical constants that optimize a quantitative objective, such as accuracy, over a set of input-output examples. We propose a general framework for optimal synthesis of such programs in a given domain specific language (DSL), with provable optimality guarantees. Our framework enumerates programs in a general search graph, where nodes represent subsets of concrete programs. To improve scalability, it uses A * search in conjunction with a search heuristic based on abstract interpretation; intuitively, this heuristic establishes upper bounds on the value of subtrees in the search graph, enabling the synthesizer to identify and prune subtrees that are provably suboptimal. In addition, we propose a natural strategy for constructing abstract transformers for monotonic semantics, which is a common property for components in DSLs for data classification. Finally, we implement our approach in the context of two such existing DSLs, demonstrating that our algorithm is more scalable than existing optimal synthesizers.
@article{paperbot2641,
title = {Optimal Program Synthesis via Abstract Interpretation},
author = {Stephen Mell and Steve Zdancewic and Osbert Bastani},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632858}
}