Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Can LLMs Perform Synthesis?

Derek Egolf, Yuhao Zhou, Stavros Tripakis

Abstract

How do LLMs compare with symbolic tools on program synthesis tasks? We investigate this question on several synthesis domains: LTL reactive synthesis, syntax-guided synthesis, distributed protocol synthesis, and recursive function synthesis. For each domain, we choose a state-of-the-art symbolic tool and compare it to an open-source, 32 billion parameter version of the Qwen LLM and the proprietary, frontier LLM GPT-5. We couple Qwen with a symbolic verifier and run it repeatedly until it either produces a solution that passes the verifier, or until there is a timeout, for each benchmark. We run GPT-5 once per benchmark and verify the generated output. In all domains, the symbolic tools solve more benchmarks than Qwen and either outperform or are about on par with GPT-5. In terms of execution time, the symbolic tools outperform GPT-5 in all domains, and either outperform or are very close to Qwen, despite the fact that the LLMs are run on significantly more powerful hardware.

Can LLMs Perform Synthesis?

Abstract

How do LLMs compare with symbolic tools on program synthesis tasks? We investigate this question on several synthesis domains: LTL reactive synthesis, syntax-guided synthesis, distributed protocol synthesis, and recursive function synthesis. For each domain, we choose a state-of-the-art symbolic tool and compare it to an open-source, 32 billion parameter version of the Qwen LLM and the proprietary, frontier LLM GPT-5. We couple Qwen with a symbolic verifier and run it repeatedly until it either produces a solution that passes the verifier, or until there is a timeout, for each benchmark. We run GPT-5 once per benchmark and verify the generated output. In all domains, the symbolic tools solve more benchmarks than Qwen and either outperform or are about on par with GPT-5. In terms of execution time, the symbolic tools outperform GPT-5 in all domains, and either outperform or are very close to Qwen, despite the fact that the LLMs are run on significantly more powerful hardware.
Paper Structure (62 sections, 3 figures, 4 tables)

This paper contains 62 sections, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Choice of synthesis domains
  3. Choice and use of LLMs
  4. Methodology and Common Elements Across Domains
  5. Fair comparison
  6. LLM toolchains
  7. LTL Reactive Synthesis
  8. Experimental Setup
  9. Symbolic tool
  10. LLM Toolchains
  11. Prompts
  12. Benchmarks
  13. Hardware and Parameters
  14. Experimental Results
  15. Determinism Checking of LLM SMV Solutions
  16. ...and 47 more sections

Figures (3)

  • Figure 1: LLM-based synthesis methodology: the Qwen toolchain has the reprompt loop, but the GPT-5 toolchain does not (GPT-5 is only queried once per benchmark).
  • Figure 2: If each benchmark is allowed a time budget (x-axis), the plot shows how many benchmarks can be solved (y-axis) within that time by each tool.
  • Figure 3: Checking determinism through self-composition.