[TYPES/announce] Call for solvers and benchmarks for the Synthesis Standard Demonstration

[Andrew Reynolds]

[Apologies for multiple postings]


Call for SyGuS and SemGuS benchmarks and solvers for the Synthesis Standard
Demonstration (Deadline July 1st 2022).

Background:

The classical formulation of the program-synthesis problem is to find a
program that meets a correctness specification given as a logical formula.
Recent work on program synthesis and program optimization illustrates many
potential benefits of allowing the user to supplement the logical
specification with a syntactic template that constrains the space of
allowed implementations.

The scope of synthesis problems in this demonstration fit into the
following paradigms:

1) Syntax-Guided Synthesis (SyGuS) is a paradigm for specifying problems
where the target program is an expression in an SMT theory. The input to
SyGuS consists of a background theory, a semantic-correctness specification
for the desired program given by a logical

formula, and a syntactic set of candidate implementations given by a
grammar.

2) Semantics-Guided Synthesis (SemGuS) is a paradigm for specifying
problems where the target program lies in an arbitrary language. The key
difference from SyGuS is that the SemGuS format allows one to specify both
the syntax and semantics that define the search space.  The syntax is
defined by giving a grammar; the semantics of the language is defined using
constrained Horn clauses (CHCs).

For both paradigms, the computational problem then is to find an
implementation

from the set of candidate programs that satisfies the specification.

Aimed at stimulating innovations in SyGuS techniques, SyGuS-Comp, a
competition of solvers for SyGuS benchmarks, was held every year from 2014
to 2019. There has been continued interest in both using SyGuS solvers for
various synthesis applications and using SyGuS benchmarks for evaluating
new solution strategies. In 2020, the SyGuS organization sent a call to the
SyGuS community requesting new benchmarks, feedback on proposed new
extensions, and suggestions for new features. Additionally,
semantics-guided synthesis was introduced recently as a way of specifying
user-defined semantics for expressions that do not fit an SMT-LIB
background theory. We demo a range of baseline solvers for these domains at
FloC 2022.

The demonstration will consist of 4 tracks. For each track, the organizers
will curate a set of benchmarks and run all available solvers on them.  The
tracks are:

   1.

   SyGuS general track:  Benchmarks in SyGuS 2.1 format (
   https://urldefense.com/v3/__https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI1-TJM-xg$ ) whose logic is limited to
   standard SMT-LIB theories.
   2.

   Tables track: Benchmarks in SyGuS 2.1 format whose logic includes a
   recently developed SMT-LIB theory of tables.
   3.

   Oracles track: Benchmarks in SyGuS 2.1 format that use the oracles
   feature.
   4.

   SemGuS track: Benchmarks in the SemGuS format (https://urldefense.com/v3/__http://semgus.org/__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2KYRNmkQ$ ).


Solvers may be judged based on speed and quality of solutions. However,
there will be no official scoring or awards. Instead, an emphasis will be
put on showcasing available features in solvers and challenging benchmarks
in current applications.

We invite the members of the synthesis community to participate in all
tracks of this demonstration, either by submitting benchmarks and new
solvers.

New categories for this year’s demonstration

Synthesis for a Theory of Tables:

Synthesizing table manipulation programs (e.g., SQL, Python Pandas, R
tidyverse) can benefit data scientists by automating their data preparation
and database querying pipelines. While table manipulation programs are
often short, they have large parameter spaces and also operate over tables
that are compound values (list of tuples); as a result, synthesizing table
manipulation programs provide unique challenges for synthesizer developers.

In order to advance our synthesis algorithm development for tables, we
start a new track of “Synthesis for a Theory of Tables” for Sygus with the
following resources:

   -

   An SMT-LIB compliant theory of tables that standardized signatures of
   common table operators including table join, filtering, and aggregation (
   https://urldefense.com/v3/__https://homepage.cs.uiowa.edu/*ajreynol/tableTheory.pdf__;fg!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI12L6AmXA$ ).


   -

   We provide a set of programming-by-examples (PBE) benchmarks from the
   paper “Synthesizing Highly Expressive SQL Queries from Input-Output
   Examples (PLDI 2017)” over this domain in the standard SyGuS format for
   evaluation of the synthesizers.

We envision this as the first step towards developing a full “theory of
relational tables” for developing general table program synthesizers.

Oracles:

Formal inductive synthesis, such as the algorithms typically deployed to
solve SyGuS problems, typically work by querying an oracle multiple times.
Typically a verification oracle, which uses the semantic constraints given
in the SyGuS file to generate a verification query to give to an SMT
solver. However, problems exist where it’s either not possible/difficult to
encode these constraints as static first-order logic constraints in
SyGuS-IF, or checking these constraints is difficult for an SMT solver and
a custom reasoning engine would be better suited. The new oracles
extension, based on work in the paper “Satisfiability and Synthesis Modulo
Oracles”, allows a user to provide external oracles alongside a typical
SyGuS specification. This enables the user to provide models that refer to
external binaries treated as queryable black-boxes, and to use external
reasoning engines as part of the verification condition.

The concrete syntax for specifying constraints involving oracles has been
incorporated in the SyGuS IF 2.1 standard (
https://urldefense.com/v3/__https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI1-TJM-xg$ ).  Specifically, this track
will involve benchmarks in the SyGuS format where the “oracles” feature
(see Section 2.8) is enabled, and where the background theories are part of
the SMT-LIB standard.

SemGuS:

The SemGuS problem formulation was first introduced in the paper
“Semantics-guided synthesis,” together with a number of solvers that could
handle various SemGuS problems.

While SyGuS is useful for synthesizing expressions over a fixed theory,
SemGuS has the capability of defining a semantics for the programming
language to be used in the synthesis problem in a domain-agnostic, logical
format. This capability allows SemGuS to support a wider range of synthesis
problems—in particular, synthesis problems for which SMT-LIB compliant
background theories have not been developed, such as imperative programs,
SQL queries, etc.

SemGuS is a new format, and so far only a handful of solvers have been
developed for solving SemGuS problems. The SemGuS format and a parser for
it are available at semgus.org.

The purpose of this call is two-fold: 1. For developers of synthesis tools
to develop new SemGuS solvers. 2. To gather a broader set of SemGuS
benchmarks.

The original SemGuS paper compiled a set of 496 benchmarks, ranging over
standard SyGuS problems, imperative program-synthesis problems, and
synthesis problems over regular expressions. Like SyGuS, there is a need to
grow the number of SemGuS benchmarks; in particular, as SemGuS promises to
be a general format capable of expressing synthesis problems over arbitrary
domains, we are looking for a wide variety of benchmarks coming from
various domains and scenarios. Any contribution adding to the set of SemGuS
benchmarks would be much appreciated.

Call for Solvers and Benchmarks (Deadline July 1st 2022):

1) Call for solvers:
This year’s demonstration will run on the existing benchmarks and on the
ones collected through this call. The demonstration will welcome solvers
that can solve benchmarks in any of the categories mentioned in this call.
Those interested in submitting a new solver can contact the organizers at
the following email addresses:

   -

   SyGuS: sygus-organizers at seas.upenn.edu.
   -

   SemGuS: semgus at office365.wisc.edu


2) Call for benchmarks:
Benchmarks can be submitted through the following ways for each category:

   -

   SyGuS: pull requests at https://urldefense.com/v3/__https://github.com/SyGuS-Org/benchmarks__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2BwyDF-w$ 
   -

   SemGuS: pull requests at https://urldefense.com/v3/__https://github.com/SemGuS-git/Semgus-Benchmarks/__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI2QTDzeUQ$ 
   .


All solvers will be presented and advertised through a talk describing the
results of this demonstration at SYNT, a workshop co-located with CAV22.

Organization:

The SyGuS infrastructure and competition was initiated as part of NSF
Expeditions in Computing project ExCAPE, and is currently organized by
Saswat Padhi (Amazon) and Andrew Reynolds (University of Iowa). For more
information see the sygus webpage https://urldefense.com/v3/__https://sygus.org/__;!!IBzWLUs!ALWKnpxaor9P_rjydK3oAxLGoOgT89Ik-Ah6p7dy4-ldfxvIPnzdcsIo_TIoluWediWogI1_OdsXuQ$  . For questions please
contact the organizers at sygus-organizers at seas.upenn.edu. The SemGuS
framework and its infrastructure were initiated by Jinwoo Kim, Loris
D’Antoni, and Tom Reps at the University of Wisconsin. The SemGuS
specification language was designed with the help of Andrew Reynolds. For
questions please contact semgus at office365.wisc.edu.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220413/1cbc85f9/attachment-0001.htm>