Search papers, labs, and topics across Lattice.
This paper introduces a framework for optimal program synthesis with numerical constants, targeting the optimization of quantitative objectives like accuracy. The approach uses A* search on a search graph of program subsets, guided by a heuristic derived from abstract interpretation to prune provably suboptimal subtrees. The authors also present a strategy for constructing abstract transformers for monotonic semantics, relevant for data classification DSLs, and demonstrate improved scalability compared to existing optimal synthesizers on two DSLs.
Provably optimal program synthesis, guided by abstract interpretation, can now outperform existing methods in data classification DSLs.
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.
