基于元文法的梯度下降语法引导综合
Gradient Descent over Metagrammars for Syntax-Guided Synthesis
摘要：
语法引导的合成算法的性能高度依赖于提供良好的语法模板或语法。这种模板的提供通常留给用户手动完成，尽管在缺少这种语法的情况下，最先进的求解器将提供它们自己的默认语法，这取决于要被合成的目标程序的签名。在这项工作中，我们推测这种默认语法可以大大改善。我们建立了一套规则，或元文法，用于构造语法，并对这些元文法执行梯度下降，旨在找到一个元文法，解决更多的基准和平均更快。我们所得到的元语法使CVC 4能够在300秒的超时内解决比默认语法多26%的基准测试，并且元语法从数十个基准测试中学习到100个基准测试的性能。
英文摘要：
The performance of a syntax-guided synthesis algorithm is highly dependent on the provision of a good syntactic template, or grammar. Provision of such a template is often left to the user to do manually, though in the absence of such a grammar, state-of-the-art solvers will provide their own default grammar, which is dependent on the signature of the target program to be sythesized. In this work, we speculate this default grammar could be improved upon substantially. We build sets of rules, or metagrammars, for constructing grammars, and perform a gradient descent over these metagrammars aiming to find a metagrammar which solves more benchmarks and on average faster. We show the resulting metagrammar enables CVC4 to solve 26% more benchmarks than the default grammar within a 300s time-out, and that metagrammars learnt from tens of benchmarks generalize to performance on 100s of benchmarks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
