Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis

William Murphy, Nikolaus Holzer, Feitong Qiao, Leyi Cui, Raven Rothkopf, Nathan Koenig, Mark Santolucito

TL;DR

This work introduces a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis, and shows that the method allows the pipeline to solve problems previously intractable for LLM code generation.

Abstract

In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.

Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis

TL;DR

This work introduces a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis, and shows that the method allows the pipeline to solve problems previously intractable for LLM code generation.

Abstract

In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.

Paper Structure

This paper contains 18 sections, 2 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. LLM Code Generation
  4. Formal Synthesis
  5. Using LLMs and Formal Synthesis
  6. Zero, few-shot learning and in context learning (ICL)
  7. System Overview
  8. Natural Language (NL) to TSL
  9. Formal Verification Assisted Code Generation
  10. Simplifying Long Context Problems
  11. Evaluation
  12. Testing Methodology
  13. Task Oriented Code Generation
  14. Complex Arbiter Problem Solution Generation
  15. Results
  16. ...and 3 more sections

Figures (4)

  • Figure 1: Overview of the full TSL + LLM code generation pipeline. The pipeline turns natural language into executable code. Pipeline (a) implements wrapper code to interact with the synthesized code similar to an API. Pipline (b) uses the synthesized code to seed an LLM prompt to generate the program described by the NL descriptions.
  • Figure 2: Examples of the TSL specification interface in both natural language and formal logic.
  • Figure 3: Overview of a reactive system as implemented in a formal TSL specification.
  • Figure 4: Six different project-oriented coding benchmarks that require working implementation of reactive applications and games.