Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics

TL;DR

This paper presents Moito, a domain-agnostic framework that automates pruning in top-down program synthesis by exploiting semantic monotonicity to construct interval-based abstractions. By casting pruning as interval abstract interpretation and enabling automatic generation of abstract transformers from concrete CHCs, the approach unifies previously domain-specific pruning techniques (e.g., AlphaRegex, SIMPL) and couples them with Grammar Flow Analysis to compute precise hole abstractions. The system demonstrably improves synthesis performance across a broad SemGuS benchmark suite, solving more problems than naive enumeration and often pruning large portions of the search space. These results indicate that monotonicity-guided interval abstractions are a scalable, general tool for accelerating domain-agnostic program synthesis in practice.

Abstract

In top-down enumeration for program synthesis, abstraction-based pruning uses an abstract domain to approximate the set of possible values that a partial program, when completed, can output on a given input. If the set does not contain the desired output, the partial program and all its possible completions can be pruned. In its general form, abstraction-based pruning requires manually designed, domain-specific abstract domains and semantics, and thus has only been used in domain-specific synthesizers. This paper provides sufficient conditions under which a form of abstraction-based pruning can be automated for arbitrary synthesis problems in the general-purpose Semantics-Guided Synthesis (SemGuS) framework without requiring manually-defined abstract domains. We show that if the semantics of the language for which we are synthesizing programs exhibits some monotonicity properties, one can obtain an abstract interval-based semantics for free from the concrete semantics of the programming language, and use such semantics to effectively prune the search space. We also identify a condition that ensures such abstract semantics can be used to compute a precise abstraction of the set of values that a program derivable from a given hole in a partial program can produce. These precise abstractions make abstraction-based pruning more effective. We implement our approach in a tool, Moito, which can tackle synthesis problems defined in the SemGuS framework. Moito can automate interval-based pruning without any a-priori knowledge of the problem domain, and solve synthesis problems that previously required domain-specific, abstraction-based synthesizers -- e.g., synthesis of regular expressions, CSV file schema, and imperative programs from examples.

Figures (6)

• Figure 1: An example-based SemGuS problem for imperative programs (\ref{['fig:imp-grammar', 'fig:imp-sem', 'fig:imp-constraint']}), and a sound abstract semantics for the grammar $G_I$ (\ref{['fig:imp-sem-abs']}). We use lowercase $l,u$ variables to denote integers and uppercase variables $L,U$ to denote pairs of integers, where $L(x)$ and $U(x)$ correspond to the first element of the pair, and $L(y), U(y)$ the second element.
• Figure 2: The first three plots compare Moito-h, Moito-n, and baseline across time, memory, and number of enumerated programs (we start the $x$-axis at 150 to better illustrate the interesting behavior---i.e., we do not show the behavior on the 150 easiest benchmarks). The last plot shows the maximum size reached before timing out on problems that could not be solved. Note that a line that is lower and to the right represents better performance in the first three plots, and higher and to the left in the final plot.
• Figure 3: Moito-n vs Moito-h (log,log)
• Figure 4: Time to compute interval abstract semantics
• Figure 5: An example-based SemGuS problem for regular expressions (\ref{['fig:regex-grammar', 'fig:regex-sem', 'fig:regex-constraint']}), and an sound abstract semantics for the grammar $G_R$ (\ref{['fig:regex-sem-abs']}). We denote $[\mathcal{S}]$ to denote the input interval over strings $s$.

Theorems & Definitions (25)

• definition 1: Regular tree grammar
• definition 2: Semantics
• definition 3: Example-based SemGuS Problem
• definition 4
• definition 5: Interval abstract domain
• definition 6: Interval Abstract Semantics
• Theorem 3.1: Sound Abstract Semantics and Pruning
• definition 7: Monotonicity
• Theorem 4.1: Abstraction of Monotonic Functions
• definition 8: CHC Interval Abstraction