Guiding Enumerative Program Synthesis with Large Language Models

• URL: http://arxiv.org/abs/2403.03997v2
• Date: Mon, 27 May 2024 12:18:40 GMT
• Title: Guiding Enumerative Program Synthesis with Large Language Models
• Authors: Yixuan Li, Julian Parsert, Elizabeth Polgreen,
• Abstract summary: In this paper, we evaluate the abilities of Large Language Models to solve formal synthesis benchmarks. When one-shot synthesis fails, we propose a novel enumerative synthesis algorithm. 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.
• Score: 15.500250058226474
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• LLM-based Optimization of Compound AI Systems: A Survey [64.39860384538338]
  In a compound AI system, components such as an LLM call, a retriever, a code interpreter, or tools are interconnected. Recent advancements enable end-to-end optimization of these parameters using an LLM. This paper presents a survey of the principles and emerging trends in LLM-based optimization of compound AI systems.
  arXiv  Detail & Related papers  (2024-10-21T18:06:25Z)
• HYSYNTH: Context-Free LLM Approximation for Guiding Program Synthesis [25.260063704712458]
  Large language models (LLMs) often fail to produce fully correct programs in unfamiliar DSLs. Motivated by these limitations, we introduce a hybrid approach, where LLM completions for a given task are used to learn a task-specific, context-free surrogate model. We evaluate this hybrid approach on three domains, and show that it outperforms both unguided search and direct sampling from LLMs, as well as existing program synthesizers.
  arXiv  Detail & Related papers  (2024-05-24T18:45:51Z)
• SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
  We study the synthesis of six datasets, covering topic classification, sentiment analysis, tone detection, and humor. We find that SynthesizRR greatly improves lexical and semantic diversity, similarity to human-written text, and distillation performance.
  arXiv  Detail & Related papers  (2024-05-16T12:22:41Z)
• Mitigating Catastrophic Forgetting in Large Language Models with Self-Synthesized Rehearsal [49.24054920683246]
  Large language models (LLMs) suffer from catastrophic forgetting during continual learning. We propose a framework called Self-Synthesized Rehearsal (SSR) that uses the LLM to generate synthetic instances for rehearsal.
  arXiv  Detail & Related papers  (2024-03-02T16:11:23Z)
• Boosting Large Language Model for Speech Synthesis: An Empirical Study [86.89548753080432]
  Large language models (LLMs) have made significant advancements in natural language processing and are concurrently extending the language ability to other modalities, such as speech and vision. We conduct a comprehensive empirical exploration of boosting LLMs with the ability to generate speech, by combining pre-trained LLM LLaMA/OPT and text-to-speech synthesis model VALL-E. We compare three integration methods between LLMs and speech models, including directly fine-tuned LLMs, superposed layers of LLMs and VALL-E, and coupled LLMs and VALL-E using LLMs as a powerful text encoder
  arXiv  Detail & Related papers  (2023-12-30T14:20:04Z)
• LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
  We introduce LILO, a neurosymbolic framework that iteratively synthesizes, compresses, and documents code. LILO combines LLM-guided program synthesis with recent algorithmic advances in automated from Stitch. We find that AutoDoc boosts performance by helping LILO's synthesizer to interpret and deploy learned abstractions.
  arXiv  Detail & Related papers  (2023-10-30T17:55:02Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• Genetic Algorithms for Searching a Matrix of Metagrammars for Synthesis [19.044613696320628]
  Syntax-guided synthesis is a paradigm in which the search space of candidate solutions is constrained by a syntactic template in the form of a grammar. In this work, we frame the space of syntactic templates as a matrix of rules, and demonstrate how this matrix can be searched effectively with little training data.
  arXiv  Detail & Related papers  (2023-06-01T10:22:22Z)
• ULSA: Unified Language of Synthesis Actions for Representation of Synthesis Protocols [2.436060325115753]
  We propose the first Unified Language of Synthesis Actions (ULSA) for describing synthesis procedures. We created a dataset of 3,040 synthesis procedures annotated by domain experts according to the proposed ULSA scheme.
  arXiv  Detail & Related papers  (2022-01-23T17:44:48Z)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  We use a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize synthesis.
  arXiv  Detail & Related papers  (2019-12-31T17:09:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.