论文标题
在语法引导合成的巨玛群上的梯度下降
Gradient Descent over Metagrammars for Syntax-Guided Synthesis
论文作者
论文摘要
语法引导的合成算法的性能高度取决于提供良好的句法模板或语法。提供此类模板的提供通常留给用户手动进行，尽管在没有这样的语法的情况下，最先进的求解器将提供自己的默认语法，这取决于要进行的目标程序的签名。在这项工作中，我们推测这种默认语法可以大大改善。我们构建了一组规则或巨玛仪，用于构建语法，并对这些群船进行梯度下降，旨在找到一个搜索更多基准和平均更快速度的Metagrammar。我们表明，所得的Metagrammar使CVC4在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.
