# Overfitting in Synthesis: Theory and Practice (Extended Version)

arXiv: https://arxiv.org/abs/1905.07457 · HTML: https://mlsanity.com/paper/1905.07457/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 May 2019.

## Built on by (most cited first, 6 of 6)

- [SQLucid: Grounding Natural Language Database Queries with Interactive Explanations](https://mlsanity.com/paper/2409.06178/) (2024)
- [Toward Neural-Network-Guided Program Synthesis and Verification](https://mlsanity.com/paper/2103.09414/) (2021)
- [Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes](https://mlsanity.com/paper/2205.14943/) (2022)
- [Program Synthesis as Dependency Quantified Formula Modulo Theory](https://mlsanity.com/paper/2105.09221/) (2021)
- [Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning](https://mlsanity.com/paper/2107.09766/) (2021)
- [Data-driven Verification of Procedural Programs with Integer Arrays](https://mlsanity.com/paper/2505.15958/) (2025)

## Abstract (arXiv)

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× mean speedup.