OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification

要約

オペレーティングシステムのカーネル検証タスクに関連する完全な仕様コードを生成する際に、大規模な言語モデル（LLMS）を評価するための新しいベンチマークであるOSVBenchを紹介します。
ベンチマークは、最初に、LLMにプログラミングモデルを提供することにより、構文とセマンティクスの限定範囲内で、仕様生成問題をプログラム合成問題に定義します。
LLMSは、提供された検証の仮定と潜在的な構文とセマンティクス空間を検索し、オペレーティングシステムの高レベルの機能記述のガイダンスの下で潜在的にバグのオペレーティングシステムコードの実装の完全な仕様を生成する必要があります。
このベンチマークは、現実世界のオペレーティングシステムカーネル、ハイパーカーネルの上に構築され、合計245の複雑な仕様生成タスクで構成されており、それぞれが約20k〜30kトークンの長いコンテキストタスクです。
12 LLMの包括的な評価は、オペレーティングシステムの検証のための仕様生成タスクでの現在のLLMの限られたパフォーマンスを示しています。
ベンチマークでのパフォーマンスの大幅な格差は、長いコンテキストコード生成タスクを処理する能力の違いを強調しています。
評価ツールキットとベンチマークは、https：//github.com/lishyu-hkust/osvbenchで入手できます。

要約(オリジナル)

We introduce OSVBench, a new benchmark for evaluating Large Language Models (LLMs) in generating complete specification code pertaining to operating system kernel verification tasks. The benchmark first defines the specification generation problem into a program synthesis problem within a confined scope of syntax and semantics by providing LLMs with the programming model. The LLMs are required to understand the provided verification assumption and the potential syntax and semantics space to search for, then generate the complete specification for the potentially buggy operating system code implementation under the guidance of the high-level functional description of the operating system. This benchmark is built upon a real-world operating system kernel, Hyperkernel, and consists of 245 complex specification generation tasks in total, each is a long context task of about 20k-30k tokens. Our comprehensive evaluation of 12 LLMs exhibits the limited performance of the current LLMs on the specification generation tasks for operating system verification. Significant disparities in their performance on the benchmark highlight differences in their ability to handle long-context code generation tasks. The evaluation toolkit and benchmark are available at https://github.com/lishangyu-hkust/OSVBench.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google