Comparative Synthesis: Learning Optimal Programs with Indeterminate Objectives.

Quantitative program synthesis aims to generate a program that satisfies not only boolean specifications but also quantitative objectives. Nonetheless, obtaining precise quantitative objectives per se can be a challenging task. In this paper, we propose comparative synthesis, a bootstrapping quantitative synthesis framework in which an indeterminate objective and a satisfying program are synthesized in tandem. The key idea is to make comparative queries to learn the user's preference over candidate programs, with which objectives can be conjectured. These objectives, which are indeterminate as they can be refined along the course of user interaction, guide the search of satisfying programs. Within the comparative synthesis framework, we developed two novel comparative synthesis procedures (CLPs) with the aim of minimizing the number of queries to the user. We prove that both CLPs converge and use them in two case studies: generating bandwidth allocations for network design and solving SyGuS benchmarks with syntactic objectives. Experiments show that our framework can successfully synthesize satisfying/optimal solutions by making queries only, without a priori knowledge about the quantitative objective.