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.

翻译：我们研究通过输入-输出示例集合成具有数值常数且优化定量目标（如准确率）的程序问题。我们提出一个通用框架，用于在给定领域特定语言（DSL）中对此类程序进行可证明最优性保证的最优综合。该框架在通用搜索图中枚举程序，其中节点表示具体程序的子集。为提升可扩展性，框架结合基于抽象解释的搜索启发式策略实施A*搜索；直观而言，该启发式策略通过建立搜索图中子树取值的上界，使综合器能够识别并剪枝可证明次优的子树。此外，我们提出一种为单调语义构建抽象转换器的自然策略，该性质在数据分类领域特定语言的组件中普遍存在。最后，我们在两种现有领域特定语言中实现该方法，证明所提算法比现有最优综合器具有更高的可扩展性。