一句话：利用查询溯源信息引导 CEGIS，从输入输出规约高效合成 Datalog 程序。
本文研究如何从输入-输出规约自动合成 Datalog 程序。作者提出一种溯源引导的方法来扩展反例引导的归纳合成（CEGIS）流程：每轮迭代中，SAT 求解器提出候选 Datalog 程序，Datalog 求解器评估该程序是否满足规约；若不满足，则基于 Datalog 求解器给出的“why”与“why not”溯源信息，学习高效约束并反馈给 SAT 求解器以缩小搜索空间。作者实现了工具 ProSynth，并在来自三个领域的 40 个合成任务上进行实验。结果显示，ProSynth 平均每个任务约 10 秒即可合成目标程序，比现有最优方法快一个数量级，其中 28 个任务耗时不到 1 秒；同时该方法还能合成 invented predicates，并显著降低合成性能的方差。
We propose a new approach to synthesize Datalog programs from input-output specifications. Our approach leverages query provenance to scale the counterexample-guided inductive synthesis (CEGIS) procedure for program synthesis. In each iteration of the procedure, a SAT solver proposes a candidate Datalog program, and a Datalog solver evaluates the proposed program to determine whether it meets the desired specification. Failure to satisfy the specification results in additional constraints to the SAT solver. We propose efficient algorithms to learn these constraints based on “ why ” and “ why not ” provenance information obtained from the Datalog solver. We have implemented our approach in a tool called ProSynth and present experimental results that demonstrate significant improvements over the state-of-the-art, including in synthesizing invented predicates, reducing running times, and in decreasing variances in synthesis performance. On a suite of 40 synthesis tasks from three different domains, ProSynth is able to synthesize the desired program in 10 seconds on average per task—an order of magnitude faster than baseline approaches—and takes only under a second each for 28 of them.
@article{paperbot526,
title = {Provenance-guided synthesis of Datalog programs},
author = {Mukund Raghothaman and Jonathan Mendelson and David Zhao and Mayur Naik and Bernhard Scholz},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371130}
}