Can LLMs Perform Synthesis?

1. Problem Statement

The paper investigates the capability of Large Language Models (LLMs) to perform program synthesis—the automatic generation of systems that satisfy formal correctness specifications—compared to state-of-the-art symbolic synthesis tools.

While LLMs are increasingly used for general code generation, their ability to synthesize programs from formal specifications (e.g., Linear Temporal Logic, SMT constraints, or TLA+ properties) without fine-tuning or complex neurosymbolic integration remains unclear. The authors ask: How do LLMs compare to symbolic tools in terms of success rate and execution time across diverse synthesis domains?

2. Methodology

The authors conducted a comparative evaluation across four distinct synthesis domains, pitting symbolic tools against two LLMs:

• LLMs:
  • Qwen-2.5-Coder-32B-Instruct: A 32B parameter open-source model (state-of-the-art for code generation fitting on a single NVIDIA H200 GPU).
  • GPT-5: A proprietary frontier model (assumed to have significantly more parameters than GPT-3's 175B).
• Symbolic Tools: State-of-the-art tools specific to each domain (e.g., ltlsynt, cvc5, PolySemist, Cataclyst).

Experimental Setup & Fairness

• Hardware: Symbolic tools ran on CPUs (4 cores, 64GB RAM). LLMs ran on powerful GPUs (NVIDIA H200) or via the OpenAI API.
• Time Budget: A uniform 10-minute timeout (15 minutes for recursive synthesis) was applied to the entire toolchain (generation + verification) for each benchmark.
• Verification: All LLM outputs were verified by a symbolic verifier. If verification failed, the process was handled differently for each LLM:
  • Qwen: Used an Iterate-LLM-Until-Solution-or-Timeout (ILST) loop. It generates a candidate, verifies it, and if failed, generates a new one (without feedback on why it failed) until the time limit is reached.
  • GPT-5: Ran once per benchmark. The authors queried it only once to avoid "over-querying" a proprietary, powerful model, simulating a user who checks a single output.
• Constraints: The study used "out-of-the-box" models (no fine-tuning, RAG, or neurosymbolic training) to isolate the raw synthesis capability of the LLMs.

Synthesis Domains

1. LTL Reactive Synthesis: Synthesizing Finite State Machines (FSMs) from Linear Temp Logic (LTL) specs. (Benchmarks: SYNTCOMP 2025).
2. Syntax-Guided Synthesis (SyGuS): Synthesizing programs satisfying specs and grammar constraints. (Benchmarks: cvc5 repository).
3. Distributed Protocol Synthesis (TLA+): Completing sketches of distributed protocols to satisfy TLA+ properties. (Benchmarks: PolySemist suite).
4. Recursive Program Synthesis (ACL2s): Completing sketches of recursive functions in a LISP-like language. (Benchmarks: Cataclyst suite).

3. Key Contributions

• Comprehensive Benchmarking: The first large-scale comparison of frontier LLMs (GPT-5) and strong open-source models (Qwen-32B) against specialized symbolic synthesis tools across four diverse domains.
• Methodological Framework: Introduction of the ILST approach for LLMs, which mimics human trial-and-error or enumerative search without providing counterexample feedback (to avoid neurosymbolic complexity).
• Empirical Evidence: Detailed analysis of success rates, execution times, token costs, and failure modes (syntax vs. semantics).
• Cost Analysis: Quantification of the monetary cost of using proprietary LLMs for synthesis tasks.

4. Experimental Results

Success Rates (Benchmarks Solved)

• LTL Reactive Synthesis:
  • Symbolic (ltlsynt): Solved 396/433 benchmarks.
  • GPT-5: Solved ~229/433 (SMV format) and 150/433 (AIGER format).
  • Qwen: Solved 50/433 (SMV) and 4/433 (AIGER).
  • Finding: Symbolic tools vastly outperformed LLMs in this domain.
• SyGuS:
  • Symbolic (cvc5): Solved 137/148.
  • GPT-5: Solved 143/148 (outperforming the symbolic tool).
  • Qwen: Solved 96/148.
  • Finding: GPT-5 matched or slightly exceeded the symbolic tool; Qwen lagged behind.
• TLA+ Protocol Synthesis:
  • Symbolic (PolySemist): Solved 140/171.
  • GPT-5: Solved 136/171.
  • Qwen: Solved 102/171.
  • Finding: GPT-5 was competitive with the symbolic tool; Qwen struggled more.
• Recursive Synthesis (ACL2s):
  • Symbolic (Cataclyst): Solved 41/42.
  • GPT-5: Solved 41/42.
  • Qwen: Solved 39/42.
  • Finding: All methods performed very well, with GPT-5 and the symbolic tool tied.

Execution Time

• Symbolic tools were consistently faster than LLMs across all domains, despite running on less powerful hardware (CPU vs. GPU/API).
• In LTL synthesis, symbolic tools were two orders of magnitude faster than GPT-5.
• In SyGuS, symbolic tools were one order of magnitude faster.
• Qwen's Iteration Overhead: While Qwen sometimes found solutions faster per attempt, the cumulative time of the ILST loop (including timeouts on failed attempts) often resulted in slower total execution times compared to symbolic tools.

Failure Modes

• Syntax Errors: LLMs frequently generated syntactically invalid code (e.g., malformed JSON, incorrect SMT-LIB syntax, wrong boolean operators). This was a major failure point for Qwen.
• Semantic Errors: LLMs often satisfied the syntax but violated the logical specification.
• Repetition: Qwen frequently repeated the same incorrect solution multiple times during the ILST loop because it was not provided with feedback on why previous attempts failed.
• Token Limits: GPT-5 occasionally hit token budgets, preventing solution generation.

Cost

• The total cost for GPT-5 experiments ranged from $0.80 (Recursive) to $43.97 (LTL AIGER) per domain, highlighting that while feasible, LLM synthesis incurs monetary costs unlike free symbolic tools.

5. Significance and Conclusions

• Symbolic Tools Remain Superior for Hard Synthesis: In domains requiring strict logical guarantees and complex state exploration (like LTL synthesis), symbolic tools are significantly more robust, efficient, and reliable than current LLMs.
• LLMs are Competitive in Specific Niches: In domains with strong structural constraints or where the search space is smaller (SyGuS, Recursive), frontier LLMs (GPT-5) can match or slightly exceed symbolic tools.
• The "Portfolio" Approach: The authors conclude that the most practical approach is a hybrid portfolio: running symbolic tools and LLMs in parallel. Since each method solves a unique subset of benchmarks that the other misses, combining them maximizes coverage.
• Limitations of "Out-of-the-Box" LLMs: Without fine-tuning or neurosymbolic feedback loops (where the LLM learns from counterexamples), LLMs struggle with the rigorous constraints of formal synthesis. They act as "heuristic guessers" rather than "guaranteed solvers."
• Syntax vs. Semantics: LLMs are prone to syntax errors in formal languages, whereas symbolic tools are designed to guarantee syntactic correctness by construction.

Final Verdict: LLMs show promise as synthesis assistants, particularly for easier tasks or as a complementary tool to symbolic solvers, but they do not yet replace symbolic tools for high-assurance, complex program synthesis tasks.