Overfitting in Synthesis: Theory and Practice (Extended Version)

TL;DR

This paper investigates overfitting in syntax-guided synthesis (SyGuS), revealing a fundamental tradeoff between grammar expressiveness and performance, and proposes techniques to mitigate overfitting, improving solver efficiency.

Contribution

It formally defines overfitting in SyGuS, proves no-free-lunch theorems, and introduces a novel hybrid enumeration method that enhances solver performance.

Findings

Performance degrades with increased grammar expressiveness.

Overfitting is a key factor affecting SyGuS solver efficiency.

Hybrid enumeration outperforms existing methods, solving more problems faster.

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.