PaperlayerView exact revision on arXiv

Source-linked AI summary

Absynthe: Abstract Interpretation-Guided Synthesis

Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn

arXiv:2302.13145v2cs.PL

TL;DR

Prior synthesis approaches can require complete source-language embeddings or language-bound solvers, making them difficult to apply to industrial-grade languages. Absynthe guides language-independent search with user-defined abstract semantics and validates candidates with concrete tests. It performs similarly to enumerative solvers on SyGuS strings and reaches parity with AutoPandas on Pandas benchmarks.

  • Problem

    Prior synthesis approaches often require complete and accurate source-language embeddings in solver logic or couple synthesis engines to a particular language model, posing difficulties for industrial-grade languages.

    Source: §1 · pp. 1–2

  • Method

    Absynthe guides language-independent program search with user-defined abstract semantics and abstract specifications, then validates candidates against concrete tests.

    Source: §1 · p. 2

  • Results

    Absynthe performs similarly to enumerative solvers on SyGuS strings and reaches parity with AutoPandas on Pandas benchmarks using simple abstractions.

    Source: §1 · p. 3, §7 · p. 22

  • Takeaways & Limitations

    The authors conclude that Absynthe combines lightweight abstract domains with testing to support guided synthesis across different language domains.

    Source: §1 · p. 3, §7 · p. 22

    Absynthe uses forward evaluation rules rather than inverse semantics, easing specification but requiring more compute to synthesize function arguments.

    Source: §4 · p. 13

Abstract

from arXiv · show

Synthesis tools have seen significant success in recent times. However, past approaches often require a complete and accurate embedding of the source language in the logic of the underlying solver, an approach difficult for industrial-grade languages. Other approaches couple the semantics of the source language with purpose-built synthesizers, necessarily tying the synthesis engine to a particular language model. In this paper, we propose Absynthe, an alternative approach based on user-defined abstract semantics that aims to be both lightweight and language agnostic, yet effective in guiding the search for programs. A synthesis goal in Absynthe is specified as an abstract specification in a lightweight user-defined abstract domain and concrete test cases. The synthesis engine is parameterized by the abstract semantics and independent of the source language. Absynthe validates candidate programs against test cases using the actual concrete language implementation to ensure correctness. We formalize the synthesis rules for Absynthe and describe how the key ideas are scaled-up in our implementation in Ruby. We evaluated Absynthe on SyGuS strings benchmark and found it competitive with other enumerative search solvers. Moreover, Absynthe's ability to combine abstract domains allows the user to move along a cost spectrum, i.e., expressive domains prune more programs but require more time. Finally, to verify Absynthe can act as a general purpose synthesis tool, we use Absynthe to synthesize Pandas data frame manipulating programs in Python using simple abstractions like types and column labels of a data frame. Absynthe reaches parity with AutoPandas, a deep learning based tool for the same benchmark suite. In summary, our results demonstrate Absynthe is a promising step forward towards a general-purpose approach to synthesis that may broaden the applicability of synthesis to more $\ldots$

1 INTRODUCTION

Absynthe addresses the difficulty of embedding industrial-grade languages in solver logic or binding synthesis engines to particular language models. It separates search from user-defined abstract semantics and checks completed candidates against concrete tests.

1 INTRODUCTION

  • Prior approaches often require complete source-language embeddings or language-specific solvers, a challenge for industrial languages such as Ruby and Python.Source: §1 · pp. 1–2
  • Absynthe separates search from user-defined abstract semantics, guiding program generation with abstract specifications and validating completed candidates against concrete tests.Source: §1 · p. 2
  • The paper formalizes abstract transformers and synthesis rules, including domain-specific strategies for finite, solver-backed, and computation-based domains.Source: §1 · p. 2
  • A Ruby core library supports custom abstract domains, product domains, and checks generated programs with a concrete interpreter against examples.Source: §1 · p. 2
  • Absynthe performs similarly to enumerative solvers on SyGuS strings and reaches parity with AutoPandas using simple Pandas abstractions.The reported Pandas abstractions include types and data-frame column labels.Source: §1 · p. 3
  • The authors present Absynthe as a step toward lightweight formal guarantees while retaining test-based correctness checks.Source: §1 · pp. 2–3

2 OVERVIEW

Absynthe guides synthesis of Pandas programs with abstract domains for column names and types, then validates completed candidates against concrete input/output examples. In the running example, this guidance finds a solution much faster than naïve enumeration.

2 OVERVIEW

  • The example abstracts data frames as column-name sets and combines this domain with a Python type domain to guide Pandas synthesis.Column-name semantics union the input columns for merge and preserve them for query; type semantics check expected argument types and return DataFrame when valid.Source: §2 · pp. 3, 5, 6
  • Naïve enumeration times out after 20 minutes, while abstract-interpretation guidance finds a solution in 0.47 seconds.The example restricts the search to selected Python constructs and merge/query methods, though the evaluation supports more methods.Source: §2 · p. 4
  • ProductDomain pairs column-name and type abstractions, while finite abstract domains can be enumerated to narrow choices at a hole.The product interpreter evaluates each component with its corresponding semantics and combines the results.Source: §2 · pp. 6–7
  • Absynthe derives an abstract function signature from input/output examples and constructs constants from example rows and columns.The running example requires a DataFrame output with specified columns and uses column names and row labels as constants.Source: §2 · p. 6
  • Synthesis expands abstractly labeled holes, interprets partial candidates, and rejects candidates that fail type or column constraints before concrete testing.Completed candidates are checked in the Python interpreter against the input/output examples.Source: §2 · pp. 6–7

3 FORMALISM

Absynthe formalizes synthesis over abstract values and uses abstract semantics to prune partial programs while concrete tests validate completed candidates. Its transformer DSL narrows abstract-variable bounds, and its search combines goal-directed and enumerative hole expansion.

3 FORMALISM

  • The formalism represents expressions as values, variables, abstraction-tagged holes, and function applications, with programs defined as single-function bodies.Abstract domains supply values, ordering, abstraction and concretization functions, and sound abstract transfer functions.Source: §3 · pp. 7–8
  • Abstract evaluation lifts concrete values, looks up variables, returns hole labels, and applies abstract transfer functions to evaluated function arguments.The synthesis goal requires a hole-free program to abstractly map the specified input abstraction to the output abstraction, then pass concrete input/output examples.Source: §3 · p. 8

3.1 Abstract Transformer Function DSL

  • Lmeta defines abstract transformers using abstractions, variables, function applications, conditionals, and tests for top, bottom, variables, values, or ordering.Failed conditional tests return top to preserve sound over-approximation, with reduced precision.Source: §3.1 · pp. 8–9
  • Ordering comparisons constrain abstract-variable bounds to ranges satisfying the comparison, narrowing the branch's possible values soundly.The DSL evaluates expressions under abstract and bounds environments; comparing a variable with an abstract value can tighten its upper bound.Source: §3.1 · pp. 9–10

3.2 Abstraction-Guided Synthesis

  • Hole expansion substitutes compatible values or variables, uses finite-domain generation or solver-backed inference where available, and otherwise enumerates applications with fresh abstract variables.Solver-backed inference requires a background-theory interpretation of the abstract transformer; S-Enumer may create candidates whose abstractions are later rejected.Source: §3.2 · pp. 10–11
  • The worklist algorithm generates candidates, abstractly checks them against the goal, tests completed programs concretely, and expands valid partial programs within a size bound.Candidate ordering uses domain-specific heuristics.Source: §3.2 · pp. 11–12

4 IMPLEMENTATION

The Ruby implementation provides reusable interfaces for user-defined domains, abstract interpreters, and concrete testing, alongside search-order and caching optimizations. Its limitations include extra search cost from forward-only semantics and possible combinatorial explosion when abstractions provide little guidance.

4 IMPLEMENTATION

  • Absynthe is a roughly 3,000-line Ruby core library with user-defined source translation and candidate-testing interfaces, plus a separate Z3 constraint library.Users may provide constants to make term generation tractable for languages with infinitely many terminals.Source: §4 · p. 12
  • The implementation explores candidates by increasing size and fixes a rule order, selecting finite-domain or solver-backed expansion when applicable and otherwise enumerating.The rule order prefers constants and variables before function applications, hashes, and arrays.Source: §4 · p. 12
  • The AbstractDomain base class supplies top, bottom, abstract variables, and ordering support; ProductDomain combines user-defined domains pointwise.Solver-aided domains check ordering constraints for satisfiability and assign solved abstract variables to holes.Source: §4 · p. 12
  • Abstract interpreters recursively evaluate terms and apply domain transformers, while ProductDomain interpreters are derived by composing base-domain interpreters.Product results combine individual interpretations pointwise.Source: §4 · pp. 12–13
  • Completed candidates that satisfy the abstract specification are run in a reference interpreter against concrete test cases and discarded if any test fails.A candidate passing all test cases is considered the correct solution.Source: §4 · p. 13
  • Forward-only semantics can increase subterm synthesis time, product domains remain independent, solver-aided domains concretize some subterms, and unguided enumeration can explode for larger terms.The authors identify problems with full formal semantics as a better fit for solver-aided synthesis tools.Source: §4 · p. 13

5 EVALUATION

The evaluation tests Absynthe on SyGuS strings and Python Pandas benchmarks, examining both synthesis performance and adaptation to a different domain. Absynthe solves 77% of SyGuS benchmarks and matches AutoPandas’s neural model in the number of Pandas programs solved.

5.1 SyGuS Strings

  • The SyGuS evaluation covers 22 benchmarks with four example-count variants, excludes programs with branches, and uses a Ruby interpreter to test generated candidates.The detailed results use the standard variant; the authors state that they generalize to the other variants.Source: §5.1 · p. 14
  • For SyGuS, the authors designed string-length, prefix, and suffix domains from benchmark examples, adding abstract annotations when unannotated enumeration timed out.SyGuS grammar type-checking meant they did not need a separate type domain.Source: §5.1 · pp. 14–15
  • Absynthe solves around 77% of SyGuS benchmarks, roughly matching EuSolver’s benchmark count despite a 600-second timeout versus EuSolver’s 3600 seconds.Most benchmarks finish within about 7 seconds; name-combine-3, phone-6, and phone-7 take longer.Source: §5.1 · pp. 15–16, Table 1 · p. 16
  • String-length semantics prune more candidates but cost more per candidate than string-suffix semantics, illustrating a trade-off between pruning precision and synthesis time.Phone-6 explores 5937 candidates in 100.54 seconds with string length; name-combine-3 explores 117370 candidates in 47.86 seconds with string suffix.Source: §5.1 · pp. 16–17
  • Disabling the small-expression cache slows every benchmark, while disabling template inference slows most and causes timeouts on phone-7 and phone-8.Without caching, phone-6 and phone-7 repeat work synthesizing the same function-application subterms.Source: §5.1 · p. 17

5.2 AutoPandas

  • For AutoPandas, Absynthe combines type and column-label domains and tests candidates in Python; the benchmarks use one input-output example and include method arguments.The type and column domains represent computed-value types and dataframe column labels, respectively.Source: §5.2 · pp. 17–18
  • Absynthe solves 17 AutoPandas programs, matching the neural model’s total while producing a different set of solutions with significant overlap.Table 2 also distinguishes benchmarks solved only by Absynthe from those solved only by AutoPandas.Source: Table 2 · p. 19, §5.2 · p. 19
  • AutoPandas synthesis time depends on abstract pruning and candidate testing, while depth-3 failures can fall back to enumeration because the domains lack relational abstractions across method arguments.Under naïve enumeration, Absynthe searches a strictly larger program set than the AutoPandas baseline, which restricts methods to those in the benchmark specification.Source: §5.2 · pp. 19–20

6 RELATED WORK

Related work spans general-purpose and domain-specific synthesis, abstraction-guided search, and learning-based methods. Absynthe differs through executable user-defined abstract semantics that guide enumerative search.

General Purpose Synthesis Tools

  • SemGuS shares the goal of general-purpose abstraction-guided synthesis but uses constrained Horn clause semantics; Absynthe instead targets synthesis with executable abstract semantics [Kim et al. 2021].The authors describe SemGuS semantics as time-consuming and error-prone to define, and note its stronger unrealizability-proving performance compared with synthesis.Source: §6 · p. 20
  • Unlike solver-aided languages such as Rosette and Sketch, Absynthe uses abstract interpretation to guide search and can reason about unbounded program properties.The authors also contrast its semantic reasoning, including polymorphism, with syntax-grammar approaches.Source: §6 · p. 20

Domain-specific synthesis

  • For SyGuS strings, CVC4 performs better than Absynthe’s simple abstract domains, while Absynthe’s reported strength is generalizability to AutoPandas benchmarks [Reynolds and Tinelli 2017].Absynthe is also enumerative like EuSolver, with abstract semantics guiding search [Alur et al. 2017b].Source: §6 · pp. 20–21
  • The authors identify adapting Absynthe to domain-specific synthesis as future work, noting that the general-purpose tool lacks domain-specific optimizations.They list prior abstractions for types and examples, table operations, refinement types, declassification, atomic sections, and SQL equivalence [Frankle et al. 2016; Osera and Zdancewic 2015; Feng et al. 2017; Polikarpova et al. 2016; Guria et al. 2022; Vechev et al. 2010; Wang et al. 2017a].Source: §6 · p. 21

Abstraction-guided Synthesis

  • Absynthe lets users provide an abstract interpreter and infer abstract values for holes, whereas Blaze requires a predicate universe and FlashMeta requires inverse operator semantics [Wang et al. 2017b; Polozov and Gulwani 2015].Simpl also combines enumerative search with static-analysis pruning [So and Oh 2017].Source: §6 · p. 21

Learning-based approaches

  • Absynthe does not use machine learning and is described as complementary to learned candidate ranking and probabilistic grammars [Balog et al. 2017; Barke et al. 2020].The authors leave exploring combinations of abstract-domain pruning and learned ordering for future work.Source: §6 · p. 21

7 CONCLUSION

Absynthe combines abstract interpretation with testing to synthesize programs using lightweight, user-defined abstract domains and partial language semantics.

7 CONCLUSION

  • Absynthe combines abstract interpretation and testing to synthesize programs.Users supply lightweight abstract domains and partial language semantics to guide search over programs.Source: §7 · p. 22
  • Absynthe solves 77% of SyGuS strings benchmarks, most within 7 seconds, and performs at par with AutoPandas on its benchmark suite.The paper also describes a pay-as-you-go model in which users pay only for the abstract domain used.Source: §7 · p. 22
  • The authors present Absynthe as a promising design choice combining testing for correctness with lightweight abstractions and partial semantics for search guidance.Source: §7 · p. 22
Loading 2302.13145v2…