Guiding Enumerative Program Synthesis with Large Language Models
arxiv(2024)
摘要
Pre-trained Large Language Models (LLMs) are beginning to dominate the
discourse around automatic code generation with natural language
specifications. In contrast, the best-performing synthesizers in the domain of
formal synthesis with precise logical specifications are still based on
enumerative algorithms. In this paper, we evaluate the abilities of LLMs to
solve formal synthesis benchmarks by carefully crafting a library of prompts
for the domain. When one-shot synthesis fails, we propose a novel enumerative
synthesis algorithm, which integrates calls to an LLM into a weighted
probabilistic search. This allows the synthesizer to provide the LLM with
information about the progress of the enumerator, and the LLM to provide the
enumerator with syntactic guidance in an iterative loop. We evaluate our
techniques on benchmarks from the Syntax-Guided Synthesis (SyGuS) competition.
We find that GPT-3.5 as a stand-alone tool for formal synthesis is easily
outperformed by state-of-the-art formal synthesis algorithms, but our approach
integrating the LLM into an enumerative synthesis algorithm shows significant
performance gains over both the LLM and the enumerative synthesizer alone and
the winning SyGuS competition tool.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要