paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions

从非递归表达式归纳合成结构递归的函数式程序
POPL 7(POPL)2023匹配度 2/10 · 该论文研究经典归纳程序合成,从输入输出示例合成结构递归函数式程序,属于程序合成/函数式编程方向;它不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户当前关注的研究画像交集很少。引用 19 inbox
Woosuk Lee, Hangyeol Cho
crossref: 2026-09-10

AI 速览

一句话:提出基于块剪枝的归纳合成方法,从输入输出示例合成结构递归的函数式程序,并在 Trio 系统中达到 98% 的基准求解率。

该论文研究如何从输入输出示例归纳合成递归函数式程序。难点在于递归子表达式需要在目标函数尚未完全定义时构造。作者提出“基于块的剪枝”:块指不含递归与条件、由特定输入产生输出的直线代码;先为每个输入输出示例合成尽可能多的块,再搜索递归程序空间并剪除与这些块不一致的候选。方法基于高效的版本空间学习,以处理可能数量巨大的块。此外,作者利用库函数采样得到的输入输出行为,实现目标导向的库函数使用搜索。在 Trio 系统中实现并评估先前工作及新增的合成任务,Trio 能求解 98% 的基准,优于先前工作。

问题
如何从输入输出示例自动合成结构递归的函数式程序,尤其是解决递归子表达式必须在目标函数完整定义前构造的困难。
方法
提出块(无递归、无条件的直线代码)概念,先枚举示例对应的块,再用基于版本空间学习的搜索探索递归程序并用块进行剪枝;同时利用库函数采样行为进行目标导向搜索。
评估
在 Trio 系统中实现,并在先前工作及新合成任务上评测,结果显示在基准套件上达到 98% 的求解率,优于先前方法。
原文摘要(Abstract)

We present a novel approach to synthesizing recursive functional programs from input-output examples. Synthesizing a recursive function is challenging because recursive subexpressions should be constructed while the target function has not been fully defined yet. We address this challenge by using a new technique we call block-based pruning. A block refers to a recursion- and conditional-free expression (i.e., straight-line code) that yields an output from a particular input. We first synthesize as many blocks as possible for each input-output example, and then we explore the space of recursive programs, pruning candidates that are inconsistent with the blocks. Our method is based on an efficient version space learning, thereby effectively dealing with a possibly enormous number of blocks. In addition, we present a method that uses sampled input-output behaviors of library functions to enable a goal-directed search for a recursive program using the library. We have implemented our approach in a system called Trio and evaluated it on synthesis tasks from prior work and on new tasks. Our experiments show that Trio outperforms prior work by synthesizing a solution to 98% of the benchmarks in our benchmark suite.

链接与引用

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

BibTeX
@article{paperbot2073,
  title = {Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions},
  author = {Woosuk Lee and Hangyeol Cho},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {POPL},
  year = {2023},
  doi = {10.1145/3571263}
}