用形式化方法增强大模型代码生成，提升复杂系统可靠性。
Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis
- 将代码生成分为大模型负责部分与形式化方法合成部分
- 在复杂系统上实现大模型单独无法解决的问题
- 适合高安全性场景的自动化代码开发
近年来，大型语言模型（LLMs）在代码生成任务中表现出巨大潜力。然而，其准确性仍不足，缺乏额外监督与验证时难以应用于高风险场景。尤其在处理高度复杂的系统，尤其是包含异常或未见逻辑时，由大模型生成的代码验证成本可能高于手写成本。本文提出一种分治方案：将代码生成任务拆分为由大模型处理的部分和由基于形式化方法的程序合成处理的部分。我们构建了一个基准测试集来评估该方案，结果表明，该方法使原本对大模型不可行的问题变得可解。
原文摘要 · Abstract (English)
In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。