We propose a new synthesis algorithm that can efficiently search programs
with local variables (e.g., those introduced by lambdas). Prior bottom-up
synthesis algorithms are not able to evaluate programs with free local
variables, and therefore cannot effectively reduce the search space of such
programs (e.g., using standard observational equivalence reduction techniques),
making synthesis slow. Our algorithm can reduce the space of programs with
local variables. The key idea, dubbed lifted interpretation, is to lift up the
program interpretation process, from evaluating one program at a time to
simultaneously evaluating all programs from a grammar. Lifted interpretation
provides a mechanism to systematically enumerate all binding contexts for local
variables, thereby enabling us to evaluate and reduce the space of programs
with local variables. Our ideas are instantiated in the domain of web
automation. The resulting tool, Arborist, can automate a significantly broader
range of challenging tasks more efficiently than state-of-the-art techniques
including WebRobot and Helena.

提出一种新的综合算法，能够有效地搜索具有局部变量（例如，由 lambda 引入的变量）的程序，并通过提升解释机制来评估和减少具有局部变量的程序空间，在 Web 自动化领域表现出比现有技术更高效的广泛自动化能力。

具有局部变量的程序的高效自底向上合成

Efficient Bottom-Up Synthesis for Programs with Local Variables

In runtime verification, manually formalizing a specification for monitoring
system executions is a tedious and error-prone process. To address this issue,
we consider the problem of automatically synthesizing formal specifications
from system executions. To demonstrate our approach, we consider the popular
specification language Metric Temporal Logic (MTL), which is particularly
tailored towards specifying temporal properties for cyber-physical systems
(CPS). Most of the classical approaches for synthesizing temporal logic
formulas aim at minimizing the size of the formula. However, for efficiency in
monitoring, along with the size, the amount of "lookahead" required for the
specification becomes relevant, especially for safety-critical applications. We
formalize this notion and devise a learning algorithm that synthesizes concise
formulas having bounded lookahead. To do so, our algorithm reduces the
synthesis task to a series of satisfiability problems in Linear Real Arithmetic
(LRA) and generates MTL formulas from their satisfying assignments. The
reduction uses a novel encoding of a popular MTL monitoring procedure using
LRA. Finally, we implement our algorithm in a tool called TEAL and demonstrate
its ability to synthesize efficiently monitorable MTL formulas in a CPS
application.

自动从系统执行中合成形式规范的学习算法，以实现有效可监控的 Metric Temporal Logic (MTL) 公式的综合。

度量时态逻辑中高效可监测公式的合成

Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic

This paper presents a new synthesis-based approach for batch image
processing. Unlike existing tools that can only apply global edits to the
entire image, our method can apply fine-grained edits to individual objects
within the image. For example, our method can selectively blur or crop specific
objects that have a certain property. To facilitate such fine-grained image
editing tasks, we propose a neuro-symbolic domain-specific language (DSL) that
combines pre-trained neural networks for image classification with other
language constructs that enable symbolic reasoning. Our method can
automatically learn programs in this DSL from user demonstrations by utilizing
a novel synthesis algorithm. We have implemented the proposed technique in a
tool called ImageEye and evaluated it on 50 image editing tasks. Our evaluation
shows that ImageEye is able to automate 96% of these tasks.

本文介绍了一种新的基于综合的批量图像处理方法，通过利用预训练神经网络和其他语言构造使得对象级别的编辑成为可能，并提出了一种 neuro-symbolic DSL 语言，该方法能够自动学习这种语言，并在该方法的工具 ImageEye 上进行实现并评估，结果显示 ImageEye 能够自动完成 96% 的图像编辑任务。

使用程序合成的批量图像处理 (ImageEye)

ImageEye: Batch Image Processing Using Program Synthesis

In application domains that store data in a tabular format, a common task is
to fill the values of some cells using values stored in other cells. For
instance, such data completion tasks arise in the context of missing value
imputation in data science and derived data computation in spreadsheets and
relational databases. Unfortunately, end-users and data scientists typically
struggle with many data completion tasks that require non-trivial programming
expertise. This paper presents a synthesis technique for automating data
completion tasks using programming-by-example (PBE) and a very lightweight
sketching approach. Given a formula sketch (e.g., AVG($?_1$, $?_2$)) and a few
input-output examples for each hole, our technique synthesizes a program to
automate the desired data completion task. Towards this goal, we propose a
domain-specific language (DSL) that combines spatial and relational reasoning
over tabular data and a novel synthesis algorithm that can generate DSL
programs that are consistent with the input-output examples. The key technical
novelty of our approach is a new version space learning algorithm that is based
on finite tree automata (FTA). The use of FTAs in the learning algorithm leads
to a more compact representation that allows more sharing between programs that
are consistent with the examples. We have implemented the proposed approach in
a tool called DACE and evaluate it on 84 benchmarks taken from online help
forums. We also illustrate the advantages of our approach by comparing our
technique against two existing synthesizers, namely PROSE and SKETCH.

本文提出了一种基于 PBE 的数据自动完成功能综合技术，并通过 DSL 和新颖的综合算法，生成了与输入输出示例一致的 DSL 程序，并将该方法实现在名为 DACE 的工具中。