Syntax-guided synthesis is a paradigm in program synthesis in which the search space of candidate solutions is constrained by a syntactic template in the form of a grammar. These syntactic constraints serve two purposes: constraining the language to the space the user desires, but also rendering the search space tractable for the synthesizer. Given a well-written syntactic template, this is an extremely effective technique. However, this is highly dependent on the user providing such a template: a syntactic template that is too large results in a larger search space and slower synthesis, and a syntactic template that is too small may not contain the solution needed. In this work, we frame the space of syntactic templates as a matrix of rules, and demonstrate how this matrix can be searched effectively with little training data using simple search techniques such as genetic algorithms, giving improvements in both the number of benchmarks solved and solving time for the state-of-the-art synthesis solver.

翻译：语法引导合成是程序合成中的一种范式，其中候选解的搜索空间由语法形式的结构化模板约束。这些语法约束具有双重作用：既将语言限定在用户期望的范围内，又能使搜索空间对于合成器而言易于处理。给定一个精心编写的语法模板，这是一种极为有效的技术。然而，这高度依赖于用户提供此类模板：过大的语法模板会导致搜索空间扩大并降低合成速度，而过小的语法模板则可能无法包含所需的解。在本工作中，我们将语法模板空间构建为规则矩阵，并展示了如何利用少量训练数据，通过遗传算法等简单搜索技术有效搜索该矩阵，从而在解决基准测试数量和解算时间两方面均提升当前最先进合成求解器的性能。