一句话：提出首个并发字符串变换合成算法，通过异步协调演绎与枚举过程，并实现工具 Synthphonia 显著提升性能。
程序合成面临任务复杂、意图与实现相互制约等挑战，已有工作多通过并行化搜索空间引入基础并发，尚未处理相互依赖的子问题。本文以字符串变换为对象，提出首个并发合成算法：让演绎与枚举过程异步协调，包含可动态分解任务的异步演绎器、响应枚举请求的通用枚举器，以及用于 if-then-else 条件/分支搜索与组装的累积式分例器。实现 Synthphonia 在多个挑战性字符串变换任务上较当前最优合成器取得显著性能提升，并首次成功求解 116 个任务。
Program synthesis aims at the automatic generation of programs based on given specifications. Despite significant progress, the inherent complexity of synthesis tasks and the interplay among intention, invention and adaptation limit its scope. A promising yet challenging avenue is the integration of concurrency to enhance synthesis algorithms. While some efforts have applied basic concurrency by parallelizing search spaces, more intricate synthesis scenarios involving interdependent subproblems remain unexplored. In this paper, we focus on string transformation as the target domain and introduce the first concurrent synthesis algorithm that enables asynchronous coordination between deductive and enumerative processes, featuring an asynchronous deducer for dynamic task decomposition, a versatile enumerator for resolving enumeration requests, and an accumulative case splitter for if-then-else condition/branch search and assembling. Our implementation, Synthphonia exhibits substantial performance improvements over state-of-the-art synthesizers, successfully solving 116 challenging string transformation tasks for the first time.
@article{paperbot3119,
title = {A Concurrent Approach to String Transformation Synthesis},
author = {Yuantian Ding and Xiaokang Qiu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729336}
}