Derek Egolf, Yuhao Zhou, Stavros Tripakis
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.