一句话：融合项图枚举、示例过滤、LLM 优先级与自底向上推导，提升位向量语法引导合成性能。
语法引导合成在多种计算机辅助编程系统中广泛应用，但位向量合成仍面临独特挑战，现有方法尚未充分解决。本文提出一种新的合成方法，采用基于多种因素的枚举策略：利用项图枚举衡量子表达式递归，通过示例引导过滤避免无用候选，借助大语言模型优先选择有价值组件，并加入自底向上演绎步骤以处理有助于演绎求解的子问题。作者将这些增强枚举技术实现于 SyGuS 求解器 DryadSynth。评估表明，该求解器在求解问题数量、执行时间和解的大小上优于当前最优求解器，并首次成功求解 31 个合成问题，其中包括 5 个著名的 Hacker's Delight 问题。
Syntax-guided synthesis has been a prevalent theme in various computer-aided programming systems. However, the domain of bit-vector synthesis poses several unique challenges that have not yet been sufficiently addressed and resolved. In this paper, we propose a novel synthesis approach that incorporates a distinct enumeration strategy based on various factors. Technically, this approach weighs in subexpression recurrence by term-graph-based enumeration, avoids useless candidates by example-guided filtration, prioritizes valuable components identified by large language models. This approach also incorporates a bottom-up deduction step to enhance the enumeration algorithm by considering subproblems that contribute to the deductive resolution. We implement all the enhanced enumeration techniques in our S y G u S solver D ryad S ynth , which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, D ryad S ynth successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker’s Delight problems.
@article{paperbot2627,
title = {Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations},
author = {Yuantian Ding and Xiaokang Qiu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632913}
}