Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The SemGuS Toolkit

Keith J. C. Johnson, Andrew Reynolds, Thomas Reps, Loris D'Antoni

TL;DR

The paper tackles the challenge of making program synthesis programmable, domain- and solver-agnostic by introducing SemGuS Format 1.0 and an open-source toolkit. It presents ks2, a baseline solver framework that compiles CHCs into executable semantics, provides incomplete SMT-based verification, and offers top-down and bottom-up enumerative solvers with extensible interfaces. A comprehensive benchmark suite of 431 SemGuS problems is provided to evaluate solver performance and guide future improvements, with 161 problems solvable by the baseline solvers. The work enables interoperability between solvers, supports multiple user-defined semantics, and lays the foundation for domain-specific languages and more scalable synthesis approaches leveraging the CHC-based semantics formalism.

Abstract

Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solvers, and presents an evaluation of the baseline enumerative solvers.

The SemGuS Toolkit

TL;DR

The paper tackles the challenge of making program synthesis programmable, domain- and solver-agnostic by introducing SemGuS Format 1.0 and an open-source toolkit. It presents ks2, a baseline solver framework that compiles CHCs into executable semantics, provides incomplete SMT-based verification, and offers top-down and bottom-up enumerative solvers with extensible interfaces. A comprehensive benchmark suite of 431 SemGuS problems is provided to evaluate solver performance and guide future improvements, with 161 problems solvable by the baseline solvers. The work enables interoperability between solvers, supports multiple user-defined semantics, and lays the foundation for domain-specific languages and more scalable synthesis approaches leveraging the CHC-based semantics formalism.

Abstract

Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a parser, a verifier, and enumerative SemGuS solvers. The paper also describes an initial set of SemGuS benchmarks, which form the basis for comparing SemGuS solvers, and presents an evaluation of the baseline enumerative solvers.
Paper Structure (8 sections, 3 equations, 3 figures, 1 table)

This paper contains 8 sections, 3 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. The SemGuS Format 1.0
  3. A Baseline SemGuS Solver
  4. Verifying Candidate Solutions
  5. Baseline Enumerative solvers
  6. Extensibility
  7. Benchmarks and Performance of Baseline Solvers
  8. Related Work

Figures (3)

  • Figure 1: Definition of a programming language (i.e., a set of programs) in the SemGuS format. The syntax of terms is given in lines \ref{['line:syntax-start']}--\ref{['line:syntax-end']}, and their semantics is given in lines \ref{['line:sem-start']}--\ref{['line:sem-end']}. The gray text denotes parts that have been omitted for brevity.
  • Figure 2: Constraints for a few example input/output pairs, used to synthesize a function mul that behaves like multiplication.
  • Figure 3: Cactus plot of runtime. (Lower and to the right is better.)