Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

要約

大規模な言語モデル（LLM）は、顕著なコード生成機能を実証していますが、生成されたコードの正しさは本質的に信頼できません。
このペーパーでは、LLMが生成したコードの信頼性を確保するために、正式なソフトウェア検証、特にADAのSpark Frameworkを使用する可能性を調査します。
Marmaraganは、既存のプログラムのSpark Annotationsを生成するためにLLMを活用するツールであり、コードの正式な検証を可能にします。
このツールは、キュレーションされた一連のスパークプログラムにベンチマークされており、注釈が選択的に削除されて特定の機能をテストします。
ベンチマークでのGPT-4Oを使用したMarmaraganのパフォーマンスは有望であり、ベンチマークケースの50.7％で正しい注釈が生成されました。
この結果は、LLMの力を正式なソフトウェア検証の信頼性と組み合わせることに関する将来の作業の基盤を確立します。

要約(オリジナル)

Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software verification, specifically the SPARK framework for Ada, to ensure the reliability of LLM-generated code. We present Marmaragan, a tool that leverages an LLM in order to generate SPARK annotations for existing programs, enabling formal verification of the code. The tool is benchmarked on a curated set of SPARK programs, with annotations selectively removed to test specific capabilities. The performance of Marmaragan with GPT-4o on the benchmark is promising, with correct annotations having been generated for 50.7% of the benchmark cases. The results establish a foundation for future work on combining the power of LLMs with the reliability of formal software verification.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google