Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software

要約

この論文では、LLM によるコード生成を形式的検証と組み合わせて、重要な組み込みソフトウェアを生成する方法を研究しています。
最初の貢献は、一般的なフレームワーク、spec2code です。このフレームワークでは、LLM が、反復的なバックプロンプトと微調整のためのフィードバックを生成するさまざまな種類の批評家と組み合わされています。
2 番目の寄稿では、最初の実現可能性調査を紹介します。そこでは、反復的なバックプロンプトや微調整を行わない、spec2code の最小限のインスタンス化が、大型車両メーカーである Scania の 3 つの産業用ケーススタディを使用して実証的に評価されています。
目標は、仕様のみから工業品質のコードを自動的に生成することです。
正式な ACSL 仕様と自然言語仕様のさまざまな組み合わせが検討されています。
この結果は、反復的なバックプロンプトや微調整を適用しなくても、形式的に正しいコードが生成できることを示しています。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google