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