11institutetext:  University of California, Los Angeles, USA
11email<EMAIL_ADDRESS>22institutetext: Microsoft Research,
Cambridge, UK
22email<EMAIL_ADDRESS>33institutetext: Microsoft Research, Bengaluru,
India
33email<EMAIL_ADDRESS>
# Overfitting in Synthesis: Theory and Practice

Saswat Padhi ✉ Contributed during an internship at Microsoft Research,
India.11 Todd Millstein 11 Aditya Nori 22 Rahul Sharma 33

###### Abstract

In syntax-guided synthesis (SyGuS), a synthesizer’s goal is to automatically
generate a program belonging to a grammar of possible implementations that
meets a logical specification. We investigate a common limitation across
state-of-the-art SyGuS tools that perform counterexample-guided inductive
synthesis (CEGIS). We empirically observe that as the expressiveness of the
provided grammar increases, the performance of these tools degrades
significantly.

We claim that this degradation is not only due to a larger search space, but
also due to _overfitting_. We formally define this phenomenon and prove _no-
free-lunch_ theorems for SyGuS, which reveal a fundamental tradeoff between
synthesizer performance and grammar expressiveness.

A standard approach to mitigate overfitting in machine learning is to run
multiple learners with varying expressiveness in parallel. We demonstrate that
this insight can immediately benefit existing SyGuS tools. We also propose a
novel single-threaded technique called _hybrid enumeration_ that interleaves
different grammars and outperforms the winner of the 2018 SyGuS competition
(Inv track), solving more problems and achieving a $5\times$ mean speedup.

##  1 Introduction

The _syntax-guided synthesis_ (SyGuS) framework [3] provides a unified format
to describe a program synthesis problem by supplying  (1) a logical
specification for the desired functionality, and  (2) a grammar of allowed
implementations.  Given these two inputs, a SyGuS tool searches through the
programs that are permitted by the grammar to generate one that meets the
specification. Today, SyGuS is at the core of several state-of-the-art program
synthesizers [14, 28, 5, 23, 24], many of which compete annually in the SyGuS
competition [1, 4].

We demonstrate empirically that five state-of-the-art SyGuS tools are very
sensitive to the choice of grammar. Increasing grammar expressiveness allows
the tools to solve some problems that are unsolvable with less-expressive
grammars. However, it also causes them to fail on many problems that the tools
are able to solve with a less expressive grammar. We analyze the latter
behavior both theoretically and empirically and present techniques that make
existing tools much more robust in the face of increasing grammar
expressiveness.

We restrict our investigation to a widely used approach [6] to SyGuS called
_counterexample-guided inductive synthesis_ (CEGIS) [36, §5]. In this
approach, the synthesizer is composed of a learner and an oracle. The learner
iteratively identifies a candidate program that is consistent with a given set
of examples (initially empty) and queries the oracle to either prove that the
program is _correct_ , i.e., meets the given specification, or obtain a
counterexample that demonstrates that the program does not meet the
specification. The counterexample is added to the set of examples for the next
iteration. The iterations continue until a correct program is found or
resource/time budgets are exhausted.

#### Overfitting.

To better understand the observed performance degradation, we instrumented one
of these SyGuS tools (§ 2.2). We empirically observe that for a large number
of problems, the performance degradation on increasing grammar expressiveness
is often accompanied by a significant increase in the number of
counterexamples required. Intuitively, as grammar expressiveness increases so
does the number of _spurious_ candidate programs, which satisfy a given set of
examples but violate the specification. If the learner picks such a candidate,
then the oracle generates a counterexample, the learner searches again, and so
on.

In other words, increasing grammar expressiveness increases the chances for
_overfitting_ , a well-known phenomenon in machine learning (ML). Overfitting
occurs when a learned function explains a given set of observations but does
not generalize correctly beyond it. Since SyGuS is indeed a form of function
learning, it is perhaps not surprising that it is prone to overfitting.
However, we identify its specific source in the context of SyGuS — the
spurious candidates induced by increasing grammar expressiveness — and show
that it is a significant problem in practice. We formally define the
_potential for overfitting_ (), in Definition 7, which captures the number of
spurious candidates.

#### No Free Lunch.

In the ML community, this tradeoff between expressiveness and overfitting has
been formalized for various settings as _no-free-lunch_ (NFL) theorems [33,
§5.1]. Intuitively such a theorem says that for every learner there exists a
function that cannot be efficiently learned, where efficiency is defined by
the number of examples required. We have proven corresponding NFL theorems for
the CEGIS-based SyGuS setting (Theorems 3.2 and 3.1).

A key difference between the ML and SyGuS settings is the notion of _$m$
-learnability_. In the ML setting, the learned function may differ from the
true function, as long as this difference (expressed as an error probability)
is relatively small. However, because the learner is allowed to make errors,
it is in turn required to learn given an arbitrary set of $m$ examples (drawn
from some distribution). In contrast, the SyGuS learning setting is _all-or-
nothing_ — either the tool synthesizes a program that meets the given
specification or it fails. Therefore, it would be overly strong to require the
learner to handle an arbitrary set of examples.

Instead, we define a much weaker notion of $m$-learnability for SyGuS, which
only requires that there _exist_ a set of $m$ examples for which the learner
succeeds. Yet, our NFL theorem shows that even this weak notion of
learnability can always be thwarted: given an integer $m\geq 0$ and an
expressive enough (as a function of $m$) grammar, for every learner there
exists a SyGuS problem that cannot be learned without access to more than $m$
examples. We also prove that overfitting is inevitable with an expressive
enough grammar (Theorems 3.3 and 3.4) and that the potential for overfitting
increases with grammar expressiveness (Theorem 3.5).

#### Mitigating Overfitting.

Inspired by _ensemble methods_ [13] in ML, which aggregate results from
multiple learners to combat overfitting (and underfitting), we propose PLearn
— a black-box framework that runs multiple parallel instances of a SyGuS tool
with different grammars. Although prior SyGuS tools run multiple instances of
learners with different random seeds [20, 7], to our knowledge, this is the
first proposal to explore multiple grammars as a means to improve the
performance of SyGuS. Our experiments indicate that PLearn significantly
improves the performance of five state-of-the-art SyGuS tools — CVC4 [32, 7],
EUSolver [5], LoopInvGen [28], SketchAC [20, 36], and Stoch [3, III F].

However, running parallel instances of a synthesizer is computationally
expensive. Hence, we also devise a white-box approach, called _hybrid
enumeration_ , that extends the enumerative synthesis technique [2] to
efficiently interleave exploration of multiple grammars in a single SyGuS
instance. We implement hybrid enumeration within LoopInvGen 111Our
implementation is available at https://github.com/SaswatPadhi/LoopInvGen.  and
show that the resulting single-threaded learner, LoopInvGen +HE, has
negligible overhead but achieves performance comparable to that of PLearn for
LoopInvGen. Moreover, LoopInvGen +HE significantly outperforms the winner [27]
of the invariant-synthesis (Inv) track of 2018 SyGuS competition [4] — a
variant of LoopInvGen specifically tuned for the competition — including a
$5\times$ mean speedup and solving two SyGuS problems that no tool in the
competition could solve.

#### Contributions.

In summary, we present the following contributions:

  * (§ 2)

We empirically observe that, in many cases, increasing grammar expressiveness
degrades performance of existing SyGuS tools due to _overfitting_.

  * (§ 3)

We formally define overfitting and prove _no-free-lunch_ theorems for the
SyGuS setting, which indicate that overfitting with increasing grammar
expressiveness is a fundamental characteristic of SyGuS.

  * (§ 4)

We propose two mitigation strategies –  (1) a black-box technique that runs
multiple parallel instances of a synthesizer, each with a different grammar,
and  (2) a single-threaded enumerative technique, called _hybrid enumeration_
, that interleaves exploration of multiple grammars.

  * (§ 5)

We show that incorporating these mitigating measures in existing tools
significantly improves their performance.

##  2 Motivation

In this section, we first present empirical evidence that existing SyGuS tools
are sensitive to changes in grammar expressiveness. Specifically, we
demonstrate that as we increase the expressiveness of the provided grammar,
every tool starts failing on some benchmarks that it was able to solve with
less-expressive grammars. We then investigate one of these tools in detail.

###  2.1 Grammar Sensitivity of SyGuS Tools

We evaluated $5$ state-of-the-art SyGuS tools that use very different
techniques:

  * •

SketchAC [20] extends the Sketch synthesis system [36] by combining both
explicit and symbolic search techniques.

  * •

Stoch [3, III F] performs a stochastic search for solutions.

  * •

EUSolver [5] combines enumeration with unification strategies.

  * •

Reynolds et al. [32] extend CVC4 [7] with a refutation-based approach.

  * •

LoopInvGen [28] combines enumeration and Boolean function learning.

$\bm{b}$ ${{{{{{{{{{{{\hskip
8.50006pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords5}{\color[rgb]{0,0.48,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.48,0}true}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords5}{\color[rgb]{0,0.48,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.48,0}false}}}}}}\bnfor\bnfpn{\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords4}{\color[rgb]{0.64,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.64,0,0}Bool}}}}}}variables}\\\
\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords7}{\color[rgb]{0.5,0.422,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.422,0}not}}}}}}\bnfsp\,\bm{b}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords7}{\color[rgb]{0.5,0.422,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.422,0}or}}}}}}\bnfsp\,\bm{b}\bnfsp\,\bm{b}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords7}{\color[rgb]{0.5,0.422,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.422,0}and}}}}}}\bnfsp\,\bm{b}\bnfsp\,\bm{b}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

$\bm{i}$ Int constants  Int variables

$\blacktriangleright$ Additional rule in Equalities grammar : $\bm{b}$
${{{\hskip 8.50006pt\raisebox{5.50003pt}{\scalebox{0.425}{$\bm{+}$}}\hskip
5.74997pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}=}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

$\blacktriangleright$ Additional rules in Intervals grammar : $\bm{b}$
${{{{{{{{{{{{\hskip
8.50006pt\raisebox{5.50003pt}{\scalebox{0.425}{$\bm{+}$}}\hskip
5.74997pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}\textgreater}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}\textgreater=}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\\\
\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}\textless}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}\textless=}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

$\blacktriangleright$ Additional rules in Octagons grammar : $\bm{i}$
${{{{{{\hskip 8.50006pt\raisebox{5.50003pt}{\scalebox{0.425}{$\bm{+}$}}\hskip
5.74997pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}+}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}-}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

$\blacktriangleright$ Additional rule in Polyhedra grammar : $\bm{i}$
${{{\hskip 8.50006pt\raisebox{5.50003pt}{\scalebox{0.425}{$\bm{+}$}}\hskip
5.74997pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}\textasteriskcentered}}}}}}\raisebox{-2.5pt}{\scalebox{0.65}{{S}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

$\blacktriangleright$ Additional rule in Polynomials grammar : $\bm{i}$
${{{\hskip 8.50006pt\raisebox{5.50003pt}{\scalebox{0.425}{$\bm{+}$}}\hskip
5.74997pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}\textasteriskcentered}}}}}}\raisebox{-2.5pt}{\scalebox{0.65}{{N}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

$\blacktriangleright$ Additional rule in Peano grammar : $\bm{i}$
${{{{{{\hskip 8.50006pt\raisebox{5.50003pt}{\scalebox{0.425}{$\bm{+}$}}\hskip
5.74997pt\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}div}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}\bnfor\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{(}}}}}}}}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language{\@listingGroup{ltx_lst_keywords6}{\color[rgb]{0.6375,0,0.2125}\definecolor[named]{pgfstrokecolor}{rgb}{0.6375,0,0.2125}mod}}}}}}\bnfsp\,\bm{i}\bnfsp\,\bm{i}\text{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@numbers\lst@@@set@language\@listingLiterate{{{\color[rgb]{0.4,0.4,0.4}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.4}\pgfsys@color@gray@stroke{0.4}\pgfsys@color@gray@fill{0.4}{)}}}}}}}}$

Figure 1: Grammars of quantifier-free predicates over integers 333We use the
$\bnfpo\raisebox{4.58336pt}{\scalebox{0.425}{$\bm{+}$}}$ operator to append
new rules to previously defined nonterminals.

We ran these five tools on $180$ invariant-synthesis benchmarks, which we
describe in § 5. We ran the benchmarks with each of the six grammars of
quantifier-free predicates, which are shown in Footnote 3. These grammars
correspond to widely used abstract domains in the analysis of integer-
manipulating programs — Equalities, Intervals [11], Octagons [25], Polyhedra
[12], algebraic expressions (Polynomials) and arbitrary integer arithmetic
(Peano) [29]. The * S operator denotes scalar multiplication, e.g., (* S 2 x),
and * N denotes nonlinear multiplication, e.g., (* N x y).

Figure 2: For each grammar, each tool, the ordinate shows the number of
benchmarks that _fail_ with the grammar but are solvable with a less-
expressive grammar.

In Fig. 2, we report our findings on running each benchmark on each tool with
each grammar, with a $30$-minute wall-clock timeout. For each $\langle$tool,
grammar$\rangle$ pair, the $y$-axis shows the number of failing benchmarks
that the same tool is able to solve with a less-expressive grammar. We observe
that, for each tool, the number of such failures increases with the grammar
expressiveness. For instance, introducing the scalar multiplication operator (
* S ) causes CVC4 to fail on $21$ benchmarks that it is able to solve with
Equalities ($\nicefrac{{4}}{{21}}$), Intervals ($\nicefrac{{18}}{{21}}$), or
Octagons ($\nicefrac{{10}}{{21}}$). Similarly, adding nonlinear
multiplication causes LoopInvGen to fail on $10$ benchmarks that it can solve
with a less-expressive grammar.

###  2.2 Evidence for Overfitting

|  Increase ($\bm{\uparrow}$) |  Unchanged ($\bm{=}$) |  Decrease ($\bm{\downarrow}$)
---|---|---|---
Expressiveness${}^{\bm{\,\uparrow}}\>\>\wedge\;$ Time${}^{\bm{\,\uparrow}}\>\rightarrow\;$ Rounds${}^{\bm{\,?}}$ |  $27$ % |  $67$ % |  $6$ %
Expressiveness${}^{\bm{\,\uparrow}}\>\>\wedge\;$ Rounds${}^{\bm{\,\uparrow}}\>\rightarrow\;$ Time${}^{\bm{\,?}}$ |  $79$ % |  $6$ % |  $15$ %

Figure 3: Observed correlation between synthesis time and number of rounds,
upon increasing grammar expressiveness, with LoopInvGen [28] on $180$
benchmarks

To better understand this phenomenon, we instrumented LoopInvGen [28] to
record the candidate expressions that it synthesizes and the number of CEGIS
iterations (called _rounds_ henceforth). We compare each pair of successful
runs of each of our $180$ benchmarks on distinct grammars.444We ignore failing
runs since they require an unknown number of rounds.  In $65$ % of such pairs,
we observe performance degradation with the more expressive grammar. We also
report the correlation between performance degradation and number of rounds
for the more expressive grammar in each pair in Fig. 3.

In $67$ % of the cases with degraded performance upon increased grammar
expressiveness, the number of rounds remains unaffected — indicating that this
slowdown is mainly due to a larger search space. However, there is significant
evidence of performance degradation due to _overfitting_ as well. We note an
increase in the number of rounds for $27$ % of the cases with degraded
performance. Moreover, we notice performance degradation in $79$ % of all
cases that required more rounds on increasing grammar expressiveness.

Thus, a more expressive grammar not only increases the search space, but also
makes it more likely for LoopInvGen to overfit — select a spurious expression,
which the oracle rejects with a counterexample, hence requiring more rounds.
In the remainder of this section, we demonstrate this overfitting phenomenon
on the verification problem shown in Fig. 4, an example by Gulwani and Jojic
[17], which is the fib_19 benchmark in the Inv track of SyGuS-Comp 2018 [4].

1 assume $(0\leq
n\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;0\leq
m\leq n)$

2 assume
$(x=0\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;y=m)$

3 while $(x<n)$ do

4 $x\leftarrow x+1$

5 if $(x>m)$ then $y\leftarrow y+1$

6 assert $(y=n)$

Figure 4: The fib_19 benchmark [17]

For Fig. 4, we require an inductive invariant that is strong enough to prove
that the assertion on line 6 always holds. In the SyGuS setting, we need to
synthesize a predicate $\mathcal{I}\colon\mathbb{Z}^{\,4}\to\mathbb{B}$
defined on a symbolic state $\sigma=\langle m,n,x,y\rangle$, that satisfies
$\forall\sigma\colon\varphi(\mathcal{I},\sigma)$ for the specification
$\varphi$:555We use $\mathbb{B}$, $\mathbb{N}$, and $\mathbb{Z}$ to denote the
sets of all Boolean values, all natural numbers (positive integers), and all
integers respectively.

$\displaystyle\varphi(\mathcal{I},\sigma)\
\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}$ $\displaystyle\
\big{(}0\leq n\,\wedge\,0\leq m\leq
n\,\wedge\,x=0\,\wedge\,y=m\big{)}\mathrel{\leavevmode\resizebox{18.56253pt}{3.9188pt}{$\;\implies\;$}}\mathcal{I}(\sigma)$
(precondition)
$\displaystyle\operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\wedge$}}}$
$\displaystyle\
\forall\sigma^{\prime}\colon\big{(}\mathcal{I}(\sigma)\,\wedge\,T(\sigma,\sigma^{\prime})\big{)}\mathrel{\leavevmode\resizebox{18.56253pt}{3.9188pt}{$\;\implies\;$}}\mathcal{I}(\sigma^{\prime})$
(inductiveness)
$\displaystyle\operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\wedge$}}}$
$\displaystyle\ \big{(}x\geq
n\,\wedge\,\mathcal{I}(\sigma)\big{)}\mathrel{\leavevmode\resizebox{18.56253pt}{3.9188pt}{$\;\implies\;$}}y=n$
(postcondition)

where $\sigma^{\prime}=\langle
m^{\prime},n^{\prime},x^{\prime},y^{\prime}\rangle$ denotes the new state
after one iteration, and $T$ is a transition relation that describes the loop
body:

$\displaystyle T(\sigma,\sigma^{\prime})\
\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}$ $\displaystyle\
(x<n)\ \operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\wedge$}}}\
(x^{\prime}=x+1)\
\operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\wedge$}}}\
(m^{\prime}=m)\
\operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\wedge$}}}\
(n^{\prime}=n)$
$\displaystyle\operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\wedge$}}}$
$\displaystyle\ \big{[}\,(x^{\prime}\leq m\wedge y^{\prime}=y)\
\operatorname*{\raisebox{-0.41252pt}{\scalebox{1.25}{$\vee$}}}\
(x^{\prime}>m\wedge y^{\prime}=y+1)\,\big{]}$

Increasing expressiveness $\rightarrow$
---
Equalities |  Intervals |  Octagons |  Polyhedra |  Polynomials |  Peano
$\times$ |  $0.32$ s |  $2.49$ s |  $2.48$ s |  $55.3$ s |  $68.0$ s
FAIL |  ($19$ rounds) |  ($57$ rounds) |  ($57$ rounds) |  ($76$ rounds) |  ($88$ rounds)

(a) Synthesis time and number of CEGIS iterations (rounds) with various
grammars

  * 16:

$(x\geq n)\vee(x+1<n)\vee(m\geq x\,\wedge\,m=y)$

  * 28:

$(x=y)\vee(y+m-n=x)\vee(x+2<n)$

  * 57:

$(m=y)\vee(x\geq m\wedge x\geq y)$

(b) Sample predicates with Polyhedra

  * 16:

$(x\geq n)\vee(x+1<n)\;\vee$
$(2y=n)\vee(y\,(m-1)=m)$

  * 28:

$(y=1)\vee(y=0)\vee(m<1)\vee(x^{2}y>1)$

  * 57:

$(x+1\geq n)\vee(x+2<n)\;\vee$
$((m-n)(x-y)=1)$

(c) Sample predicates with Peano

Solution in both grammars: $(n\geq
y)\;\operatorname*{\raisebox{-0.42502pt}{\scalebox{1.25}{$\wedge$}}}\;(y\geq
x)\;\operatorname*{\raisebox{-0.42502pt}{\scalebox{1.25}{$\wedge$}}}\;((m=y)\,\vee\,(x\geq
m\wedge x\geq y))$

Figure 5: Performance of LoopInvGen [28] on the fib_19 benchmark (Fig. 4). In
(b) and (c), we show predicates generated at various rounds (numbered in
bold).

In Fig. 5(a), we report the performance of LoopInvGen on fib_19 (Fig. 4) with
our six grammars (Footnote 3). It succeeds with all but the least-expressive
grammar. However, as grammar expressiveness increases, the number of rounds
increase significantly — from $19$ rounds with Intervals to $88$ rounds with
Peano.

LoopInvGen converges to the _exact same_ invariant with both Polyhedra and
Peano but requires $30$ more rounds in the latter case. In Figs. 5(b) and
5(c), we list some expressions synthesized with Polyhedra and Peano
respectively. These expressions are solutions to intermediate subproblems —
the final loop invariant is a conjunction of a subset of these expressions
[28, §3.2]. Observe that the expressions generated with the Peano grammar are
quite complex and unlikely to generalize well. Peano’s extra expressiveness
leads to more spurious candidates, increasing the chances of overfitting and
making the benchmark harder to solve.

##  3 SyGuS Overfitting in Theory

In this section, first we formalize the _counterexample-guided inductive
synthesis_ (CEGIS) approach [36] to SyGuS, in which examples are iteratively
provided by a verification oracle. We then state and prove _no-free-lunch_
theorems, which show that there can be no optimal learner for this learning
scheme. Finally, we formalize a natural notion of _overfitting_ for SyGuS and
prove that the potential for overfitting increases with grammar
expressiveness.

###  3.1 Preliminaries

We borrow the formal definition of a SyGuS problem from prior work [3]:

######  Definition 1 (SyGuS Problem)

Given a background theory $\mathbb{T}$, a function symbol $f\colon X\to Y$,
and constraints on $f$:  (1) a semantic constraint, also called a
_specification_ , $\phi(f,x)$ over the vocabulary of $\mathbb{T}$ along with
$f$ and a symbolic input $x$, and  (2) a syntactic constraint, also called a
_grammar_ , given by a (possibly infinite) set $\mathcal{E}$ of expressions
over the vocabulary of the theory $\mathbb{T}$ ; find an expression
$e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}$ such that the formula $\forall
x\mathrel{\raisebox{0.5pt}{$\in$}}X\colon\phi(e,x)$ is valid modulo
$\mathbb{T}$.

We denote this SyGuS problem as $\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ and
say that it is _satisfiable_ iff there exists such an expression $e$, i.e.,
$\exists\,e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}\colon\forall
x\mathrel{\raisebox{0.5pt}{$\in$}}X\colon\phi(e,x)$. We call $e$ a _satisfying
expression_ for this problem, denoted as
$e\models\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$.

Recall, we focus on a common class of SyGuS learners, namely those that learn
from examples. First we define the notion of input-output (IO) examples that
are consistent with a SyGuS specification:

######  Definition 2 (Input-Output Example)

Given a specification $\phi$ defined on $f\colon X\to Y$ over a background
theory $\mathbb{T}$, we call a pair $\langle
x,y\rangle\mathrel{\raisebox{0.5pt}{$\in$}}X\times Y$ an input-output (IO)
example for $\phi$, denoted as $\langle
x,y\rangle\mathrel{\raisebox{-1.54999pt}{\scalebox{1.5}[2.0]{$\shortmid$}}\mkern-4.0mu\raisebox{-0.09995pt}{$\approx$}_{\,\mathbb{T}}}\phi$
iff it is satisfied by some valid interpretation of $f$ within $\mathbb{T}$,
i.e.,

$\langle
x,y\rangle\mathrel{\raisebox{-1.54999pt}{\scalebox{1.5}[2.0]{$\shortmid$}}\mkern-4.0mu\raisebox{-0.09995pt}{$\approx$}_{\,\mathbb{T}}}\phi\;\>\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\>\;\exists\,e_{\ast}\mathrel{\raisebox{0.5pt}{$\in$}}\mathbb{T}\colon
e_{\ast}(x)=y\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;\big{(}\forall
x\mathrel{\raisebox{0.5pt}{$\in$}}X\colon\phi(e_{\ast},x)\big{)}$

The next two definitions respectively formalize the two key components of a
CEGIS-based SyGuS tool: the verification oracle and the learner.

######  Definition 3 (Verification Oracle)

Given a specification $\phi$ defined on a function $f\colon X\to Y$ over
theory $\mathbb{T}$, a verification oracle $\mathcal{O}_{\phi}$ is a partial
function that given an expression $e$, either returns $\bot$ indicating
$\forall x\mathrel{\raisebox{0.5pt}{$\in$}}X\colon\phi(e,x)$ holds, or gives a
counterexample $\langle x,y\rangle$ against $e$, denoted as
$e\mathrel{\rightsquigarrow\mkern-12.5mu\scalebox{0.875}{\raisebox{0.29999pt}{$\times$}}}_{\phi}\\!\langle
x,y\rangle$, such that

$e\mathrel{\rightsquigarrow\mkern-12.5mu\scalebox{0.875}{\raisebox{0.29999pt}{$\times$}}}_{\phi}\\!\langle
x,y\rangle\;\>\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\>\;\neg\,\phi(e,x)\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;e(x)\neq
y\,\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;\langle
x,y\rangle\mathrel{\raisebox{-1.54999pt}{\scalebox{1.5}[2.0]{$\shortmid$}}\mkern-4.0mu\raisebox{-0.09995pt}{$\approx$}_{\,\mathbb{T}}}\phi$

We omit $\phi$ from the notations $\mathcal{O}_{\phi}$ and
$\mathrel{\rightsquigarrow\mkern-12.5mu\scalebox{0.875}{\raisebox{0.29999pt}{$\times$}}}_{\phi}\\!$
when it is clear from the context.

######  Definition 4 (CEGIS-based Learner)

A CEGIS-based learner $\mathcal{L}^{\mathcal{O}}\\!(q,\mathcal{E})$ is a
partial function that given an integer $q\geq 0$, a set $\mathcal{E}$ of
expressions, and access to an oracle $\mathcal{O}$ for a specification $\phi$
defined on $f\colon X\to Y$, queries $\mathcal{O}$ at most $q$ times and
either fails with $\bot$ or generates an expression
$e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}$. The _trace_

$\big{[}e_{0}\mathrel{\rightsquigarrow\mkern-12.5mu\scalebox{0.875}{\raisebox{0.29999pt}{$\times$}}}\\!\langle
x_{0},y_{0}\rangle,\>\ldots,\>e_{p-1}\mathrel{\rightsquigarrow\mkern-12.5mu\scalebox{0.875}{\raisebox{0.29999pt}{$\times$}}}\\!\langle
x_{p-1},y_{p-1}\rangle,\>e_{p}\big{]}\qquad\textnormal{where }0\leq p\leq q$

summarizes the interaction between the oracle and the learner. Each $e_{i}$
denotes the $i^{\text{th}}$ candidate for $f$ and $\langle x_{i},y_{i}\rangle$
is a counterexample $e_{i}$, i.e.,

$\big{(}\forall j<i\colon
e_{i}(x_{j})=y_{j}\wedge\phi(e_{i},x_{j})\big{)}\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;\big{(}e_{i}\mathrel{\rightsquigarrow\mkern-12.5mu\scalebox{0.875}{\raisebox{0.29999pt}{$\times$}}}_{\phi}\\!\langle
x_{i},y_{i}\rangle\big{)}$

Note that we have defined oracles and learners as (partial) functions, and
hence as _deterministic_. In practice, many SyGuS tools are deterministic and
this assumption simplifies the subsequent theorems. However, we expect that
these theorems can be appropriately generalized to randomized oracles and
learners.

###  3.2 Learnability and No Free Lunch

In the machine learning (ML) community, the limits of learning have been
formalized for various settings as _no-free-lunch_ theorems [33, §5.1]. Here,
we provide a natural form of such theorems for CEGIS-based SyGuS learning.

In SyGuS, the learned function must conform to the given grammar, which may
not be fully expressive. Therefore we first formalize grammar expressiveness:

######  Definition 5 ($\bm{k}$-Expressiveness)

Given a domain $X$ and range $Y$, a grammar $\mathcal{E}$ is said to be
$k$-expressive iff $\mathcal{E}$ can express exactly $k$ distinct $X\to Y$
functions.

A key difference from the ML setting is our notion of _$m$ -learnability_,
which formalizes the number of examples that a learner requires in order to
learn a desired function. In the ML setting, a function is considered to
$m$-learnable by a learner if it can be learned using an _arbitrary_ set of
$m$ i.i.d. examples (drawn from some distribution). This makes sense in the ML
setting since the learned function is allowed to make errors (up to some given
bound on the error probability), but it is much too strong for the _all-or-
nothing_ SyGuS setting.

Instead, we define a much weaker notion of $m$-learnability for CEGIS-based
SyGuS, which only requires that there _exist_ a set of $m$ examples that
allows the learner to succeed. The following definition formalizes this
notion.

######  Definition 6 (CEGIS-based $\bm{m}$-Learnability)

Given a SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ and an
integer $m\geq 0$, we say that S is $m$-learnable by a CEGIS-based learner
$\mathcal{L}$ iff there exists a verification oracle $\mathcal{O}$ under which
$\mathcal{L}$ can learn a satisfying expression for S with at most $m$ queries
to $\mathcal{O}$, i.e.,
$\exists\,\mathcal{O}\colon\mathcal{L}^{\mathcal{O}}\\!(m,\mathcal{E})\models\textsf{S}$.

Finally we state and prove the no-free-lunch (NFL) theorems, which make
explicit the tradeoff between grammar expressiveness and learnability.
Intuitively, given an integer $m$ and an expressive enough (as a function of
$m$) grammar, for every learner there exists a SyGuS problem that cannot be
solved without access to at least $m+1$ examples. This is true despite our
weak notion of learnability.

Put another way, as grammar expressiveness increases, so does the number of
examples required for learning. On one extreme, if the given grammar is
$1$-expressive, i.e., can express exactly one function, then all satisfiable
SyGuS problems are $0$-learnable — no examples are needed because there is
only one function to learn — but there are _many_ SyGuS problems that cannot
be satisfied by this function. On the other extreme, if the grammar is
$|Y|^{|X|}$-expressive, i.e., can express all functions from $X$ to $Y$, then
for every learner there exists a SyGuS problem that requires _all $|X|$
examples_ in order to be solved.

Below we first present the NFL theorem for the case when the domain $X$ and
range $Y$ are finite. We then generalize to the case when these sets may be
countably infinite. The proofs of these theorems can be found in § 0.A.1.

######  Theorem 3.1 (NFL in CEGIS-based SyGuS on Finite Sets)

Let $X$ and $Y$ be two arbitrary finite sets, $\mathbb{T}$ be a theory that
supports equality, $\mathcal{E}$ be a grammar over $\mathbb{T}$, and $m$ be an
integer such that $0\leq m<|X|$. Then, either:

  * •

$\mathcal{E}$ is not $k$-expressive for any $k>\sum_{i\,=\,0}^{m}$
$\frac{|X|\bm{!}\>\;|Y|^{i}}{(|X|\,-\,i)\bm{!}}$, or

  * •

for every CEGIS-based learner $\mathcal{L}$, there exists a satisfiable SyGuS
problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that S is not $m$-learnable by $\mathcal{L}$. Moreover, there exists a
different CEGIS-based learner for which S is $m$-learnable.

######  Theorem 3.2 (NFL in CEGIS-based SyGuS on Countably Infinite Sets)

Let $X$ be an arbitrary countably infinite set, $Y$ be an arbitrary finite or
countably infinite set,$\mathbb{T}$ be a theory that supports equality,
$\mathcal{E}$ be a grammar over $\mathbb{T}$, and $m$ be an integer such that
$m\geq 0$. Then, either:

  * •

$\mathcal{E}$ is not $k$-expressive for any $k>\aleph_{0}$, where
$\aleph_{0}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}|\mathbb{N}|$, or

  * •

for every CEGIS-based learner $\mathcal{L}$, there exists a satisfiable SyGuS
problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that S is not $m$-learnable by $\mathcal{L}$. Moreover, there exists a
different CEGIS-based learner for which S is $m$-learnable.

###  3.3 Overfitting

Last, we relate the above theory to the notion of overfitting from ML. In the
context of SyGuS, overfitting can potentially occur whenever there are
multiple candidate expressions that are consistent with a given set of
examples. Some of these expressions may not generalize to satisfy the
specification, but the learner has no way to distinguish among them (using
just the given set of examples) and so can “guess” incorrectly. We formalize
this idea through the following measure:

######  Definition 7 (Potential for Overfitting)

Given a problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ and a
set $Z$ of IO examples for $\phi$, we define the potential for overfitting  as
the number of expressions in $\mathcal{E}$ that are consistent with $Z$ but do
not satisfy S, i.e.,

$\textnormal{\textOmega}(\textsf{S},Z)\,\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\,\left\\{\begin{array}[]{ll}\left|\big{\\{}e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}\;\mid\;e\not\models\textsf{S}\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;\forall\langle
x,y\rangle\mathrel{\raisebox{0.5pt}{$\in$}}Z\colon
e(x)=y\big{\\}}\right|&\hskip 23.99997pt\forall
z\mathrel{\raisebox{0.5pt}{$\in$}}Z\colon
z\mathrel{\raisebox{-1.54999pt}{\scalebox{1.5}[2.0]{$\shortmid$}}\mkern-4.0mu\raisebox{-0.09995pt}{$\approx$}_{\,\mathbb{T}}}\phi\\\\[3.75pt]
\bot\qquad\textnormal{(undefined)}&\hskip
23.99997pt\textnormal{otherwise}\end{array}\right.$

Intuitively, a zero potential for overfitting means that overfitting is not
possible on the given problem with respect to the given set of examples,
because there is no spurious candidate. A positive potential for overfitting
means that overfitting is possible, and higher values imply more spurious
candidates and hence more potential for a learner to choose the “wrong”
expression.

The following theorems connect our notion of overfitting to the earlier NFL
theorems by showing that overfitting is inevitable with an expressive enough
grammar. We provide their proofs in § 0.A.2.

######  Theorem 3.3 (Overfitting in SyGuS on Finite Sets)

Let $X$ and $Y$ be two arbitrary finite sets, $m$ be an integer such that
$0\leq m<|X|$, $\mathbb{T}$ be a theory that supports equality, and
$\mathcal{E}$ be a $k$-expressive grammar over $\mathbb{T}$ for some $k>$
$\frac{|X|\bm{!}\>\;|Y|^{m}}{m\bm{!}\;(|X|\,-\,m)\bm{!}}$. Then, there exists
a satisfiable SyGuS problem
$\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that $\textnormal{\textOmega}(\textsf{S},Z)>0$, for every set $Z$ of $m$ IO
examples for $\phi$.

######  Theorem 3.4 (Overfitting in SyGuS on Countably Infinite Sets)

Let $X$ be an arbitrary countably infinite set, $Y$ be an arbitrary finite or
countably infinite set, $\mathbb{T}$ be a theory that supports equality, and
$\mathcal{E}$ be a $k$-expressive grammar over $\mathbb{T}$ for some
$k>\aleph_{0}$. Then, there exists a satisfiable SyGuS problem
$\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that $\textnormal{\textOmega}(\textsf{S},Z)>0$, for every set $Z$ of $m$ IO
examples for $\phi$.

Finally, it is straightforward to show that as the expressiveness of the
grammar provided in a SyGuS problem increases, so does its potential for
overfitting.

######  Theorem 3.5 (Overfitting Increases with Expressiveness)

Let $X$ and $Y$ be two arbitrary sets, $\mathbb{T}$ be an arbitrary theory,
$\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ be grammars over $\mathbb{T}$ such
that $\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{2}$,
$\phi$ be an arbitrary specification over $\mathbb{T}$ and a function symbol
$f\colon X\to Y$, and $Z$ be a set of IO examples for $\phi$. Then, we have

$\textnormal{\textOmega}\big{(}\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}_{1}$}\right\rangle_{\,\mathbb{T}},Z\big{)}\;\leq\;\textnormal{\textOmega}\big{(}\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}_{2}$}\right\rangle_{\,\mathbb{T}},Z\big{)}$

##  4 Mitigating Overfitting

_Ensemble methods_ [13] in machine learning (ML) are a standard approach to
reduce overfitting. These methods aggregate predictions from several learners
to make a more accurate prediction. In this section we propose two approaches,
inspired by ensemble methods in ML, for mitigating overfitting in SyGuS. Both
are based on the key insight from § 3.3 that synthesis over a subgrammar has
a smaller potential for overfitting as compared to that over the original
grammar.

###  4.1 Parallel SyGuS on Multiple Grammars

Our first idea is to run multiple parallel instances of a synthesizer on the
same SyGuS problem but with grammars of varying expressiveness. This
framework, called PLearn, is outlined in Algorithm 1. It accepts a synthesis
tool $\mathcal{T}$, a SyGuS problem $\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, and
subgrammars $\mathcal{E}_{1\ldots p}$,666We use the shorthand
$\textnormal{X}_{1,\ldots,n}$ to denote the sequence
$\langle\textnormal{X}_{1},\ldots,\textnormal{X}_{n}\rangle$.  such that
$\mathcal{E}_{i}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$. The
parallel for construct creates a new thread for each iteration. The loop in
PLearn creates $p$ copies of the SyGuS problem, each with a different grammar
from $\mathcal{E}_{1\ldots p}$, and dispatches each copy to a new instance of
the tool $\mathcal{T}$. PLearn returns the first solution found or $\bot$ if
none of the synthesizer instances succeed.

1 func PLearn ($\mathcal{T}\colon$Synthesis Tool,
$\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}\colon$Problem,
$\mathcal{E}_{1\ldots p}\colon$Subgrammars)

2 $\blacktriangleright$ Requires:
$\forall\,\mathcal{E}_{i}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1\ldots
p}\colon\;\mathcal{E}_{i}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$

3 parallel for $i\leftarrow 1,\ldots,p$ do

4 $\textsf{S}_{i}\leftarrow\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}_{i}$}\right\rangle_{\,\mathbb{T}}$

5 $e_{i}\leftarrow\mathcal{T}(\textsf{S}_{i})$

6 if $e_{i}\neq\bot$ then return $e_{i}$

7 return $\bot$

Algorithm 1 The PLearn framework for SyGuS tools.

Since each grammar in $\mathcal{E}_{1\ldots p}$ is subsumed by the original
grammar $\mathcal{E}$, any expression found by PLearn is a solution to the
original SyGuS problem. Moreover, from Theorem 3.5 it is immediate that PLearn
indeed reduces overfitting.

######  Theorem 4.1 (PLearn Reduces Overfitting)

Given a SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, if
PLearn is instantiated with S and subgrammars $\mathcal{E}_{1\ldots p}$ such
that
$\forall\,\mathcal{E}_{i}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1\ldots
p}\colon\mathcal{E}_{i}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$,
then for each $\textsf{S}_{i}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}_{i}$}\right\rangle_{\,\mathbb{T}}$
constructed by PLearn, we have that
$\textnormal{\textOmega}(\textsf{S}_{i},Z)\leq\textnormal{\textOmega}(\textsf{S},Z)$
on any set $Z$ of IO examples for $\phi$.

A key advantage of PLearn is that it is agnostic to the synthesizer’s
implementation. Therefore, existing SyGuS learners can immediately benefit
from PLearn, as we demonstrate in § 5.1. However, running $p$ parallel SyGuS
instances can be prohibitively expensive, both computationally and memory-
wise. The problem is worsened by the fact that many existing SyGuS tools
already use multiple threads, e.g., the SketchAC [20] tool spawns $9$ threads.
This motivates our hybrid enumeration technique described next, which is a
novel synthesis algorithm that interleaves exploration of multiple grammars in
a single thread.

###  4.2 Hybrid Enumeration

Hybrid enumeration extends the _enumerative synthesis_ technique, which
enumerates expressions within a given grammar in order of size and returns the
first candidate that satisfies the given examples [2]. Our goal is to simulate
the behavior of PLearn with an enumerative synthesizer in a single thread.
However, a straightforward interleaving of multiple PLearn threads would be
highly inefficient because of redundancies – enumerating the same expression
(which is contained in multiple grammars) multiple times. Instead, we propose
a technique that  (1) enumerates each expression at most once, and  (2) reuses
previously enumerated expressions to construct larger expressions.

To achieve this, we extend a widely used [2, 30, 15] synthesis strategy,
called _component-based synthesis_ [21], wherein the grammar of expressions is
induced by a set of components, each of which is a typed operator with a fixed
arity. For example, the grammars shown in Footnote 3 are induced by integer
components (such as 1, +, mod, =, etc.) and Boolean components (such as true,
and, or, etc.). Below, we first formalize the grammar that is implicit in this
synthesis style.

######  Definition 8 (Component-Based Grammar)

Given a set $\,\mathscr{C}$ of typed components, we define the _component-
based_ grammar $\mathcal{E}$ as the set of all expressions formed by well-
typed component application over $\mathscr{C}$, i.e.,

$\begin{array}[]{rcl}\mathcal{E}\;=\;\\{\,c(e_{1},\ldots,e_{a})&\mid&(c:\tau_{1}\times\cdots\times\tau_{a}\to\tau)\mathrel{\raisebox{0.5pt}{$\in$}}\mathscr{C}\,\wedge\,e\raisebox{-1.99997pt}{\scalebox{0.65}{$1\ldots
a$}}\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}\\\\[1.25pt]
&\wedge&e_{1}:\tau_{1}\,\wedge\,\cdots\,\wedge\,e_{a}:\tau_{a}\,\\}\end{array}$

where $e:\tau$ denotes that the expression $e$ has type $\tau$.

We denote the set of all components appearing in a component-based grammar
$\mathcal{E}$ as $\textnormal{{components}}(\mathcal{E})$. Henceforth, we
assume that $\textnormal{{components}}(\mathcal{E})$ is known (explicitly
provided by the user) for each $\mathcal{E}$. We also use
$\textnormal{{values}}(\mathcal{E})$ to denote the subset of nullary
components (variables and constants) in
$\textnormal{{components}}(\mathcal{E})$, and
$\textnormal{{operators}}(\mathcal{E})$ to denote the remaining components
with positive arities.

The closure property of component-based grammars significantly reduces the
overhead of tracking which subexpressions can be combined together to form
larger expressions. Given a SyGuS problem over a grammar $\mathcal{E}$, hybrid
enumeration requires a sequence $\mathcal{E}_{1\ldots p}$ of grammars such
that each $\mathcal{E}_{i}$ is a component-based grammar and that
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$.
Next, we explain how the subset relationship between the grammars enables
efficient enumeration of expressions.

Given grammars
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}$,
observe that an expression of size $k$ in $\mathcal{E}_{i}$ may only contain
subexpressions of size $\\{1,\ldots,(k-1)\\}$ belonging to
$\mathcal{E}_{1\ldots i}$. This allows us to enumerate expressions in an order
such that each subexpression $e$ is synthesized (and cached) before any
expressions that have $e$ as a subexpression. We call an enumeration order
that ensures this property a _well order_.

######  Definition 9 (Well Order)

Given arbitrary grammars $\mathcal{E}_{1\ldots p}$, we say that a strict
partial order $\,\mathrel{\textnormal{$\triangleleft$}}$ on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$ is a well order iff

$\forall\,\mathcal{E}_{a},\mathcal{E}_{b}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1\ldots
p}:\enskip\forall\,k_{1},k_{2}\mathrel{\raisebox{0.5pt}{$\in$}}\mathbb{N}:\enskip[\,\mathcal{E}_{a}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{b}\,\wedge\,k_{1}<k_{2}\,]\mathrel{\leavevmode\resizebox{22.50003pt}{4.75006pt}{$\;\implies\;$}}(\mathcal{E}_{a},k_{1})\mathrel{\textnormal{$\triangleleft$}}\,(\mathcal{E}_{b},k_{2})$

Motivated by Theorem 3.5, our implementation of hybrid enumeration uses a
particular well order that incrementally increases the expressiveness of the
space of expressions. For a rough measure of the expressiveness (Definition 5)
of a pair ($\mathcal{E}$, $k$), i.e., the set of expressions of size $k$ in a
given grammar $\mathcal{E}$, we simply overapproximate the number of
syntactically distinct expressions:

###### Theorem 4.2

Let $\mathcal{E}_{1\ldots p}$ be component-based grammars and
$\mathscr{C}_{i}=\textnormal{{components}}(\mathcal{E}_{i})$. Then, the
following strict partial order
$\,\mathrel{\textnormal{$\triangleleft$}}_{\mkern 2.0mu\ast}$ on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$ is a well order

$\forall\,\mathcal{E}_{a},\mathcal{E}_{b}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1\ldots
p}:\enskip\forall\,m,n\mathrel{\raisebox{0.5pt}{$\in$}}\mathbb{N}:\enskip(\mathcal{E}_{a},m)\mathrel{\textnormal{$\triangleleft$}}_{\mkern
2.0mu\ast}(\mathcal{E}_{b},n)\mathrel{\leavevmode\resizebox{27.50003pt}{4.75006pt}{$\;\iff\;$}}|\mkern
2.0mu\mathscr{C}_{a}\mkern 1.0mu|^{m}<|\mkern 2.0mu\mathscr{C}_{b}\mkern
1.0mu|^{n}$

We now describe the main hybrid enumeration algorithm, which is listed in
Algorithm 2. The HEnum function accepts a SyGuS problem
$\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, a set
$\mathcal{E}_{1\ldots p}$ of component-based grammars such that
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$,
a well order $\mathrel{\textnormal{$\triangleleft$}}$, and an upper bound
$q\geq 0$ on the size of expressions to enumerate. In lines 4–8, we first
enumerate all values and cache them as expressions of size one. In general
$C[j,k][\tau]$ contains expressions of type $\tau$ and size $k$ from
$\mathcal{E}_{j}\setminus\mathcal{E}_{j-1}$. In line 9 we sort (grammar, size)
pairs in some total order consistent with
$\mathrel{\textnormal{$\triangleleft$}}$. Finally, in lines 10–20, we iterate
over each pair $(\mathcal{E}_{j},k)$ and each operator from
$\mathcal{E}_{1\ldots j}$ and invoke the Divide procedure (Footnote 8) to
carefully choose the operator’s argument subexpressions ensuring  (1)
_correctness_ – their sizes sum up to $k-1$,  (2) _efficiency_ – expressions
are enumerated at most once, and  (3) _completeness_ – all expressions of size
$k$ in $\mathcal{E}_{j}$ are enumerated.

1 func HEnum ($\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}\colon$Problem,
$\mathcal{E}_{1\ldots p}\colon$Grammars,
$\mathrel{\textnormal{$\triangleleft$}}\colon$WO, $q\colon$Max. Size)

2 $\blacktriangleright$ Requires: component-based grammars
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$
and $v$ as the input variable

3 $C\leftarrow\\{\\}$

4 for $i\leftarrow 1$ to $p$ do

5 $V\leftarrow$ if $i=1$ then $\textnormal{{values}}(\mathcal{E}_{1})$ else
$[\,\textnormal{{values}}(\mathcal{E}_{i})\setminus\textnormal{{values}}(\mathcal{E}_{i-1})\,]$

6 for each $(e:\tau)\mathrel{\raisebox{0.5pt}{$\in$}}V$ do

7 $C[i,1][\tau]\leftarrow C[i,1][\tau]\cup\\{e\\}$

8 if $\forall x\mathrel{\raisebox{0.5pt}{$\in$}}X\colon\phi(\lambda v.\,e,x)$
then return $\lambda v.\,e$

9
$R\leftarrow\textsc{Sort}(\mathrel{\textnormal{$\triangleleft$}},\;\mathcal{E}_{1\ldots
p}\times\\{2,\ldots,q\\})$

10 for $i\leftarrow 1$ to $|\,R\,|$ do

11 $(\mathcal{E}_{j},k)\leftarrow R[i]$

12 for $l\leftarrow 1$ to $j$ do

13 $O\leftarrow\textbf{if}\ l=1\ \textbf{then}\
\textnormal{{operators}}(\mathcal{E}_{1})\ \textbf{else}\
[\,\textnormal{{operators}}(\mathcal{E}_{l})\setminus\textnormal{{operators}}(\mathcal{E}_{l-1})\,]$

14 for each
$(o:\tau_{1}\times\cdots\times\tau_{a}\to\tau)\mathrel{\raisebox{0.5pt}{$\in$}}O$
do

15 $L\leftarrow\textsc{Divide}(a,\ k-1,\ l,\ j,\ \langle\rangle)$

16 for each
$\big{\langle}(x_{1},y_{1}),\ldots,(x_{a},y_{a})\big{\rangle}\mathrel{\raisebox{0.5pt}{$\in$}}L$
do

17 for each $e\raisebox{-1.69997pt}{\scalebox{0.65}{$1\ldots
a$}}\mathrel{\raisebox{0.5pt}{$\in$}}C[x_{1},y_{1}][\tau_{1}]\times\cdots\times
C[x_{a},y_{a}][\tau_{a}]$ do

18 $e\leftarrow o(e_{1},\ldots,e_{a})$

19 $C[j,k][\tau]\leftarrow C[j,k][\tau]\cup\\{e\\}$

20 if $\forall x\mathrel{\raisebox{0.5pt}{$\in$}}X\colon\phi(\lambda v.\,e,x)$
then return $\lambda v.\,e$

21 return $\bot$

Algorithm 2 _Hybrid enumeration_ to combat overfitting in SyGuS

The Divide algorithm generates a set of locations for selecting arguments to
an operator. Each location is a pair $(x,y)$ indicating that any expression
from $C[x,y][\tau]$ can be an argument, where $\tau$ is the argument type
required by the operator. Divide accepts an arity $a$ for an operator $o$, a
size budget $q$, the index $l$ of the least-expressive grammar containing $o$,
the index $j$ of the least-expressive grammar that should contain the
constructed expressions of the form $o(e_{1},\ldots,e_{a})$, and an
accumulator $\alpha$ that stores the list of argument locations. In lines 7–9,
the size budget is recursively divided among $a-1$ locations. In each
recursive step, the upper bound $(q-a+1)$ on $v$ ensures that we have a size
budget of at least $q-(q-a+1)=a-1$ for the remaining $a-1$ locations. This
results in a call tree such that the accumulator $\alpha$ at each leaf node
contains the locations from which to select the last $a-1$ arguments, and we
are left with some size budget $q\geq 1$ for the first argument $e_{1}$.
Finally in lines 4–5, we carefully select the locations for $e_{1}$ to ensure
that $o(e_{1},\ldots,e_{a})$ has not been synthesized before — either
$o\mathrel{\raisebox{0.5pt}{$\in$}}\textnormal{{components}}(\mathcal{E}_{j})$
or at least one argument belongs to
$\mathcal{E}_{j}\setminus\mathcal{E}_{j-1}$.

1 func Divide ($a\colon$Arity, $q\colon$Size, $l\colon$Op. Level,
$j\colon$Expr. Level, $\alpha\colon$Accumulated Args.)

2 $\blacktriangleright$ Requires: $1\leq a\leq q\;\wedge\;l\leq j$

3 if $a=1$ then

4 if $l=j\;\vee\;\exists\,\langle
x,y\rangle\mathrel{\raisebox{0.5pt}{$\in$}}\alpha\colon x=j$ then return
$\big{\\{}(1,q)\diamond\alpha,\ldots,(j,q)\diamond\alpha\big{\\}}$

5 return $\big{\\{}(j,q)\diamond\alpha\big{\\}}$

6 $L=\\{\\}$

7 for $u\leftarrow 1$ to $j$ do

8 for $v\leftarrow 1$ to $(q-a+1)$ do

9 $L\leftarrow L\;\cup\;\textsc{Divide}(a-1,\ q-v,\ l,\ j,\
(u,v)\diamond\alpha)$

10 return $L$

Algorithm 3 An algorithm to divide a given size budget among subexpressions
888We use $\diamond$ as the cons operator for sequences, e.g.,
$x\diamond\langle y,z\rangle=\langle x,y,z\rangle$.

We conclude this section by stating some desirable properties satisfied by
HEnum. The proofs of the following theorems can be found in § 0.A.3.

######  Theorem 4.3 (HEnum is Complete up to Size $\bm{q}$)

Given a SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, let
$\mathcal{E}_{1\ldots p}$ be component-based grammars over theory $\mathbb{T}$
such that
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}=\mathcal{E}$,
$\mathrel{\textnormal{$\triangleleft$}}$ be a well order on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$, and $q\geq 0$ be an upper bound on
size of expressions. Then, HEnum$(\textsf{S},\mathcal{E}_{1\ldots
p},\mathrel{\textnormal{$\triangleleft$}},q)$ will eventually find a
satisfying expression if there exists one with size $\leq q$.

######  Theorem 4.4 (HEnum is Efficient)

Given a SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, let
$\mathcal{E}_{1\ldots p}$ be component-based grammars over theory $\mathbb{T}$
such that
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$,
$\mathrel{\textnormal{$\triangleleft$}}$ be a well order on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$, and $q\geq 0$ be an upper bound on
size of expressions. Then, HEnum$(\textsf{S},\mathcal{E}_{1\ldots
p},\mathrel{\textnormal{$\triangleleft$}},q)$ will enumerate each distinct
expression at most once.

##  5 Experimental Evaluation

In this section we empirically evaluate PLearn and HEnum. Our evaluation uses
a set of $180$ synthesis benchmarks,999All benchmarks are available at
https://github.com/SaswatPadhi/LoopInvGen.  consisting of all $127$ official
benchmarks from the Inv track of 2018 SyGuS competition [4] augmented with
benchmarks from the 2018 Software Verification competition (SV-Comp) [8] and
challenging verification problems proposed in prior work [9, 10]. All these
synthesis tasks are defined over integer and Boolean values, and we evaluate
them with the six grammars described in Footnote 3. We have omitted benchmarks
from other tracks of the SyGuS competition as they either require us to
construct $\mathcal{E}_{1\ldots p}$ (§ 4) by hand or lack verification
oracles. All our experiments use an $8$-core Intel ® Xeon ® E5 machine clocked
at 2.30 GHz with 32 GB memory running Ubuntu ® 18.04.

###  5.1 Robustness of PLearn

For five state-of-the-art SyGuS solvers –  (a) LoopInvGen[28],  (b) CVC4[32,
7],  (c) Stoch[3, III F],  (d) SketchAC[20, 8], and  (e) EUSolver[5]–  we have
compared the performance across various grammars, with and without the PLearn
framework (Algorithm 1). In this framework, to solve a SyGuS problem with the
$p^{\text{th}}$ expressiveness level from our six integer-arithmetic grammars
(see Footnote 3), we run $p$ independent parallel instances of a SyGuS tool,
each with one of the first $p$ grammars. For example, to solve a SyGuS problem
with the Polyhedra grammar, we run four instances of a solver with the
Equalities, Intervals, Octagons and Polyhedra grammars. We evaluate these runs
for each tool, for each of the $180$ benchmarks and for each of the six
expressiveness levels.

(a) LoopInvGen [28]

(b) CVC4 [32, 7]

Solid blue curves (❌) show original failure counts.
Dashed orange curves ($\bullet$) show failure counts with PLearn.

Timeout = $30$ min. (wall-clock)

(c) Stoch [3, III F]

(d) SketchAC [20, 36]

(e) EUSolver [5]

Figure 6: The number of failures on increasing grammar expressiveness, for
state-of-the-art SyGuS tools, with and without the PLearn framework (Algorithm
1)

Fig. 6 summarizes our findings. Without PLearn the number of failures
initially decreases and then increases across all solvers, as grammar
expressiveness increases. However, with PLearn the tools incur fewer failures
at a given level of expressiveness, and there is a trend of _decreased_
failures with increased expressiveness. Thus, we have demonstrated that PLearn
is an effective measure to mitigate overfitting in SyGuS tools and
significantly improve their performance.

###  5.2 Performance of Hybrid Enumeration

To evaluate the performance of hybrid enumeration, we augment an existing
synthesis engine with HEnum (Algorithm 2). We modify our LoopInvGen tool [28],
which is the best-performing SyGuS synthesizer from Fig. 6. Internally,
LoopInvGen leverages Escher [2], an enumerative synthesizer, which we replace
with HEnum. We make no other changes to LoopInvGen. We evaluate the
performance and resource usage of this solver, LoopInvGen +HE, relative to the
original LoopInvGen with and without PLearn (Algorithm 1).

#### Performance.

In Fig. 7(a), we show the number of failures across our six grammars for
LoopInvGen, LoopInvGen +HE and LoopInvGen with PLearn, over our $180$
benchmarks. LoopInvGen +HE has a significantly lower failure rate than
LoopInvGen, and the number of failures decreases with grammar expressiveness.
Thus, hybrid enumeration is a good proxy for PLearn.

(a) Failures on increasing grammar expressiveness

Grammar |  M$\big{[}\\!\frac{\textbf{\scalebox{1.4}{\texttau}[P]}}{\textbf{\scalebox{1.4}{\texttau}[H]}}\\!\big{]}$ |  M$\big{[}\\!\frac{\textbf{\scalebox{1.4}{\texttau}[H]}}{\textbf{\scalebox{1.4}{\texttau}[L]}}\\!\big{]}$
---|---|---
Equalities |  $1.00$ |  $1.00$
Intervals |  $1.91$ |  $1.04$
Octagons |  $2.84$ |  $1.03$
Polyhedra |  $3.72$ |  $1.01$
Polynomials |  $4.62$ |  $1.00$
Peano |  $5.49$ |  $0.97$
(b) Median(M) overhead

Figure 7: L = LoopInvGen, H = LoopInvGen +HE, P = PLearn (LoopInvGen). H is
not only significantly robust against increasing grammar expressiveness, but
it also has a smaller total-time cost () than P and a negligible overhead over
L.

#### Resource Usage.

To estimate how computationally expensive each solver is, we compare their
_total-time cost_ (  ). Since LoopInvGen and LoopInvGen +HE are single-
threaded, for them we simply use the wall-clock time for synthesis as the
total-time cost. However, for PLearn with $p$ parallel instances of
LoopInvGen, we consider the total-time cost as $p$ times the wall-clock time
for synthesis.

In Fig. 7(b), we show the median overhead (ratio of  ) incurred by PLearn over
LoopInvGen +HE and LoopInvGen +HE over LoopInvGen, at various expressiveness
levels. As we move to grammars of increasing expressiveness, the total-time
cost of PLearn increases significantly, while the total-time cost of
LoopInvGen +HE essentially matches that of LoopInvGen.

###  5.3 Competition Performance

Finally, we evaluate the performance of LoopInvGen +HE on the benchmarks from
the Inv track of the 2018 SyGuS competition [4], against the official winning
solver, which we denote LIG [27] — a version of LoopInvGen [28] that has been
extensively tuned for this track. In the competition, there are some
invariant-synthesis problems where the postcondition itself is a satisfying
expression. LIG starts with the postcondition as the first candidate and is
extremely fast on such programs. For a fair comparison, we added this
heuristic to LoopInvGen +HE as well. No other change was made to LoopInvGen
+HE.

LoopInvGen solves $115$ benchmarks in a total of $2191$ seconds whereas
LoopInvGen +HE solves $117$ benchmarks in $429$ seconds, for a mean speedup of
over $5\times$. Moreover, no entrants to the competition could solve [4] the
two additional benchmarks (gcnr_tacas08 and fib_20) that LoopInvGen +HE
solves.

##  6 Related Work

The most closely related work to ours investigates overfitting for
verification tools [35]. Our work differs from theirs in several respects.
First, we address the problem of overfitting in CEGIS-based synthesis. Second,
we formally define overfitting and prove that all synthesizers must suffer
from it, whereas they only observe overfitting empirically. Third, while they
use cross-validation to combat overfitting in tuning a specific hyperparameter
of a verifier, our approach is to search for solutions at different
expressiveness levels.

The general problem of efficiently searching a large space of programs for
synthesis has been explored in prior work. Lee et al. [24] use a probabilistic
model, learned from known solutions to synthesis problems, to enumerate
programs in order of their likelihood. Other approaches employ type-based
pruning of large search spaces [31, 26]. These techniques are orthogonal to,
and may be combined with, our approach of exploring grammar subsets.

Our results are widely applicable to existing SyGuS tools, but some tools fall
outside our purview. For instance, in programming-by-example (PBE) systems
[18, §7], the specification consists of a set of input-output examples. Since
any program that meets the given examples is a valid satisfying expression,
our notion of overfitting does not apply to such tools. However in a recent
work, Inala and Singh [19] show that incrementally increasing expressiveness
can also aid PBE systems. They report that searching within increasingly
expressive grammar subsets requires significantly fewer examples to find
expressions that generalize better over unseen data. Other instances where the
synthesizers can have a free lunch, i.e., always generate a solution with a
small number of counterexamples, include systems that use grammars with
limited expressiveness [21, 34, 16].

Our paper falls in the category of formal results about SyGuS. In one such
result, Jha and Seshia [22] analyze the effects of different kinds of
counterexamples and of providing bounded versus unbounded memory to learners.
Notably, they do not consider variations in “concept classes” or “program
templates,” which are precisely the focus of our study. Therefore, our results
are complementary: we treat counterexamples and learners as opaque and instead
focus on grammars.

##  7 Conclusion

Program synthesis is a vibrant research area; new and better synthesizers are
being built each year. This paper investigates a general issue that affects
all CEGIS-based SyGuS tools. We recognize the problem of overfitting,
formalize it, and identify the conditions under which it must occur.
Furthermore, we provide mitigating measures for overfitting that significantly
improve the existing tools.

#### Acknowledgements

We thank Guy Van den Broeck and the anonymous reviewers for helpful feedback
for improving this work, and the organizers of the SyGuS competition for
making the tools and benchmarks publicly available.

This work was supported in part by the National Science Foundation (NSF) under
grants CCF-1527923 and CCF-1837129. The lead author was also supported by an
internship and a PhD Fellowship from Microsoft Research.

## References

  * web [2019] The SyGuS Competition.  http://sygus.org/comp/ (2019), Accessed: 2019-05-10
  * Albarghouthi et al. [2013] Albarghouthi, A., Gulwani, S., Kincaid, Z.: Recursive Program Synthesis.  In: Computer Aided Verification - 25th International Conference, CAV, Proceedings. Lecture Notes in Computer Science, vol. 8044, pp. 934–950. Springer (2013), https://doi.org/10.1007/978-3-642-39799-8_67
  * Alur et al. [2013] Alur, R., Bodík, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-Guided Synthesis.  In: Formal Methods in Computer-Aided Design, FMCAD. pp. 1–8. IEEE (2013), http://ieeexplore.ieee.org/document/6679385/
  * Alur et al. [2019] Alur, R., Fisman, D., Padhi, S., Singh, R., Udupa, A.: SyGuS-Comp 2018: Results and Analysis.  CoRR abs/1904.07146 (2019), http://arxiv.org/abs/1904.07146
  * Alur et al. [2017] Alur, R., Radhakrishna, A., Udupa, A.: Scaling Enumerative Program Synthesis via Divide and Conquer.  In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 319–336 (2017), https://doi.org/10.1007/978-3-662-54577-5_18
  * Alur et al. [2018] Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-Based Program Synthesis.  Commun. ACM 61(12), 84–93 (2018), https://doi.org/10.1145/3208071
  * Barrett et al. [2011] Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4.  In: Computer Aided Verification - 23rd International Conference, CAV, Proceedings. Lecture Notes in Computer Science, vol. 6806, pp. 171–177. Springer (2011), https://doi.org/10.1007/978-3-642-22110-1_14
  * Beyer [2017] Beyer, D.: Software Verification with Validation of Results - (Report on SV-COMP 2017).  In: Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10206, pp. 331–349 (2017), https://doi.org/10.1007/978-3-662-54580-5_20
  * Bounov et al. [2018] Bounov, D., DeRossi, A., Menarini, M., Griswold, W.G., Lerner, S.: Inferring Loop Invariants through Gamification.  In: Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems, CHI. p. 231. ACM (2018), https://doi.org/10.1145/3173574.3173805
  * Bradley et al. [2005] Bradley, A.R., Manna, Z., Sipma, H.B.: The Polyranking Principle.  In: Automata, Languages and Programming, 32nd International Colloquium, ICALP, Proceedings. Lecture Notes in Computer Science, vol. 3580, pp. 1349–1361. Springer (2005), https://doi.org/10.1007/11523468_109
  * Cousot and Cousot [1977] Cousot, P., Cousot, R.: Static Determination of Dynamic Properties of Generalized Type Unions.  In: Language Design for Reliable Software. pp. 77–94 (1977), https://doi.org/10.1145/800022.808314
  * Cousot and Halbwachs [1978] Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program.  In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages. pp. 84–96. ACM Press (1978), https://doi.org/10.1145/512760.512770
  * Dietterich [2000] Dietterich, T.G.: Ensemble Methods in Machine Learning.  In: Multiple Classifier Systems, First International Workshop, MCS, Proceedings. Lecture Notes in Computer Science, vol. 1857, pp. 1–15. Springer (2000), https://doi.org/10.1007/3-540-45014-9_1
  * Ezudheen et al. [2018] Ezudheen, P., Neider, D., D’Souza, D., Garg, P., Madhusudan, P.: Horn-ICE Learning for Synthesizing Invariants and Contracts.  PACMPL 2(OOPSLA), 131:1–131:25 (2018), https://doi.org/10.1145/3276501
  * Feng et al. [2017] Feng, Y., Martins, R., Geffen, J.V., Dillig, I., Chaudhuri, S.: Component-Based Synthesis of Table Consolidation and Transformation Tasks From Examples.  In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. pp. 422–436. ACM (2017), https://doi.org/10.1145/3062341.3062351
  * Godefroid and Taly [2012] Godefroid, P., Taly, A.: Automated Synthesis of Symbolic Instruction Encodings From I/O Samples.  In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. pp. 441–452. ACM (2012), https://doi.org/10.1145/2254064.2254116
  * Gulwani and Jojic [2007] Gulwani, S., Jojic, N.: Program Verification as Probabilistic Inference.  In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. pp. 277–289. ACM (2007), https://doi.org/10.1145/1190216.1190258
  * Gulwani et al. [2017] Gulwani, S., Polozov, O., Singh, R.: Program Synthesis.  Foundations and Trends in Programming Languages 4(1-2), 1–119 (2017), https://doi.org/10.1561/2500000010
  * Inala and Singh [2018] Inala, J.P., Singh, R.: WebRelate: Integrating Web Data with Spreadsheets using Examples.  PACMPL 2(POPL), 2:1–2:28 (2018), https://doi.org/10.1145/3158090
  * Jeon et al. [2015] Jeon, J., Qiu, X., Solar-Lezama, A., Foster, J.S.: Adaptive Concretization for Parallel Program Synthesis.  In: Computer Aided Verification - 27th International Conference, CAV, Proceedings, Part II. pp. 377–394. Lecture Notes in Computer Science, Springer (2015), https://doi.org/10.1007/978-3-319-21668-3_22
  * Jha et al. [2010] Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-Guided Component-Based Program Synthesis.  In: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 1, ICSE. pp. 215–224. ACM (2010), https://doi.org/10.1145/1806799.1806833
  * Jha and Seshia [2017] Jha, S., Seshia, S.A.: A Theory of Formal Synthesis via Inductive Learning.  Acta Informatica 54(7), 693–726 (2017), https://doi.org/10.1007/s00236-017-0294-5
  * Le et al. [2017] Le, X.D., Chu, D., Lo, D., Le Goues, C., Visser, W.: S3: Syntax- and Semantic-Guided Repair Synthesis via Programming by Examples.  In: Proceedings of the 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE. pp. 593–604. ACM (2017), https://doi.org/10.1145/3106237.3106309
  * Lee et al. [2018] Lee, W., Heo, K., Alur, R., Naik, M.: Accelerating Search-Based Program Synthesis using Learned Probabilistic Models.  In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018. pp. 436–449. ACM (2018), https://doi.org/10.1145/3192366.3192410
  * Miné [2001] Miné, A.: The Octagon Abstract Domain.  In: Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE. p. 310. IEEE Computer Society (2001), https://doi.org/10.1109/WCRE.2001.957836
  * Osera and Zdancewic [2015] Osera, P., Zdancewic, S.: Type-and-Example-Directed Program Synthesis.  In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. pp. 619–630. ACM (2015), https://doi.org/10.1145/2737924.2738007
  * Padhi et al. [2018] Padhi, S., Sharma, R., Millstein, T.: LoopInvGen: A Loop Invariant Generator based on Precondition Inference.  CoRR abs/1707.02029 (2018), http://arxiv.org/abs/1707.02029
  * Padhi et al. [2016] Padhi, S., Sharma, R., Millstein, T.D.: Data-Driven Precondition Inference with Learned Features.  In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. pp. 42–56. ACM (2016), https://doi.org/10.1145/2908080.2908099
  * Peano [1888] Peano, G.: Calcolo geometrico secondo l’Ausdehnungslehre di H. Grassmann: preceduto dalla operazioni della logica deduttiva, vol. 3.  Fratelli Bocca (1888)
  * Perelman et al. [2014] Perelman, D., Gulwani, S., Grossman, D., Provost, P.: Test-driven synthesis.  In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. pp. 408–418. ACM (2014), https://doi.org/10.1145/2594291.2594297
  * Polikarpova et al. [2016] Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program Synthesis from Polymorphic Refinement Types.  In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. pp. 522–538. ACM (2016), https://doi.org/10.1145/2908080.2908093
  * Reynolds et al. [2015] Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-Guided Quantifier Instantiation for Synthesis in SMT.  In: Computer Aided Verification - 27th International Conference, CAV, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9207, pp. 198–216. Springer (2015), https://doi.org/10.1007/978-3-319-21668-3_12
  * Shalev-Shwartz and Ben-David [2014] Shalev-Shwartz, S., Ben-David, S.: Understanding Machine Learning: From Theory to Algorithms.  Cambridge University Press (2014)
  * Sharma et al. [2013] Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A Data Driven Approach for Algebraic Loop Invariants.  In: Programming Languages and Systems - 22nd European Symposium on Programming, ESOP, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS, Proceedings. Lecture Notes in Computer Science, vol. 7792, pp. 574–592. Springer (2013), https://doi.org/10.1007/978-3-642-37036-6_31
  * Sharma et al. [2014] Sharma, R., Nori, A.V., Aiken, A.: Bias-Variance Tradeoffs in Program Analysis.  In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. pp. 127–138. ACM (2014), http://doi.acm.org/10.1145/2535838.2535853
  * Solar-Lezama [2013] Solar-Lezama, A.: Program Sketching.  STTT 15(5-6), 475–495 (2013), https://doi.org/10.1007/s10009-012-0249-7

##  Appendix 0.A Proofs of Theorems

###  0.A.1 No-Free-Lunch Theorems (§ 3.2)

######  Theorem 0.A.1 (NFL in CEGIS-based SyGuS on Finite Sets)

Let $X$ and $Y$ be two arbitrary finite sets, $\mathbb{T}$ be a theory that
supports equality, $\mathcal{E}$ be a grammar over $\mathbb{T}$, and $m$ be an
integer such that $0\leq m<|X|$. Then, either:

  * •

$\mathcal{E}$ is not $k$-expressive for any $k>\sum_{i\,=\,0}^{m}$
$\frac{|X|\bm{!}\>\;|Y|^{i}}{(|X|\,-\,i)\bm{!}}$, or

  * •

for every CEGIS-based learner $\mathcal{L}$, there exists a satisfiable SyGuS
problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that S is not $m$-learnable by $\mathcal{L}$. Moreover, there exists a
different CEGIS-based learner for which S is $m$-learnable.

###### Proof

First, note that there are
$t=\sum_{i\,=\,0}^{m}\frac{|X|\bm{!}\>\;|Y|^{i}}{(|X|\,-\,i)\bm{!}}$ distinct
traces (sequences of counterexamples) of length at most $m$ over $X$ and $Y$.
Now, consider some CEGIS-based learner $\mathcal{L}$, and suppose
$\mathcal{E}$ is $k$-expressive for some $k>t$. Then, since the learner can
deterministically choose at most $t$ candidates for the $t$ traces, there must
be at least one function $f$ that is expressible in $\mathcal{E}$, but does
not appear in the trace of $\mathcal{L}^{\mathcal{O}}\\!(m,\mathcal{E})$ for
any oracle $\mathcal{O}$.

Let $e$ be an expression in $\mathcal{E}$ that implements the function $f$.
Then, we can define the specification
$\phi(f,x)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}f(x)=e(x)$
and the SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$. By
construction, S is satisfiable since $e\models\textsf{S}$, but we have that
$\mathcal{L}^{\mathcal{O}}\\!(m,\mathcal{E})\not\models\textsf{S}$ for all
oracles $\mathcal{O}$. So, by Definition 6, we have that S is not
$m$-learnable by $\mathcal{L}$.

However, we can construct a learner $\mathcal{L}^{\prime}$ such that S is
$m$-learnable by $\mathcal{L}^{\prime}$. We construct $\mathcal{L}^{\prime}$
such that $\mathcal{L}^{\prime}$ always produces $e$ as its first candidate
expression for any trace. The result then follows by Definition 6. ∎

######  Theorem 0.A.2 (NFL in CEGIS-based SyGuS on Countably Infinite Sets)

Let $X$ be an arbitrary countably infinite set, $Y$ be an arbitrary finite
or countably infinite set, $\mathbb{T}$ be a theory that supports equality,
$\mathcal{E}$ be a grammar over $\mathbb{T}$, and $m$ be an integer such that
$m\geq 0$. Then, either:

  * •

$\mathcal{E}$ is not $k$-expressive for any $k>\aleph_{0}$, where
$\aleph_{0}\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}|\mathbb{N}|$, or

  * •

for every CEGIS-based learner $\mathcal{L}$, there exists a satisfiable SyGuS
problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that S is not $m$-learnable by $\mathcal{L}$. Moreover, there exists a
different CEGIS-based learner for which S is $m$-learnable.

###### Proof

Consider some CEGIS-based learner $\mathcal{L}$, and suppose $\mathcal{E}$ is
$k$-expressive for some $k>\aleph_{0}$. Note that there are
$\sum_{i\,=\,0}^{m}\frac{|X|\bm{!}\>\;|Y|^{i}}{(|X|\,-\,i)\bm{!}}$ distinct
traces of length at most $m$ over $X$ and $Y$. Let us overapproximate each
$\frac{|X|\bm{!}\>\;|Y|^{i}}{(|X|\,-\,i)\bm{!}}$ as $(|X|\,|Y|)^{m}$, and thus
the number of distinct traces as $(m+1)\,(|X|\,|Y|)^{m}$. We have two cases
for $Y$:

  1. 1.

$Y$ is finite i.e., $|X|=\aleph_{0}$ and $|Y|<\aleph_{0}$. Then, the number of
distinct traces is at most
$(m+1)\,(|X|\,|Y|)^{m}=(\aleph_{0}\,|Y|)^{m}=\aleph_{0}$. Or,

  2. 2.

$Y$ is countably infinite i.e., $|X|=|Y|=\aleph_{0}$. Then, the number of
distinct traces is at most
$(m+1)\,(|X|\,|Y|)^{m}=(\aleph_{0}\,\aleph_{0})^{m}=\aleph_{0}$.

Thus, the number of distinct traces is at most $\aleph_{0}$, i.e., countably
infinite. Since the number of distinct functions $k>\aleph_{0}$, the claim
follows using a construction similar to the proof of Theorem 0.A.1. ∎

###  0.A.2 Overfitting Theorems (§ 3.3)

######  Theorem 0.A.3 (Overfitting in SyGuS on Finite Sets)

Let $X$ and $Y$ be two arbitrary finite sets, $m$ be an integer such that
$0\leq m<|X|$, $\mathbb{T}$ be a theory that supports equality, and
$\mathcal{E}$ be a $k$-expressive grammar over $\mathbb{T}$ for some $k>$
$\frac{|X|\bm{!}\>\;|Y|^{m}}{m\bm{!}\;(|X|\,-\,m)\bm{!}}$. Then, there exists
a satisfiable SyGuS problem
$\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that $\textnormal{\textOmega}(\textsf{S},Z)>0$, for every set $Z$ of $m$ IO
examples for $\phi$.

###### Proof

First, note that there are
$t=\frac{|X|\bm{!}\>\;|Y|^{m}}{m\bm{!}\;(|X|\,-\,m)\bm{!}}$ distinct ways of
constructing a set of $m$ IO examples, over $X$ and $Y$. Now, suppose
$\mathcal{E}$ is $k$-expressive for some $k>t$. Then, there must be at least
one function $f$ that is expressible in $\mathcal{E}$, but every set of $m$ IO
examples that $f$ is consistent with is also satisfied by some other
expressible function.

Let $e$ be an expression in $\mathcal{E}$ that implements the function $f$.
Then, we can define the specification
$\phi(f,x)\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny def}}}{=}}f(x)=e(x)$
and the SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$. The
claim then immediately follows from Definition 7. ∎

######  Theorem 0.A.4 (Overfitting in SyGuS on Countably Infinite Sets)

Let $X$ be an arbitrary countably infinite set, $Y$ be an arbitrary finite or
countably infinite set, $\mathbb{T}$ be a theory that supports equality, and
$\mathcal{E}$ be a $k$-expressive grammar over $\mathbb{T}$ for some
$k>\aleph_{0}$. Then, there exists a satisfiable SyGuS problem
$\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$ such
that $\textnormal{\textOmega}(\textsf{S},Z)>0$, for every set $Z$ of $m$ IO
examples for $\phi$.

###### Proof

Let us overapproximate the number of distinct ways of constructing a set of
$m$ IO examples, $\frac{|X|\bm{!}\>\;|Y|^{m}}{m\bm{!}\;(|X|\,-\,m)\bm{!}}$ as
$(|X|\,|Y|)^{m}$. Using cardinal arithmetic, as shown in the the proof of
Theorem 0.A.2, this number is always at most $\aleph_{0}$. Then the claim
follows using a construction similar to the proof of Theorem 0.A.3. ∎

######  Theorem 0.A.5 (Overfitting Increases with Expressiveness)

Let $X$ and $Y$ be two arbitrary sets, $\mathbb{T}$ be an arbitrary theory,
$\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ be grammars over $\mathbb{T}$ such
that $\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{2}$,
$\phi$ be an arbitrary specification over $\mathbb{T}$ and a function symbol
$f\colon X\to Y$, and $Z$ be a set of IO examples for $\phi$. Then, we have

$\textnormal{\textOmega}\big{(}\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}_{1}$}\right\rangle_{\,\mathbb{T}},Z\big{)}\;\leq\;\textnormal{\textOmega}\big{(}\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}_{2}$}\right\rangle_{\,\mathbb{T}},Z\big{)}$

###### Proof

If $\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{2}$,
then for any set $Z\mathrel{\raisebox{0.5pt}{$\subseteq$}}X\times Y$ of IO
examples, we have

$\left\\{e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1}\,\mid\,\forall\langle
x,y\rangle\mathrel{\raisebox{0.5pt}{$\in$}}Z\colon
e(x)=y\right\\}\;\mathrel{\raisebox{0.5pt}{$\subseteq$}}\;\left\\{e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{2}\,\mid\,\forall\langle
x,y\rangle\mathrel{\raisebox{0.5pt}{$\in$}}Z\colon e(x)=y\right\\}$

The claim immediately follows from this observation and Definition 7. ∎

###  0.A.3 Properties of Hybrid Enumeration (§ 4.2)

###### Lemma 1

Let $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ be two arbitrary component-based
grammars. Then, if
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{2}$, it
must also be the case that
$\textnormal{{components}}(\mathcal{E}_{1})\mathrel{\raisebox{0.5pt}{$\subseteq$}}\,\textnormal{{components}}(\mathcal{E}_{2})$,
where $\textnormal{{components}}(\mathcal{E}_{i})$ denotes the set of all
components appearing in $\mathcal{E}_{i}$.

###### Proof

Let $\mathscr{C}_{1}=\textnormal{{components}}(\mathcal{E}_{1})$,
$\mathscr{C}_{2}=\textnormal{{components}}(\mathcal{E}_{2})$, and
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{2}$.
Suppose
$\mathscr{C}_{1}\not\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathscr{C}_{2}$.
Then, there must be at least one component $c$ such that
$c\mathrel{\raisebox{0.5pt}{$\in$}}\mathscr{C}_{1}\setminus\mathscr{C}_{2}$.
By definition of $\textnormal{{components}}(\mathcal{E}_{1})$, the component
$c$ must appear in at least one expression
$e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1}$. However, since
$c\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathscr{C}_{2}$, it must be the case
that $e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{2}$, thus
contradicting
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{2}$.
Hence, our assumption
$\mathscr{C}_{1}\not\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathscr{C}_{2}$
must be false. ∎

###### Theorem 0.A.7

Given component-based grammars $\mathcal{E}_{1\ldots p}$, the following strict
partial order $\,\mathrel{\textnormal{$\triangleleft$}}_{\mkern 2.0mu\ast}$ on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$ is a well order

$\forall\,\mathcal{E}_{a},\mathcal{E}_{b}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{1\ldots
p}:\enskip\forall\,m,n\mathrel{\raisebox{0.5pt}{$\in$}}\mathbb{N}:\enskip(\mathcal{E}_{a},m)\mathrel{\textnormal{$\triangleleft$}}_{\mkern
2.0mu\ast}(\mathcal{E}_{b},n)\mathrel{\leavevmode\resizebox{27.50003pt}{4.75006pt}{$\;\iff\;$}}|\mkern
2.0mu\mathscr{C}_{a}\mkern 1.0mu|^{m}<|\mkern 2.0mu\mathscr{C}_{b}\mkern
1.0mu|^{n}$

where $\mathscr{C}_{i}=\textnormal{{components}}(\mathcal{E}_{i})$ denotes the
set of all components appearing in $\mathcal{E}_{i}$.

###### Proof

Let $\mathcal{E}_{a}$ and $\mathcal{E}_{b}$ be two component-based grammars in
$\mathcal{E}_{1\ldots p}$. By Lemma 1, we have that
$\mathcal{E}_{a}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{b}\mathrel{\leavevmode\resizebox{22.50003pt}{4.75006pt}{$\;\implies\;$}}\textnormal{{components}}(\mathcal{E}_{1})\mathrel{\raisebox{0.5pt}{$\subseteq$}}\textnormal{{components}}(\mathcal{E}_{2})$.
The claim then immediately follows from Definition 9. ∎

######  Definition 10 ($\bm{j^{k}}$-Uniqueness)

Given grammars
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\cdots\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{p}$,
we say that an expression $e$ of size $k$ is $j^{k}$-unique with respect to
$\mathcal{E}_{1\ldots p}$ if it is contained in $\mathcal{E}_{j}$ but not in
$\mathcal{E}_{(j-1)}$. We define
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$ as
the maximal such set of expressions, i.e.,

$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\;\mathrel{\overset{\makebox[0.0pt]{\mbox{\tiny
def}}}{=}}\;\left\\{e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\;\mid\;\text{\sf
size}(e)=k\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}\right\\}$

###### Lemma 2

Let
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\cdots\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{p}$
be $p$ component-based grammars. Then, for any expression
$o(e_{1},\ldots,e_{a})\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}$, if the operator $o$ belongs to
$\textnormal{{operators}}(\mathcal{E}_{q})$ such that $q<j$, at least one
argument must belong to $\mathcal{E}_{j}$ but not $\mathcal{E}_{(j-1)}$, i.e.,

$o\mathrel{\raisebox{0.5pt}{$\in$}}\textnormal{{operators}}(\mathcal{E}_{q})\,\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\,q<j\;\mathrel{\leavevmode\resizebox{22.50003pt}{4.75006pt}{$\;\implies\;$}}\;\exists\,e\mathrel{\raisebox{0.5pt}{$\in$}}e\raisebox{-1.99997pt}{\scalebox{0.65}{$1\ldots
a$}}\colon
e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}$

###### Proof

Consider an arbitrary expression
$e_{\ast}=o(e_{1},\ldots,e_{a})\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}$ such that
$o\mathrel{\raisebox{0.5pt}{$\in$}}\textnormal{{operators}}(\mathcal{E}_{q})\;\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}\;q<j$.
Suppose
$\left[\forall\,e\mathrel{\raisebox{0.5pt}{$\in$}}e\raisebox{-1.99997pt}{\scalebox{0.65}{$1\ldots
a$}}\colon
e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\,\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\vee$}}}\,e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}\right]$.
Then, for any argument subexpression $e$, we have the following three
possibilities:

  * ✗

$e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\,\wedge\,e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}$
is impossible since
$\mathcal{E}_{(j-1)}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{j}$.

  * ✗

$e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\,\wedge\,e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}$
is also impossible, by Definition 8, due to the closure property of component-
based grammars.

  * ✗

$e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\,\wedge\,e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}$
must be false for at least one argument subexpression. Otherwise, since
$o\mathrel{\raisebox{0.5pt}{$\in$}}\textnormal{{operators}}(\mathcal{E}_{(j-1)})$
and $\mathcal{E}_{(j-1)}$ is closed under operator application by Definition
8, $e_{\ast}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}$ must be
true. However, by Definition 10, we have that
$e_{\ast}\mathrel{\raisebox{0.5pt}{$\in$}}\,\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\mathrel{\leavevmode\resizebox{22.50003pt}{4.75006pt}{$\;\implies\;$}}e_{\ast}\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}$.

Therefore, our assumption
$\left[\forall\,e\mathrel{\raisebox{0.5pt}{$\in$}}e\raisebox{-1.99997pt}{\scalebox{0.65}{$1\ldots
a$}}\colon
e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j}\,\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\vee$}}}\,e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{(j-1)}\right]$
must be false. ∎

###### Lemma 3

Let $\mathcal{E}_{0}=\\{\\}$ and
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\cdots\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{p}$
be $p$ component-based grammars. Then, for any $l\geq 1$ and any operator
$o\mathrel{\raisebox{0.5pt}{$\in$}}\textnormal{{operators}}(\mathcal{E}_{l})\setminus\textnormal{{operators}}(\mathcal{E}_{l-1})$
of arity $a$, $\textnormal{{Divide}}(a,k-1,l,j,\langle\rangle)$ generates the
following set $L$ of all possible distinct locations for selecting the
arguments for $o$ such that
$o(e_{1},\ldots,e_{a})\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}$:

$\begin{array}[]{rcl}L=\Big{\\{}\\!\big{\langle}(j_{1},k_{1}),\ldots,(j_{a},k_{a})\big{\rangle}&\scalebox{1.45}{$\mid$}&o(e_{1},\ldots,e_{a})\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\\\\[2.5pt]
&\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\wedge$}}}&\forall\,1\leq
i\leq a\colon
e_{i}\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j_{i}}^{k_{i}}\Big{\\}}\end{array}$

###### Proof

In lines 7–9 of Footnote 8, the top-level
$\textsc{Divide}(a,k-1,l,j,\langle\rangle)$ call first recursively creates a
call tree of height $a-1$ such that the accumulator $\alpha$ at each leaf node
contains the locations for selecting the last $a-1$ arguments from. Since $u$
in line $7$ ranges over $\\{1,\ldots,j\\}$ and $v$ in line $8$ ranges over
$\\{1,\ldots,(k-2)\\}$, the call tree must be exhaustive by construction.
Concretely, the values of $\alpha$ at the the leaf nodes must capture every
possible sequence of $a-1$ locations,
$\left\langle(j_{1},k_{1}),\ldots,(j_{(a-1)},k_{(a-1)})\right\rangle$, such
that $k_{1}+\cdots+k_{(a-1)}\leq k-2$.

Finally at the leaf nodes of the call tree, lines 4–5 are triggered to select
locations for the first argument. The naïve approach of simply assigning the
remaining size to each grammar in $\mathcal{E}_{1\ldots j}$ would be
exhaustive, but may lead to enumerating other expressions
$o(e_{1},\ldots,e_{a})\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}$ when $l<j$. Therefore, we check if $l<j$ and no location
$(x,y)$ in $\alpha$ satisfies $x=j$, in which case we assign the remaining
size to only $\mathcal{E}_{j}$ in line $5$. Lemma 2 shows that this check is
sufficient to guarantee that we only enumerate expressions in
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$. ∎

######  Theorem 0.A.8 (HEnum is Complete up to Size $\bm{q}$)

Given a SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, let
$\mathcal{E}_{1\ldots p}$ be component-based grammars over theory $\mathbb{T}$
such that
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}=\mathcal{E}$,
$\mathrel{\textnormal{$\triangleleft$}}$ be a well order on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$, and $q\geq 0$ be an upper bound on
size of expressions. Then, HEnum$(\textsf{S},\mathcal{E}_{1\ldots
p},\mathrel{\textnormal{$\triangleleft$}},q)$ will eventually find a
satisfying expression if there exists one with size $\leq q$.

###### Proof

First, we observe that every expression
$e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}$ must belong to _some_ maximal
set of $j^{k}$-unique expressions with respect to $\mathcal{E}_{1\ldots p}$:

$\forall\,e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}\colon\;\exists\,j\mathrel{\raisebox{0.5pt}{$\in$}}\\{1,\ldots,p\\}\colon\;\exists\,k\mathrel{\raisebox{0.5pt}{$\in$}}\\{1,\ldots,q\\}\colon\;e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}$

We show that $C[j,k]$ in HEnum (Algorithm 2) stores
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$,
into various $C[j,k][\tau]$ lists based on the expression type $\tau$. Since
HEnum computes $C[j,k]$ for each
$j\mathrel{\raisebox{0.5pt}{$\in$}}\\{1,\ldots,p\\}$ and each
$k\mathrel{\raisebox{0.5pt}{$\in$}}\\{1,\ldots,q\\}$, it must enumerate every
expression in $\mathcal{E}$ with size at most $q$, and thus eventually find
$e$.

The base cases $C[i,1]=\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{i}^{1}$ are straightforward. The inductive case follows from Lemma
3. For each
$(j,k)\mathrel{\raisebox{0.5pt}{$\in$}}\\{1,\ldots,p\\}\times\\{1,\ldots,q\\}$
and each operator in $\mathcal{E}_{1\ldots j}$, we invoke Divide (Footnote 8)
to generate all possible locations for the operator’s arguments such that the
final expression is contained in
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$.
Lines 16–20 in HEnum then populate $C[j,k]$ as
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$ by
applying the operator to subexpressions of appropriate types drawn from these
locations. ∎

###### Lemma 4

Given grammars
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\cdots\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}_{p}$,
for any distinct pairs $(j,k)$ and $(j^{\prime},k^{\prime})$ the sets
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$ and
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j^{\prime}}^{k^{\prime}}$ must be disjoint, i.e.,

$\forall\ j,k,j^{\prime},k^{\prime}\colon\;j\neq
j^{\prime}\operatorname*{\raisebox{-0.50003pt}{\scalebox{1.25}{$\vee$}}}k\neq
k^{\prime}\;\mathrel{\leavevmode\resizebox{22.50003pt}{4.75006pt}{$\;\implies\;$}}\;\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\,\cap\,\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j^{\prime}}^{k^{\prime}}=\\{\\}$

###### Proof

When $k\neq k^{\prime}$, it is straightforward to show that
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\,\cap\,\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j^{\prime}}^{k^{\prime}}=\\{\\}$, since an expression cannot be of
size $k$ and $k^{\prime}$ at the same time.

We now prove the claim for the case when $j\neq j^{\prime}$ by contradiction.
Suppose there exists an expression
$e\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\,\cap\,\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j^{\prime}}^{k}$. Without loss of generality, assume
$j>j^{\prime}$, and therefore
$\mathcal{E}_{j}\supseteq\mathcal{E}_{j^{\prime}}$. But then, by Definition
10, it must be the case that
$e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{E}_{j^{\prime}}$ and thus
$e\not\mathrel{\raisebox{0.5pt}{$\in$}}\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j^{\prime}}^{k}$. Therefore, our assumption that
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j}^{k}\,\cap\,\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots
p}$}\bm{]}_{j^{\prime}}^{k}\neq\\{\\}$ must be false. ∎

######  Theorem 0.A.9 (HEnum is Efficient)

Given a SyGuS problem $\textsf{S}=\left\langle\scalebox{0.95}{$f$}_{\\!X\to
Y}\,|\,\scalebox{0.95}{$\phi,\mathcal{E}$}\right\rangle_{\,\mathbb{T}}$, let
$\mathcal{E}_{1\ldots p}$ be component-based grammars over theory $\mathbb{T}$
such that
$\mathcal{E}_{1}\mathrel{\raisebox{0.5pt}{$\subset$}}\cdots\mathrel{\raisebox{0.5pt}{$\subset$}}\mathcal{E}_{p}\mathrel{\raisebox{0.5pt}{$\subseteq$}}\mathcal{E}$,
$\mathrel{\textnormal{$\triangleleft$}}$ be a well order on
$\mathcal{E}_{1\ldots p}\times\mathbb{N}$, and $q\geq 0$ be an upper bound on
size of expressions. Then, HEnum$(\textsf{S},\mathcal{E}_{1\ldots
p},\mathrel{\textnormal{$\triangleleft$}},q)$ will enumerate each distinct
expression at most once.

###### Proof

As shown in the proof of Theorem 0.A.8, $C[j,k]$ in HEnum (Algorithm 2) stores
$\mathcal{U}\bm{[}\scalebox{0.9}{$\mathcal{E}_{1\ldots p}$}\bm{]}_{j}^{k}$.
Then, by Lemma 4, we immediately have that all pairs $C[j,k]$ and
$C[j^{\prime},k^{\prime}]$ of synthesized expressions are disjoint when $j\neq
j^{\prime}$ or $k\neq k^{\prime}$.

Furthermore, although each $C[j,k]$ is implemented as a list, we show that any
two expressions within any $C[j,k]$ list must be syntactically distinct. The
base cases $C[i,1]$ are straightforward. For the inductive case, observe that
if each list $C[j_{1},k_{1}],\ldots,C[j_{a},k_{a}]$ only contains
syntactically distinct expressions, then all tuples within
$C[j_{1},k_{1}]\times\cdots\times C[j_{a},k_{a}]$ must also be distinct. Thus,
if an operator $o$ with arity $a$ is applied to subexpressions drawn from the
cross product, i.e., $\langle
e_{1},\ldots,e_{a}\rangle\mathrel{\raisebox{0.5pt}{$\in$}}C[j_{1},k_{1}]\times\cdots\times
C[j_{a},k_{a}]$, then all resulting expressions of the form
$o(e_{1},\ldots,e_{a})$ must be syntactically distinct. Thus, by structural
induction, we have that in any list $C[j,k]$ all contained expressions are
syntactically distinct. ∎