用大模型生成汽车嵌入式代码，仅靠规范就能产出正确可运行的工业级程序
Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
- 构建spec2code框架，用形式化与自然语言规范驱动大模型迭代生成代码
- 在斯堪尼亚三例真实案例中验证，无需反复优化也能生成符合规范的正确代码
- 适合汽车软件自动化开发、形式化验证初学者快速上手
本文研究如何将大模型代码生成与形式化验证结合，以生成关键嵌入式软件。首个贡献是提出通用框架spec2code，融合多种评判器，实现对大模型的迭代反向提示与微调反馈。第二个贡献是首次可行性研究，采用spec2code的极简版本（无迭代反向提示与微调），在重型车辆制造商Scania的三个工业案例中进行实证评估。目标是从规格说明书自动生成工业级代码。探索了形式化ACSL规范与自然语言规范的不同组合。结果表明，即使不使用迭代反向提示与微调，也能生成符合规范的形式正确代码。
原文摘要 · Abstract (English)
The paper studies how code generation by LLMs can be combined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for iterative backprompting and fine-tuning. The second contribution presents a first feasibility study, where a minimalistic instantiation of spec2code, without iterative backprompting and fine-tuning, is empirically evaluated using three industrial case studies from the heavy vehicle manufacturer Scania. The goal is to automatically generate industrial-quality code from specifications only. Different combinations of formal ACSL specifications and natural language specifications are explored. The results indicate that formally correct code can be generated even without the application of iterative backprompting and fine-tuning.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。