Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Optimal Program Synthesis via Abstract Interpretation

Stephen Mell, Steve Zdancewic, Osbert Bastani

TL;DR

The paper addresses optimal synthesis of neurosymbolic programs with real-valued constants by introducing a unified framework that couples A* search with an admissible heuristic derived from abstract interpretation. It expands the search space to generalized partial programs and uses interval domains to overapproximate both program semantics and the objective, enabling provable pruning of suboptimal branches. The authors instantiate the framework on two DSLs (NEAR and Quivr) and demonstrate superior scalability compared to SMT-based optima and BFS baselines, while maintaining optimality guarantees within a user-defined tolerance $\bepsilon$. This approach offers a principled, scalable path for synthesizing high-quality programs for trajectory labeling and related data-processing tasks. The work advances the state of neurosymbolic synthesis by providing a general, provably optimal framework that leverages abstract interpretation to guide search.

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.

Optimal Program Synthesis via Abstract Interpretation

TL;DR

The paper addresses optimal synthesis of neurosymbolic programs with real-valued constants by introducing a unified framework that couples A* search with an admissible heuristic derived from abstract interpretation. It expands the search space to generalized partial programs and uses interval domains to overapproximate both program semantics and the objective, enabling provable pruning of suboptimal branches. The authors instantiate the framework on two DSLs (NEAR and Quivr) and demonstrate superior scalability compared to SMT-based optima and BFS baselines, while maintaining optimality guarantees within a user-defined tolerance . This approach offers a principled, scalable path for synthesizing high-quality programs for trajectory labeling and related data-processing tasks. The work advances the state of neurosymbolic synthesis by providing a general, provably optimal framework that leverages abstract interpretation to guide search.

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.
Paper Structure (21 sections, 2 theorems, 55 equations, 2 figures, 1 table, 1 algorithm)

This paper contains 21 sections, 2 theorems, 55 equations, 2 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Optimal Synthesis via Abstract Interpretation
  4. Problem Formulation
  5. $A^*$ Synthesis via Abstract Interpretation
  6. Instantiation for Interval Domains
  7. Interval Domains from Partial Orders
  8. Interval Transformers for Monotone Functions
  9. Interval Transfomers for Monotone Objectives
  10. Partial Programs with Interval Constraints
  11. Interval Transformers for Partial Programs with Interval Constraints
  12. Implementation
  13. NEAR DSL for Trajectory Labeling
  14. Quivr DSL For Trajectory Queries
  15. Abstract $F_1$ Score
  16. ...and 6 more sections

Key Result

theorem 1

If Algorithm alg:main returns an abstract program $\hat{p}$, then $\hat{p}$ is $\epsilon$-optimal---i.e. $\forall p \in \gamma(\hat{p})$, $\phi^*_Z - \phi(p,Z) \leq \epsilon$.

Figures (2)

  • Figure 1: A frame from a video of two mice interacting calms21; the mice are very close together, and are exhibiting the "sniff" behavior. The video has been processed using deep neural networks to produce certain keypoints, which are shown.
  • Figure 2: The time (seconds, log scale) to identify the optimal program and prove its optimality, for our approach (blue, solid) and an SMT solver (red, dashed), as a function of the size of the training dataset, for two different tasks.

Theorems & Definitions (9)

  • definition 1
  • definition 2
  • theorem 1
  • definition 3
  • definition 4
  • definition 5
  • lemma 1
  • definition 6
  • definition 7