一句话：提出基于关系函数签名的离线算法到在线流式算法的自动合成方法，并实现 Opera。
在线流式算法适合连续数据处理，但通常比离线算法更难设计。本文提出从离线算法自动合成在线流式算法的方法，核心是关系函数签名（RFS）的概念，用以刻画从离线版本推导在线版本的依据。基于 RFS，作者将合成问题分解为若干独立子任务，并结合符号推理与搜索逐个求解。该技术实现为工具 Opera，并在统计计算与在线拍卖两个领域的 50 多个任务上评估。结果显示，Opera 能为 98% 的任务自动导出原始算法的在线版本，并显著优于将 SyGuS 求解器适配到该问题的方案以及 Opera 自身的两个消融变体。
Online streaming algorithms, tailored for continuous data processing, offer substantial benefits but are often more intricate to design than their offline counterparts. This paper introduces a novel approach for automatically synthesizing online streaming algorithms from their offline versions. In particular, we propose a novel methodology, based on the notion of relational function signature (RFS) , for deriving an online algorithm given its offline version. Then, we propose a concrete synthesis algorithm that is an instantiation of the proposed methodology. Our algorithm uses the RFS to decompose the synthesis problem into a set of independent subtasks and uses a combination of symbolic reasoning and search to solve each subproblem. We implement the proposed technique in a new tool called Opera and evaluate it on over 50 tasks spanning two domains: statistical computations and online auctions. Our results show that Opera can automatically derive the online version of the original algorithm for 98% of the tasks. Our experiments also demonstrate that Opera significantly outperforms alternative approaches, including adaptations of SyGuS solvers to this problem as well as two of Opera ’s own ablations.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{WangPPWD24,
title = {From Batch to Stream: Automatic Generation of Online Algorithms},
author = {Ziteng Wang and Shankara Pailoor and Aaryan Prakash and Yuepeng Wang and Işıl Dillig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656418}
}