[madPL] SemGuS Reading Group Jun 17

[Liam Hupfer <lhupfer@xxxxxxxx>]

Hi everyone,

For this weekâs SemGuS Reading Group tomorrow (Thursday) at 1pm, Iâm going to be presenting on the paper âSyntax-Guided Synthesis with Quantitative Syntactic Objectivesâ, by Qinheping Hu and Loris DâAntoni (sound familiar?). Join our Zoom meeting!

Abstract

Automatic program synthesis promises to increase the productivity of programmers and end-users of computing devices by automating tedious and error-prone tasks. Despite the practical successes of program synthesis, we still do not have systematic frameworks to synthesize programs that are âgoodâ according to certain metricsâe.g., produce programs of reasonable sizes or with good runtimeâand to understand when synthesis can result in such good programs. In this paper, we propose QSyGuS, a unifying framework for describing syntax-guided synthesis problems with quantitative objectives over the syntax of the synthesized programs. QSyGuS builds on weighted (tree) grammars, a clean and foundational formalism that provides flexible support for different quantitative objectives, useful closure properties, and practical decision procedures. We then present an algorithm for solving QSyGuS. Our algorithm leverages closure properties of weighted grammars to generate intermediate problems that can be solved using non-quantitative SyGuS solvers. Finally, we implement our algorithm in a tool, QuaSi, and evaluate it on 26 quantitative extensions of existing SyGuS benchmarks. QuaSi can synthesize optimal solutions in 15/26 benchmarks with times comparable to those needed to find an arbitrary solution.

âHomework Questionâ

QSyGuS employs weighted grammars in order to differentiate solutions to a SyGuS problem. Given a weighted grammar:

This grammar is designed to differentiate solutions by how many if-then-else expressions they contain. Can you construct a new, non-weighted grammar that effectively limits the above grammar to only those solutions containing 0 or 1 if-then-else expressions? Hint: introduce intermediate terms

See you there!

âLiam Hupfer