1. 程序合成技术概述程序合成Program Synthesis是一种自动生成满足给定规范的程序的技术。这项技术最早可以追溯到1950年代Church提出的电路合成问题经过几十年的发展已经从最初的演绎式程序合成扩展到如今的多种方法包括反应式合成、语法引导合成等。1.1 程序合成的核心原理程序合成的核心在于将高级规范转换为可执行的程序实现。这个过程通常涉及规范描述使用形式化语言如LTL、SyGuS-IF等精确描述程序应满足的行为搜索算法在可能的程序空间中寻找满足规范的程序验证机制确保生成的程序确实满足原始规范传统符号工具如ltlsynt、cvc5等通常采用形式化方法和枚举搜索相结合的方式保证生成的程序构造即正确correct by construction。这些工具在特定领域表现出色但往往需要专业的规范编写知识。1.2 大语言模型的兴起与挑战近年来大语言模型LLM在代码生成方面展现出强大能力。GPT-5等模型能够根据自然语言描述生成代码这自然引出一个问题LLM能否用于程序合成与符号工具相比LLM具有以下特点无需精确规范能处理模糊或部分规范泛化能力强可跨领域应用开发门槛低使用自然语言交互然而LLM生成的代码缺乏形式化保证需要额外验证步骤。此外LLM对计算资源的需求远高于传统符号工具。2. 实验设计与方法2.1 对比框架本研究设计了严格的对比实验在四个程序合成领域比较LLM与符号工具的表现LTL反应式合成生成满足线性时序逻辑规范的有限状态机语法引导合成(SyGuS)在给定语法约束下合成满足规范的程序分布式协议合成完成TLA协议草图使其满足性质递归程序合成完成ACL2s中的递归函数草图2.2 评估指标采用以下指标进行公平比较解决能力在规定时间内能解决的基准测试数量执行时间生成正确解所需时间资源消耗计算资源和API调用成本2.3 工具链配置为确保公平性实验采用以下配置工具类型硬件配置超时设置迭代机制符号工具CPU(4核/64GB)10分钟(递归合成15分钟)内置枚举Qwen-32BCPUGPU(H200)同符号工具ILST循环GPT-5OpenAI API同符号工具单次查询其中ILST(Iterate-LLM-until-Solution-or-Timeout)是专为实验设计的迭代机制反复调用LLM直到获得通过验证器的解或超时。3. LTL反应式合成对比3.1 实验设置LTL合成要求根据线性时序逻辑规范生成有限状态机。实验采用SYNTCOMP 2025的433个可实现基准测试比较以下工具符号工具ltlsyntSYNTCOMP 2025冠军LLM工具链QwenAIG/QwenSMV分别生成AIGER和SMV格式GPT-5AIG/GPT-5SMV同上验证流程严格遵循SYNTCOMP标准使用nuXmv进行模型检查。3.2 关键结果工具解决数量平均时间(秒)独特解决数ltlsynt3544.6143QwenAIG479.60QwenSMV50164.91GPT-5AIG150124.02GPT-5SMV229107.03结果显示符号工具ltlsynt优势明显解决了最多基准测试354个GPT-5表现优于Qwen特别是在SMV格式下各工具解决的基准测试存在部分重叠但也有独特解3.3 失败分析QwenSMV在383个未解决的测试中276个生成了最终候选但未验证134个语法错误142个语义错误其余因超时未生成解GPT-5SMV在361个生成解中229个正确51个语法错误40个语义错误41个验证超时4. 语法引导合成(SyGuS)对比4.1 实验设置SyGuS要求在给定语法约束下合成满足规范的程序。实验使用cvc5代码库中的148个基准测试比较符号工具cvc5默认配置LLM工具链Qwen和GPT-5生成SMT-LIB格式验证使用Z3求解器检查语法和语义正确性。4.2 关键结果工具解决数量平均时间(秒)独特解决数cvc51371.84Qwen9627.86GPT-514328.710发现GPT-5表现接近cvc5甚至多解决10个独特基准Qwen落后但仍有独特贡献所有方法共解决147/148个基准4.3 成本分析GPT-5在此领域的API调用成本极低平均输入1340 token输出1609 token总成本仅2.62美元148次查询5. 分布式协议合成对比5.1 实验设置基于TLA的分布式协议合成需要完成协议草图并满足性质。使用171个基准测试比较符号工具PolySemist状态压缩优化LLM工具链Qwen和GPT-5生成TLA补全验证使用TLC模型检查器检查语法和语义。5.2 关键结果工具解决数量平均时间(秒)独特解决数PolySemist14070.9416Qwen10235.031GPT-5136102.2211特别发现放松语法约束后LLM表现提升Qwen从102→133GPT-5从136→149Qwen存在大量重复提案总计16824次响应中7326次重复6. 递归程序合成对比6.1 实验设置在ACL2s中完成递归函数草图满足给定性质和输入输出示例。使用42个基准测试比较符号工具CataclystLLM工具链Qwen和GPT-5验证使用ACL2s反例生成器。6.2 关键结果工具解决数量平均时间(秒)独特解决数Cataclyst4139.111Qwen399.030GPT-54148.330发现所有工具表现接近Qwen在三个基准上失败pairs,split-on,suffixbCataclyst在ternary-tree-eq上失败7. 综合分析与实践建议7.1 性能对比总结综合四个领域的实验结果解决能力符号工具在LTL合成中优势显著其他领域GPT-5与符号工具相当Qwen整体落后但仍有价值执行效率符号工具普遍更快即使LLM使用更强硬件GPT-5比Qwen更高效独特价值各工具都有独特解决的基准实际应用可采用组合策略7.2 实践启示基于实验结果建议LTL合成优先使用符号工具如ltlsyntLLM可作为辅助SyGuSGPT-5与cvc5性能相当可根据成本选择协议合成考虑混合方法结合两者优势递归程序LLM效率更高适合快速原型7.3 优化方向针对LLM在程序合成中的局限未来可探索验证集成更紧密的生成-验证循环提示工程改进规范表达方式领域适应针对特定合成任务的微调资源优化降低LLM的算力需求程序合成领域正面临LLM带来的变革但符号方法仍不可替代。最佳实践可能是两者的有机结合而非非此即彼的选择。
程序合成技术：LLM与符号工具对比研究
发布时间：2026/7/18 18:33:08
1. 程序合成技术概述程序合成Program Synthesis是一种自动生成满足给定规范的程序的技术。这项技术最早可以追溯到1950年代Church提出的电路合成问题经过几十年的发展已经从最初的演绎式程序合成扩展到如今的多种方法包括反应式合成、语法引导合成等。1.1 程序合成的核心原理程序合成的核心在于将高级规范转换为可执行的程序实现。这个过程通常涉及规范描述使用形式化语言如LTL、SyGuS-IF等精确描述程序应满足的行为搜索算法在可能的程序空间中寻找满足规范的程序验证机制确保生成的程序确实满足原始规范传统符号工具如ltlsynt、cvc5等通常采用形式化方法和枚举搜索相结合的方式保证生成的程序构造即正确correct by construction。这些工具在特定领域表现出色但往往需要专业的规范编写知识。1.2 大语言模型的兴起与挑战近年来大语言模型LLM在代码生成方面展现出强大能力。GPT-5等模型能够根据自然语言描述生成代码这自然引出一个问题LLM能否用于程序合成与符号工具相比LLM具有以下特点无需精确规范能处理模糊或部分规范泛化能力强可跨领域应用开发门槛低使用自然语言交互然而LLM生成的代码缺乏形式化保证需要额外验证步骤。此外LLM对计算资源的需求远高于传统符号工具。2. 实验设计与方法2.1 对比框架本研究设计了严格的对比实验在四个程序合成领域比较LLM与符号工具的表现LTL反应式合成生成满足线性时序逻辑规范的有限状态机语法引导合成(SyGuS)在给定语法约束下合成满足规范的程序分布式协议合成完成TLA协议草图使其满足性质递归程序合成完成ACL2s中的递归函数草图2.2 评估指标采用以下指标进行公平比较解决能力在规定时间内能解决的基准测试数量执行时间生成正确解所需时间资源消耗计算资源和API调用成本2.3 工具链配置为确保公平性实验采用以下配置工具类型硬件配置超时设置迭代机制符号工具CPU(4核/64GB)10分钟(递归合成15分钟)内置枚举Qwen-32BCPUGPU(H200)同符号工具ILST循环GPT-5OpenAI API同符号工具单次查询其中ILST(Iterate-LLM-until-Solution-or-Timeout)是专为实验设计的迭代机制反复调用LLM直到获得通过验证器的解或超时。3. LTL反应式合成对比3.1 实验设置LTL合成要求根据线性时序逻辑规范生成有限状态机。实验采用SYNTCOMP 2025的433个可实现基准测试比较以下工具符号工具ltlsyntSYNTCOMP 2025冠军LLM工具链QwenAIG/QwenSMV分别生成AIGER和SMV格式GPT-5AIG/GPT-5SMV同上验证流程严格遵循SYNTCOMP标准使用nuXmv进行模型检查。3.2 关键结果工具解决数量平均时间(秒)独特解决数ltlsynt3544.6143QwenAIG479.60QwenSMV50164.91GPT-5AIG150124.02GPT-5SMV229107.03结果显示符号工具ltlsynt优势明显解决了最多基准测试354个GPT-5表现优于Qwen特别是在SMV格式下各工具解决的基准测试存在部分重叠但也有独特解3.3 失败分析QwenSMV在383个未解决的测试中276个生成了最终候选但未验证134个语法错误142个语义错误其余因超时未生成解GPT-5SMV在361个生成解中229个正确51个语法错误40个语义错误41个验证超时4. 语法引导合成(SyGuS)对比4.1 实验设置SyGuS要求在给定语法约束下合成满足规范的程序。实验使用cvc5代码库中的148个基准测试比较符号工具cvc5默认配置LLM工具链Qwen和GPT-5生成SMT-LIB格式验证使用Z3求解器检查语法和语义正确性。4.2 关键结果工具解决数量平均时间(秒)独特解决数cvc51371.84Qwen9627.86GPT-514328.710发现GPT-5表现接近cvc5甚至多解决10个独特基准Qwen落后但仍有独特贡献所有方法共解决147/148个基准4.3 成本分析GPT-5在此领域的API调用成本极低平均输入1340 token输出1609 token总成本仅2.62美元148次查询5. 分布式协议合成对比5.1 实验设置基于TLA的分布式协议合成需要完成协议草图并满足性质。使用171个基准测试比较符号工具PolySemist状态压缩优化LLM工具链Qwen和GPT-5生成TLA补全验证使用TLC模型检查器检查语法和语义。5.2 关键结果工具解决数量平均时间(秒)独特解决数PolySemist14070.9416Qwen10235.031GPT-5136102.2211特别发现放松语法约束后LLM表现提升Qwen从102→133GPT-5从136→149Qwen存在大量重复提案总计16824次响应中7326次重复6. 递归程序合成对比6.1 实验设置在ACL2s中完成递归函数草图满足给定性质和输入输出示例。使用42个基准测试比较符号工具CataclystLLM工具链Qwen和GPT-5验证使用ACL2s反例生成器。6.2 关键结果工具解决数量平均时间(秒)独特解决数Cataclyst4139.111Qwen399.030GPT-54148.330发现所有工具表现接近Qwen在三个基准上失败pairs,split-on,suffixbCataclyst在ternary-tree-eq上失败7. 综合分析与实践建议7.1 性能对比总结综合四个领域的实验结果解决能力符号工具在LTL合成中优势显著其他领域GPT-5与符号工具相当Qwen整体落后但仍有价值执行效率符号工具普遍更快即使LLM使用更强硬件GPT-5比Qwen更高效独特价值各工具都有独特解决的基准实际应用可采用组合策略7.2 实践启示基于实验结果建议LTL合成优先使用符号工具如ltlsyntLLM可作为辅助SyGuSGPT-5与cvc5性能相当可根据成本选择协议合成考虑混合方法结合两者优势递归程序LLM效率更高适合快速原型7.3 优化方向针对LLM在程序合成中的局限未来可探索验证集成更紧密的生成-验证循环提示工程改进规范表达方式领域适应针对特定合成任务的微调资源优化降低LLM的算力需求程序合成领域正面临LLM带来的变革但符号方法仍不可替代。最佳实践可能是两者的有机结合而非非此即彼的选择。
