Can LLMs Perform Synthesis?

这是一份关于论文《Can LLMs Perform Synthesis?》（大语言模型能执行合成吗？）的详细技术总结。该论文由东北大学的 Derek Egolf、Yuhao Zhou 和 Stavros Tripakis 撰写。

1. 研究问题与背景

核心问题：大语言模型（LLM）在程序合成任务上的表现如何？它们能否与最先进的符号化（Symbolic）合成工具相媲美？
背景：

• 程序合成旨在自动生成满足特定正确性规范的系统。
• 近年来，LLM 在通用代码生成任务中表现出色。
• 然而，LLM 是否具备从形式化规范（Formal Specifications）自动生成正确程序的能力，尚缺乏系统性的评估，特别是与传统的符号化合成工具（如基于 SAT/SMT/模型检测的工具）进行对比时。

2. 研究方法与实验设计

2.1 评估领域 (Synthesis Domains)

作者在四个不同的合成领域进行了评估，涵盖了从硬件电路到分布式协议和递归函数：

1. LTL 反应式合成 (LTL Reactive Synthesis)：根据线性时序逻辑（LTL）规范合成有限状态机（FSM）。
2. 语法引导合成 (SyGuS)：根据语法约束和规范合成程序。
3. 分布式协议合成 (Distributed Protocol Synthesis)：基于 TLA+ 草图（Sketch）补全分布式协议。
4. 递归程序合成 (Recursive Program Synthesis)：基于 ACL2s 语言的草图和逻辑规范合成递归函数。

2.2 对比工具

• 符号化工具 (Symbolic Tools)：
  • LTL: ltlsynt (SYNTCOMP 2025 冠军)
  • SyGuS: cvc5
  • 协议合成: PolySemist
  • 递归合成: Cataclyst
• 大语言模型 (LLMs)：
  • Qwen-2.5-Coder-32B：开源模型，320 亿参数，运行在 NVIDIA H200 GPU 上。
  • GPT-5：闭源前沿模型（参数未公开，推测远超 GPT-3 的 1750 亿），通过 API 调用。

2.3 实验设置与公平性考量

• LLM 使用策略：
  • Qwen：采用 ILST (Iterate-LLM-Until-Solution-or-Timeout) 策略。即：生成候选 -> 符号化验证器检查 -> 若失败则重新生成（不向 LLM 提供具体的反例反馈，仅重试），直到找到解或超时。
  • GPT-5：每个基准测试仅运行一次生成，然后进行验证。这是为了平衡资源，因为 GPT-5 单次生成能力极强且运行在更强大的硬件上。
  • 验证器：所有 LLM 生成的输出都必须经过独立的符号化验证器（如 nuXmv, Z3, TLC, ACL2s 等）检查，确保满足规范。
• 资源分配：
  • 所有工具链均设定了相同的超时时间（通常为 10 分钟，递归合成为 15 分钟）。
  • 尽管 LLM 运行在 GPU 上而符号工具运行在 CPU 上，作者试图通过限制 GPT-5 的调用次数（单次）来平衡计算资源，尽管作者承认这仍可能存在不公平（Qwen 利用了 GPU 的并行重试能力）。
• 提示工程 (Prompting)：使用了严格的提示词，要求 LLM 输出特定格式（如 AIGER, SMV, SMT-LIB, JSON 等），并包含语法约束，但不使用微调（Fine-tuning）或检索增强生成（RAG）。

3. 主要实验结果

3.1 解决能力 (Solved Benchmarks)

• 总体趋势：在所有领域，符号化工具解决的基准测试数量均多于 Qwen。
• LTL 合成：符号工具 ltlsynt 表现显著优于 LLM。ltlsynt 解决了 354+42 个基准，而 Qwen 仅解决了个位数（SMV 格式 50 个，AIGER 格式 4 个），GPT-5 解决了 150-229 个（取决于格式）。
• SyGuS：cvc5 解决了 137 个，GPT-5 解决了 143 个（略优于 cvc5），Qwen 解决了 96 个。
• 协议合成：PolySemist 解决了 140 个，GPT-5 解决了 136 个，Qwen 解决了 102 个。
• 递归合成：Cataclyst 和 GPT-5 均解决了 41/42 个，Qwen 解决了 39 个。
• 互补性：存在一部分基准测试是 LLM 能解决但符号工具不能，反之亦然。这表明**组合使用（Portfolio Approach）**可能更有效。

3.2 执行时间 (Execution Time)

• 符号工具显著更快：
  • 在 LTL 和 SyGuS 领域，符号工具比 GPT-5 快1-2 个数量级。
  • 即使在 Qwen 运行在更强大的 GPU 上，符号工具在大多数领域（除递归合成外）的总执行时间（包括超时情况）仍优于或接近 Qwen。
  • 原因：符号工具通过枚举和剪枝高效搜索，而 LLM 需要多次生成和验证，且容易陷入重复生成错误答案的循环。

3.3 错误类型与局限性

• 重复生成：Qwen 在 ILST 循环中经常重复生成相同的错误答案（例如在协议合成中，16,824 次响应中有 16,722 次失败，且大量重复）。
• 语法错误：Qwen 经常违反严格的语法约束（如 SMV 格式中的非确定性、SMT-LIB 中的非法操作符）。相比之下，GPT-5 在语法合规性上表现更好。
• 语义错误：即使语法正确，LLM 生成的代码也常违反逻辑规范。
• Token 限制：GPT-5 在某些复杂任务中因超出 Token 预算而失败。

4. 关键贡献

1. 系统性评估：首次在同一框架下，跨多个合成领域，将前沿 LLM（包括 GPT-5 和 Qwen）与最先进符号工具进行直接对比。
2. 方法论创新：提出了 ILST 策略（迭代生成直到解决或超时），模拟了用户“生成 - 检查 - 重试”的实际工作流程，并严格区分了“纯 LLM 能力”与“神经符号混合系统”。
3. 揭示差距：明确指出了当前 LLM 在形式化程序合成任务上与专用符号工具的巨大差距，特别是在效率和确定性方面。
4. 数据与基准：提供了详细的实验数据、失败案例分析以及不同格式（AIGER vs SMV）下的性能差异。

5. 结论与意义

• 结论：

  • LLM 目前无法完全替代符号合成工具。在解决率、速度和可靠性上，符号工具仍占主导地位。
  • GPT-5 表现强劲：在 SyGuS、协议合成和递归合成领域，GPT-5 的表现与符号工具相当甚至略优，但在 LTL 合成领域仍落后。
  • Qwen 表现较弱：尽管运行在 GPU 上，Qwen 的解决率和效率均低于符号工具，且容易陷入重复错误的循环。
  • 语法合规是瓶颈：LLM 难以严格遵守复杂的语法和结构约束，这是合成任务失败的主要原因之一。

• 意义：

  • 对研究者的启示：单纯依靠 LLM 进行形式化合成目前不可行。未来的方向应侧重于神经符号（Neurosymbolic）方法，即利用 LLM 作为启发式搜索的引导者（Guidance），而将验证和精确搜索交给符号工具。
  • 对实践者的建议：在需要高可靠性的合成任务中，应优先使用符号工具，或采用“符号工具 + LLM"的并行组合策略（Portfolio），利用 LLM 解决符号工具难以处理的特定案例。
  • 硬件与成本：尽管 LLM 运行在昂贵硬件上，但其单次推理成本高且效率低，而符号工具在 CPU 上即可高效运行。

总结：这篇论文有力地证明了，虽然 LLM 在代码生成方面取得了巨大进步，但在从形式化规范到正确程序的严格合成任务中，它们尚未达到甚至超越传统符号化方法的水平。符号工具在确定性、效率和保证正确性方面仍是不可替代的。