一句话:提出距离引导搜索,用不完美的 LLM 生成程序启发自顶向下与自底向上合成,提升程序合成的可扩展性。
基于搜索的程序合成系统通过系统化探索程序空间来满足规约,但受组合爆炸影响难以扩展;大语言模型能生成较大程序,却常给出错误或不满足规约的解。本文提出距离引导搜索算法,利用不完美的 LLM 生成程序同时引导自顶向下与自底向上合成。该方法使用基于 anti-unification 的距离度量,在自顶向下搜索中优先选择与 LLM 输出结构相似的候选;在自底向上合成中,生成与 LLM 解的子表达式接近的组件,同时保持完备性与剪枝效率。作者在递归函数程序双向合成器 Trio 上实现该技术,并在 80 个合成任务上评估。结果表明,距离引导搜索有效结合了 LLM 与搜索式方法的优势,可解决任一技术单独无法完成的任务。
Search-based program synthesis systematically explores a space of programs to find one that satisfies a given specification. While effective for small programs, it struggles with scalability due to the combinatorial explosion of the search space. In contrast, large language models (LLMs) can generate large programs but often produce solutions that are incorrect or fail to meet the specification. We propose a novel distance-guided search algorithm that leverages imperfect LLM-generated programs to guide both top-down and bottom-up synthesis. Using an anti-unification-based distance metric, we prioritize candidates in the top-down search that are structurally similar to the LLM output. For bottom-up synthesis, we generate components close to subexpressions of the LLM solution while preserving completeness and pruning efficiency. We implement our approach atop Trio, a bidirectional synthesizer for recursive functional programs, and evaluate it on 80 synthesis tasks. Our results show that distance-guided search effectively combines the strengths of LLMs and search-based methods, solving tasks beyond the reach of either technique alone.