paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection

通过高效的问题选择改进 Oracle 引导的归纳合成
OOPSLA 7(OOPSLA1)2023匹配度 2/10 · 论文属于程序合成/OGIS 求解器优化,虽与形式化方法相关,但未涉及用户核心关注的静态分析、LLM/Agent 与静态分析/形式化验证交叉、浮点程序分析或贝叶斯程序分析。引用 6 inbox
Ruyi Ji, Chaozhe Kong, Yingfei Xiong, Zhenjiang Hu
crossref: 2026-09-10

AI 速览

一句话:提出高效且有效的问题选择器 LearnSy,首次普遍提升 OGIS 求解器性能。

Oracle 引导的归纳合成(OGIS)广泛用于程序合成,其中问题选择通过为每轮迭代挑选合适输入来减少迭代次数。已有有效选择器通常把问题选择转化为优化问题,求解耗时,难以满足效率要求。本文提出 LearnSy:将算子复杂行为估计为简单随机事件,给出估计精度的理论结果,并设计高效计算算法。评估表明,在交互式任务中,LearnSy 与现有选择器性能相当但更高效、更通用;在非交互式任务中,可将现有 CEGIS 求解器的时间成本最多降低 43.0%。

问题
OGIS 中如何选择每轮迭代的输入,以既减少迭代次数又保持选择过程高效,从而普遍提升求解器性能。
方法
将问题选择中算子行为估计为简单随机事件,提供估计精度的理论分析,并设计高效计算算法实现 LearnSy 选择器。
评估
在交互式和非交互式任务上评估;交互任务中与已有选择器竞争且更高效、更通用,非交互任务中使 CEGIS 求解器时间最多降低 43.0%。
原文摘要(Abstract)

Oracle-guided inductive synthesis (OGIS) is a widely-used framework to apply program synthesis techniques in practice. The question selection problem aims at reducing the number of iterations in OGIS by selecting a proper input for each OGIS iteration. Theoretically, a question selector can generally improve the performance of OGIS solvers on both interactive and non-interactive tasks if it is not only effective for reducing iterations but also efficient. However, all existing effective question selectors fail in satisfying the requirement of efficiency. To ensure effectiveness, they convert the question selection problem into an optimization one, which is difficult to solve within a short time. In this paper, we propose a novel question selector, named LearnSy . LearnSy is both efficient and effective and thus achieves general improvement for OGIS solvers for the first time. Since we notice that the optimization tasks in previous studies are difficult because of the complex behavior of operators, we estimate these behaviors in LearnSy as simple random events. Subsequently, we provide theoretical results for the precision of this estimation and design an efficient algorithm for its calculation. According to our evaluation, when dealing with interactive tasks, LearnSy can offer competitive performance compared to existing selectors while being more efficient and more general. Moreover, when working on non-interactive tasks, LearnSy can generally reduce the time cost of existing CEGIS solvers by up to 43.0%.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2032,
  title = {Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection},
  author = {Ruyi Ji and Chaozhe Kong and Yingfei Xiong and Zhenjiang Hu},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {OOPSLA1},
  year = {2023},
  doi = {10.1145/3586055}
}