基于大型语言模型和蒙特卡洛树搜索的多步骤合成验证
内容提要
该文综述大语言模型在程序合成与验证中的研究：LLM4PLC利用用户反馈和外部验证工具提升代码可验证性；结合LLM与静态分析、蒙特卡洛树搜索、测试驱动开发及SMT求解器，迭代生成并修复代码，提高正确性与可靠性，并优化RTL代码生成的功耗、性能与面积。
延伸解读
LLM与形式验证工具结合的价值
文章提到，LLM4PLC通过用户反馈和外部验证工具改善LLM生成代码的可验证性，提高成功生成比例和代码质量。另一项工作将LLM与静态分析结合，在Rust形式验证框架Verus中迭代查询GPT-4，显著减少编写入门级证明代码的人力。这表明，将LLM与形式验证工具结合，能弥补LLM在正确性保证上的不足，尤其适合对可靠性要求高的场景。
蒙特卡洛树搜索在代码生成中的双重角色
文章介绍了蒙特卡洛树搜索（MCTS）在LLM代码生成中的两种应用：一是与自动转换器解码算法结合，用于寄存器传输级（RTL）代码生成，生成可编译、功能正确且功耗性能面积（PPA）优化的代码，在16位加法器设计上实现延迟面积乘积31.8%的改进；二是基于鉴别器引导的MCTS解码，在文本生成中控制约束，避免微调，效果与最先进方法相当。
测试驱动开发与程序综合的可靠性提升
文章提到LLM4TDD方法，利用测试驱动开发指导LLM迭代生成代码，以提高软件系统正确性，并在ChatGPT和LeetCode问题上评估测试、提示和问题属性的影响。另一项工作通过学习分析程序和断言的一致性，判断哪个程序最可能正确，从而提升程序综合器的可靠性和总体准确性。这些方法共同指向通过迭代验证和反馈来增强LLM生成代码的可信度。
Q&A
LLM4PLC 是什么？它如何提升 LLM 生成代码的可验证性？
LLM4PLC 是一种用户引导的迭代流程，通过用户反馈和外部验证工具来改善大型语言模型生成的代码的可验证性，从而提高成功生成的比例并提高代码质量。
如何将大型语言模型与静态分析结合用于形式验证？
基于 LLM 和静态分析相结合，开发了基于 Rust 形式验证框架 Verus 的原型。通过将验证任务分解为多个较小的任务，迭代地查询 GPT-4，并将其输出与轻量级静态分析相结合，显著减少了编写入门级证明代码的人力工作。
蒙特卡洛树搜索如何用于改进 LLM 生成的 RTL 代码？
通过引入蒙特卡洛树搜索，并将其与自动转换器解码算法相结合，以解决现有 LLM 在寄存器传输级代码生成中遇到的问题，从而实现能够生成可编译、功能正确且功耗性能面积优化的代码。经评估，相对于仅使用提示的方法，该技术能一直生成功能正确的代码，并有效解决朴素 LLM 的 PPA 非感知缺陷。对于 16 位加法器，该技术可以在延迟面积乘积方面实现 31.8% 的改进。
LLM4TDD 方法是什么？它如何提高程序综合的正确性？
LLM4TDD 是一种使用测试驱动开发方法，将大型语言模型指导进行迭代式代码生成，以提高软件系统正确性的程序综合方法。通过在 ChatGPT 和 LeetCode 编码问题上进行实证评估，研究不同测试、提示和问题属性对 LLM4TDD 方法有效性的影响。
如何利用大型语言模型和 SMT 求解器生成可验证的正确解决方案？
使用方便的自然语言进行交流，结合生成式大型语言模型和可满足模理论求解器，可以生成可验证的正确解决方案。
在程序合成中，Synthesize、Execute、Debug 方法是如何实现的？
本文探讨了使用大型语言模型进行程序合成时，实现 Synthesize、Execute、Debug 方法的方法，包括替换或修复故障程序，以及不同基于模板和基于模型的提示生成技术，取得了比传统方法更好的表现。
