Can LLMs Perform Synthesis?

TL;DR

This paper compares the effectiveness of large language models and symbolic tools in program synthesis across various domains, finding symbolic tools generally outperform LLMs in both success rate and speed.

Contribution

It provides a systematic comparison of LLMs and symbolic tools on multiple synthesis tasks, highlighting the strengths and limitations of current LLMs in this domain.

Findings

Symbolic tools solve more benchmarks than LLMs.

Symbolic tools are faster than LLMs in all domains.

LLMs perform comparably or worse than symbolic tools in synthesis tasks.

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.