Overfitting in synthesis: theory and practice

DOI10.1007/978-3-030-25540-4_17MaRDI QIDQ6194583zbMATH OpenOpenAlexFDO

Authors Saswat Padhi, Todd D. Millstein, Aditya V. Nori, Rahul Sharma

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1905.07457

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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 $5imes$ mean speedup.

Recommendations

• Proving unrealizability for syntax-guided synthesis
• Scaling enumerative program synthesis via divide and conquer
• Syntax-guided synthesis with quantitative syntactic objectives
• Counterexample guided inductive synthesis modulo theories
• A theory of formal synthesis via inductive learning

Cited in

(8)

• Toward neural-network-guided program synthesis and verification
• Syntax-guided synthesis for lemma generation in hardware model checking
• Proving unrealizability for syntax-guided synthesis
• Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
• Towards neural-network-guided program synthesis and verification
• A query-based constraint acquisition approach for enhanced precision in program precondition inference
• Constraint-based relational verification
• Decision tree learning in CEGIS-based termination analysis

This page was built for publication: Overfitting in synthesis: theory and practice

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6194583)