Overfitting in Synthesis: Theory and Practice
Overfitting in Synthesis: Theory and Practice
复制标题
综合中的过度拟合：理论与实践
DOI：
10.1007/978-3-030-25540-4_17
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Sharma, Rahul
中科院分区：
文献类型：
--
作者：
Padhi, Saswat;Millstein, Todd;Nori, Aditya;Sharma, Rahul
在syntax-guided synthesis（SyGuS）中，synthesizer的目标是自动生成一个程序，该程序属于满足逻辑规范的可能实现的语法。我们调查了一个共同的限制，在国家的最先进的SyGuS工具，执行反例引导归纳合成（CEGIS）。我们根据经验观察到，随着所提供的语法的表达能力的增加，这些工具的性能显着下降。我们声称，这种下降不仅是由于更大的搜索空间，但也由于tooverfitting。我们正式定义了这种现象和Proveno-free-lunchtheorems，揭示了合成器性能和语法表达之间的基本权衡。在机器学习中减轻过拟合的标准方法是并行运行具有不同表达能力的多个学习器。我们证明，这种见解可以立即受益于现有的SyGuS工具。我们还提出了一种新的单线程技术，称为混合枚举，它交织不同的语法，并优于2018年SyGuS竞赛（Invtrack）的赢家，解决了更多的问题并实现了平均加速。
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 tooverfitting. We formally define this phenomenon and proveno-free-lunchtheorems 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 calledhybrid enumerationthat interleaves different grammars and outperforms the winner of the 2018 SyGuS competition (Invtrack), solving more problems and achieving amean speedup.