# Guiding Enumerative Program Synthesis with Large Language Models

arXiv: https://arxiv.org/abs/2403.03997 · HTML: https://mlsanity.com/paper/2403.03997/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 45 references that are in the map.
- First posted on arXiv 6 Mar 2024.

## Builds on (most cited first, 23 of 23)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Sparks of Artificial General Intelligence: Early experiments with GPT-4](https://mlsanity.com/paper/2303.12712/) (2023)
- [LLM-Planner: Few-Shot Grounded Planning for Embodied Agents with Large Language Models](https://mlsanity.com/paper/2212.04088/) (2022)
- [Asleep at the Keyboard? Assessing the Security of GitHub Copilot's Code Contributions](https://mlsanity.com/paper/2108.09293/) (2021)
- [Do Users Write More Insecure Code with AI Assistants?](https://mlsanity.com/paper/2211.03622/) (2022)
- [DeepCoder: Learning to Write Programs](https://mlsanity.com/paper/1611.01989/) (2016)
- [Large Language Models Understand and Can be Enhanced by Emotional Stimuli](https://mlsanity.com/paper/2307.11760/) (2023)
- [An Empirical Study of the Non-determinism of ChatGPT in Code Generation](https://mlsanity.com/paper/2308.02828/) (2023)
- [Jigsaw: Large Language Models meet Program Synthesis](https://mlsanity.com/paper/2112.02969/) (2021)
- [Lost at C: A User Study on the Security Implications of Large Language Model Code Assistants](https://mlsanity.com/paper/2208.09727/) (2022)
- [Leveraging Grammar and Reinforcement Learning for Neural Program Synthesis](https://mlsanity.com/paper/1805.04276/) (2018)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Lemur: Integrating Large Language Models in Automated Program Verification](https://mlsanity.com/paper/2310.04870/) (2023)
- [Finding Inductive Loop Invariants using Large Language Models](https://mlsanity.com/paper/2311.07948/) (2023)
- [Program Synthesis using Conflict-Driven Learning](https://mlsanity.com/paper/1711.08029/) (2017)
- [A Theory of Formal Synthesis via Inductive Learning](https://mlsanity.com/paper/1505.03953/) (2015)
- [Using SyGuS to Synthesize Reactive Motion Plans](https://mlsanity.com/paper/1611.07620/) (2016)
- [Reinforcement Learning and Data-Generation for Syntax-Guided Synthesis](https://mlsanity.com/paper/2307.09564/) (2023)
- [Grammar Filtering For Syntax-Guided Synthesis](https://mlsanity.com/paper/2002.02884/) (2020)
- [Using Program Synthesis for Program Analysis](https://mlsanity.com/paper/1508.07829/) (2015)

## Built on by (most cited first, 9 of 9)

- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generation](https://mlsanity.com/paper/2502.05344/) (2025)
- [An LLM-enabled Multi-Agent Autonomous Mechatronics Design Framework](https://mlsanity.com/paper/2504.14681/) (2025)
- [FormalJudge: A Neuro-Symbolic Paradigm for Agentic Oversight](https://mlsanity.com/paper/2602.11136/) (2026)
- [Engineering Systems for Data Analysis Using Interactive Structured Inductive Programming](https://mlsanity.com/paper/2503.14488/) (2025)
- [EcoSearch: A Constant-Delay Best-First Search Algorithm for Program Synthesis](https://mlsanity.com/paper/2412.17330/) (2024)
- [On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability](https://mlsanity.com/paper/2509.09194/) (2025)
- [AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution](https://mlsanity.com/paper/2512.07501/) (2025)
- [AlgoEvolve: LLM-driven Meta-evolution of Algorithmic Trading Programs](https://mlsanity.com/paper/2606.26173/) (2026)

## Abstract (arXiv)

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.