about
Can LLMs Perform Synthesis? (arxiv.org)
4 points by PaulHoule 173 days ago | hide | past | pdf | discuss on HN

In plain words: Program-writing AI models were pitted against the best classic search tools on four kinds of code-generation tasks, with each answer checked by a verifier. The classic tools beat one model outright, matched or beat the other, and were faster in every case.

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.

Derek Egolf, Yuhao Zhou, Stavros Tripakis
arXiv:2603.20264 · cs.PL, cs.LO · submitted Mar 13, 2026
abstract · pdf · html

add comment on HN