Optimal Program Synthesis via Abstract Interpretation

TL;DR

This paper introduces a scalable, optimal program synthesis framework using abstract interpretation and A* search, providing guarantees of optimality for programs with numerical constants in domain-specific languages.

Contribution

It presents a novel search-based synthesis method with provable optimality and scalability improvements over existing approaches, leveraging abstract interpretation heuristics.

Findings

The framework guarantees optimality of synthesized programs.

It outperforms existing methods in scalability.

The approach is effective for data classification DSLs.

Abstract

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.