Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
复制标题
用于位向量操作的语法引导合成的增强枚举技术
DOI：
10.1145/3632913
复制
发表时间：
2024
影响因子：
--
通讯作者：
Qiu, Xiaokang
中科院分区：
文献类型：
--
作者：
Ding, Yuantian;Qiu, Xiaokang
语法引导合成在各种计算机辅助编程系统中一直是一个流行的主题。然而，位矢量合成领域提出了一些尚未得到充分处理和解决的独特挑战。在本文中，我们提出了一种新的综合方法，该方法结合了基于各种因素的独特枚举策略。从技术上讲，这种方法通过基于词图的枚举来权衡子表达式的递归，通过示例引导的过滤来避免无用的候选，优先考虑由大型语言模型确定的有价值的组件。该方法还包含一个自下而上的演绎步骤，通过考虑有助于演绎解决的子问题来增强枚举算法。我们在SyGuS求解器DryadSynth中实现了所有增强的枚举技术，它在解决问题的数量、执行时间和解决方案大小方面优于最先进的求解器。值得注意的是，DryadSynth首次成功解决了31个合成问题，其中包括5个著名的黑客喜悦问题。
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 SyGuS solver DryadSynth, which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, DryadSynth successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker's Delight problems.
登录
查看更多内容
影响因子：
0.8
作者：
Jinseong Jeon;Xiaokang Qiu;Armando Solar;J. Foster
通讯作者：
J. Foster
DOI：
--
发表时间：
2018-09
期刊：
--
影响因子：
--
作者：
X. Si;Yuan Yang;H. Dai;M. Naik;Le Song
通讯作者：
X. Si;Yuan Yang;H. Dai;M. Naik;Le Song
DOI：
10.34727/2020/isbn.978-3-85448-042-6_29
发表时间：
2020-09
期刊：
2020 Formal Methods in Computer Aided Design (FMCAD)
影响因子：
--
作者：
Aina Niemetz;Mathias Preiner
通讯作者：
Aina Niemetz;Mathias Preiner
DOI：
10.1145/3385412.3386027
发表时间：
2020
期刊：
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Huang, Kangjing;Qiu, Xiaokang;Shen, Peiyuan;Wang, Yanjun
通讯作者：
Wang, Yanjun
影响因子：
--
作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
通讯作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig