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.

翻译：预训练大型语言模型（LLMs）正逐渐主导基于自然语言规约的自动代码生成领域。相比之下，在具有精确逻辑规约的形式化综合领域，性能最佳的合成器仍基于枚举算法。本文通过精心构建该领域的提示库，评估了LLMs解决形式化综合基准测试的能力。当单次综合失败时，我们提出了一种新颖的枚举式综合算法，该算法将LLM调用集成到加权概率搜索中。这使得合成器能够向LLM提供枚举器的进度信息，而LLM则可在迭代循环中为枚举器提供语法引导。我们在语法引导综合（SyGuS）竞赛的基准测试上评估了我们的技术。研究发现，作为独立的形式化综合工具，GPT-3.5的性能明显落后于最先进的形式化综合算法，但我们将LLM集成到枚举式综合算法中的方法，相较于单独使用LLM、单独使用枚举式合成器以及SyGuS竞赛的优胜工具，均显示出显著的性能提升。