Synthesis Benchmarks for Automated Reasoning

TL;DR

This paper introduces a new, evolving benchmark dataset for deductive program synthesis based on $orallorall$-formulas, aiming to advance research in automated reasoning and synthesis methods.

Contribution

It provides the first canonical benchmark set for $orallorall$-specification synthesis with uncomputable symbol restrictions, complementing existing benchmarks.

Findings

New benchmark dataset for deductive synthesis introduced

Dataset supports uncomputable symbol restrictions

Benchmark set is dynamically growing to foster future research

Abstract

Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $\forall\exists$-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the $\forall\exists$-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, composed by complementing existing benchmarks by new ones. Our data set is dynamically growing and should motivate future developments in the theory and practice of automating synthesis.