Guiding Enumerative Program Synthesis with Large Language Models
Yixuan Li, Julian Parsert, Elizabeth Polgreen
TL;DR
The paper tackles formal program synthesis under the SyGuS framework by comparing standalone large language models (LLMs) with traditional enumerative solvers and by introducing two hybrid approaches. It first shows that a stand-alone GPT-3.5-based solver solves about 49% of benchmarks, then develops pCFG-synth, which derives a weighted probabilistic CFG from the LLM’s incorrect solutions to guide enumeration, and iLLM-synth, which injects syntactic feedback from the LLM into the enumerative search via helper functions and grammar updates. Empirical results on SyGuS benchmarks demonstrate that these hybrids significantly outperform the stand-alone LLM and a baseline enumerator, with union approaches rivaling or surpassing the state-of-the-art solver cvc5 in several settings. The work highlights that LLMs are most impactful when combined with established formal-search techniques, reinforcing that enumerative synthesis remains a valuable and competitive approach in formal program synthesis.
Abstract
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.