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.

翻译：我们探究了LLM与符号工具在程序合成任务上的对比表现。在多个合成领域（包括LTL反应式合成、语法引导合成、分布式协议合成以及递归函数合成）中，我们分别选取了各自领域最先进的符号工具，将其与开源320亿参数的Qwen LLM以及专有前沿模型GPT-5进行比较。针对每个基准测试，我们将Qwen与符号验证器结合，反复运行直至生成通过验证的解或超时为止；GPT-5则每个基准仅运行一次并验证其输出。实验结果表明：在所有领域中，符号工具解决的基准测试数量均多于Qwen，且性能优于或与GPT-5相当；在执行时间方面，符号工具在所有领域均优于GPT-5，并与Qwen持平或极为接近——尽管LLM运行在性能显著更强的硬件平台上。