一句话：提出离线预合成阶段，用树自动机与 oracle 支撑细粒度抽象语义下的快速剪枝，显著加速程序合成。
抽象语义一直被用于加速基于搜索的程序合成，它可以在不枚举程序的前提下可靠地剪除大量错误程序。直觉上，抽象语义粒度越细，可剪掉的程序越多，合成应当越快；但事实并非如此——粒度提升虽然减少了枚举量，剪枝本身的开销也随之增大，从而对整体合成性能形成根本性瓶颈。本文提出引入一个离线的“预合成”（presynthesis）阶段来打破这一限制，该阶段包含两步：给定带抽象语义的 DSL，第一步语义建模为输入空间构造一棵树自动机 A，使得对任意程序 P 与所考虑的输入 I，A 都存在一条对应 P 在抽象语义下于 I 上执行的运行；第二步为 A 构造 oracle O，使合成过程中能够高效地找出恰好满足给定输入-输出示例的 DSL 程序，从而实现快速剪枝。作者在框架 Foresighter 中实现了该范式，并针对 SQL、字符串变换与矩阵操作给出三个实例，均显著优于各领域先前工作。
Abstract semantics has proven to be instrumental for accelerating search-based program synthesis, by enabling the sound pruning of a set of incorrect programs (without enumerating them). One may expect faster synthesis with increasingly finer-grained abstract semantics. Unfortunately, to the best of our knowledge, this is not the case, yet. The reason is because, as abstraction granularity increases -- while fewer programs are enumerated -- pruning becomes more costly. This imposes a fundamental limit on the overall synthesis performance, which we aim to address in this work. Our key idea is to introduce an offline presynthesis phase, which consists of two steps. Given a DSL with abstract semantics, the first semantics modeling step constructs a tree automaton A for a space of inputs -- such that, for any program P and for any considered input I, A has a run that corresponds to P's execution on I under abstract semantics. Then, the second step builds an oracle O for A. This O enables fast pruning during synthesis, by allowing us to efficiently find exactly those DSL programs that satisfy a given input-output example under abstract semantics. We have implemented this presynthesis-based synthesis paradigm in a framework, Foresighter. On top of it, we have developed three instantiations for SQL, string transformation, and matrix manipulation. All of them significantly outperform prior work in the respective domains.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2604-13290,
title = {Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics},
author = {Rui Dong and Qingyue Wu and Danny Ding and Zheng Guo and Ruyi Ji and Xinyu Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808288}
}