一句话：提出多路交集方法，直接合并多个小型版本空间代数，避免中间结果爆炸，显著加速程序合成。
版本空间代数（VSA）是程序合成中表示程序集合的有效数据结构，但其在处理大量 IO 示例时效率低下：典型合成器先为每个示例构造一个 VSA，再逐个求交，而两个 VSA 的交集可能远大于原 VSA，这种膨胀在迭代中累积，使中间 VSA 规模迅速爆炸。本文考察迭代求交过程后发现，尽管中间结果可能巨大，最终 VSA 在实践中通常很小，因为只有少数程序能通过全部示例。基于此，作者提出多路交集方法，直接由多个小型 VSA 求交得到最终结果，绕开构造巨大中间 VSA 的瓶颈；并针对原有算法在多 VSA 场景下的低效，设计了避免大量不必要 VSA 节点的新算法。该方法被集成到两个基于 VSA 的 SOTA 合成器中——一个通用 VSA 合成器和一个面向字符串领域的 Blaze。在 4 个数据集、994 个合成任务上的评估表明，该方法最多多解决 105 个任务，取得 7.36 倍加速。
Version space algebra (VSA) is an effective data structure for representing sets of programs and has been extensively used in program synthesis. Despite this success, a crucial shortcoming of VSA-based synthesis is its inefficiency when processing many examples. Given a set of IO examples, a typical VSA-based synthesizer runs by first constructing an individual VSA for each example and then iteratively intersecting these VSAs one by one. However, the intersection of two VSAs can be much larger than the original ones – this effect accumulates during the iteration, making the scale of intermediate VSAs quickly explode. In this paper, we aim to reduce the cost of intersecting VSAs in synthesis. We investigate the process of the iterative intersection and observe that, although this process may construct some huge intermediate VSAs, its final VSA is usually small in practice because only a few programs can pass all examples. Utilizing this observation, we propose the approach of multi-way intersection , which directly intersects multiple small VSAs into the final result, thus avoiding the previous bottleneck of constructing huge intermediate VSAs. Furthermore, since the previous intersection algorithm is inefficient for multiple VSAs, we design a novel algorithm to avoid most unnecessary VSA nodes. We integrated our approach into two SOTA VSA-based synthesizers: a general synthesizer based on VSA and a specialized one for the string domain Blaze. We evaluate them over 4 different datasets, 994 synthesis tasks; the results show that our approach can significantly improve the performance of VSA-based synthesis, with up to 105 more tasks solved and a speedup of 7.36×.
@article{paperbot2984,
title = {Tunneling through the Hill: Multi-way Intersection for Version-Space Algebras in Program Synthesis},
author = {Guanlin Chen and Ruyi Ji and Shuhao Zhang and Yingfei Xiong},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763176}
}