技術概要：BODHI：精密な OS カーネル仕様の推論

問題定義

オペレーティングシステム（OS）カーネルの形式検証は、安全クリティカルなシステムにとって不可欠であるが、精密な形式仕様を構築するために必要な手作業によってボトルネックとなっている。大規模言語モデル（LLM）は一般的なコード生成において有能であることを示してきたが、OS カーネルの形式仕様を合成する能力は依然として限られている。C 言語のシステムコール実装を Python/Z3 の状態機械仕様に変換する能力を評価する OSV-Bench ベンチマークは、顕著な性能ギャップを明らかにした。評価された 12 のモデルの中で、最高報告 Pass@1 スコアはわずか 55.10% であった。

このギャップは、以下の 4 つの主要な課題に起因している：

1. 長文脈の複雑性：プロンプトには、プログラミングモデル、例、およびターゲットコードを含む約 26K トークンが含まれている。
2. 意味的ギャップ：このタスクは、命令型 C カーネルコードを宣言型 Z3 Python 仕様に翻訳することを要求し、根本的に異なるプログラミングパラダイムを伴う。
3. 交差する関心：C コードは、事前条件（エラーチェック）と事後条件（状態変更）の論理をしばしば混在させるが、形式仕様では厳密に分離されなければならない。
4. ドメイン固有の知識：カーネル API には、一般的な LLM のトレーニングでカバーされていない専門的なパターン（ページテーブルエントリ数式、参照カウントのセマンティクス、TLB フッシュ操作など）が含まれている。

手法：BODHI

著者は、標準的なファウショットプロンプトに構造化されたC-to-Python 変換ガイドを付加するドメイン知識プロンプティング手法であるBODHIを提案する。中間推論ステップの生成に焦点を当てる標準的なチェーン・オブ・ソート（CoT）または構造化チェーン・オブ・ソート（SCoT）とは異なり、BODHI は構造化された参照資料を入力コンテキストに注入する。

プロンプト構造

BODHI プロンプトは、OSV-Bench ベースラインの 4 つのコンポーネントを維持する：

1. システムプロンプト（指示）。
2. プログラミングモデル（クラス、定数、関数の定義）。
3. 5 つのファウショット例（C 実装から Z3 仕様へのペア）。
4. ターゲットタスク（機能説明と C コード）。

BODHI は第 5 のコンポーネントを追加する。これは、ファウショット例とターゲットタスクの間に挿入される 519 行の変換ガイドである。この配置は、トランスフォーマーの注意機構における「最近性効果」を活用し、ドメイン固有のパターンが生成中に最もアクセスしやすくなるようにする。

変換ガイドの設計

このガイドは、中級モデル（Claude Haiku 4.5）の失敗の反復分析から導き出された15 のカテゴリに整理されている。これは、事前条件の抽出と事後条件の生成を区別する関心の分離の原則に従う。カテゴリは 3 つのティアにグループ化される：

• ティア 1（構文）：仕様テンプレート、事前条件の翻訳（C のエラーチェックの否定）、事後条件パターン、マップフィールド構文（読み取り () と書き込み [] の区別）、演算子規則、および定数の接頭辞をカバーする。
• ティア 2（ドメインセマンティクス）：ページテーブルエントリ（PTE）数式（x86 と IOMMU の区別）、シャドウメタデータ、参照カウント、TLB フッシュ操作、状態ポインタ名、およびフィールド名のマッピングをカバーする。
• ティア 3（完全性）：C ヘルパー関数の展開、利用可能なヘルパーインベントリ、および複雑な IPC 状態機械パターンに対処する。

重要なのは、このガイドがタスク固有の解決策や完全なコードではなく、一般的な翻訳規則と図示的なパターンを含む「ドメインの教科書」として機能することである。

主な貢献

1. ドメイン固有の変換ガイド：検証済みの真の仕様から導き出された C-to-Python/Z3 変換パターンを網羅する、構造化された 15 カテゴリのガイド。
2. 包括的な評価：Anthropic、Mistral、Amazon、DeepSeek、Meta、Alibaba の 6 つのベンダーから 9 つのモデルを対象としたテスト。密、エキスパート混合、推論アーキテクチャを網羅。
3. エラー分析：BODHI が構文エラーと意味エラーの両方を削減することを示す詳細な分解。特に、指示追従能力を持つが特定のドメイン知識を欠く中級モデルに最も大きな影響を与えた。
4. 新しい最先端：OSV-Bench で Pass@1 **96.73%**を達成し、以前の最高値 55.10% を大幅に上回った。

結果

• 性能向上：BODHI はテストされたすべてのモデルの Pass@1 スコアを向上させ、Qwen3 で**+11.0%、Devstral 2 で+31.8%**の向上幅を示した。
• 最高性能：Claude Opus 4.6 + BODHIの構成は**96.73%**を達成し、245 タスクのうちわずか 8 タスクで失敗した。
• エラー削減：
  • 構文エラー：BODHI は、特にタイプ/ソートの不一致や API の誤用（マップ書き込みに対して括弧を使用するなど）の構文エラーを大幅に削減した。Devstral 2 の場合、構文エラーは 31.0% から 8.2% に低下した。
  • 意味エラー：このガイドは、ドメインパターンエラー（誤った PTE 数式など）と翻訳論理エラーを効果的に解決した。Claude Opus 4.6 の場合、ベースラインの失敗はほぼ一貫してドメインパターンエラーであったが、BODHI はこれを 2.4% に削減した。
• モデル非依存性：改善は多様なアーキテクチャとベンダー間で一貫しており、この手法が特定のモデルファミリーのトレーニングデータに依存していないことを示唆している。
• 中級モデルの最適化：最大の相対的向上は、ガイドを利用するのに十分な指示追従能力を持つが、最上位モデルのような内在的なドメイン知識を欠く中級モデル（Devstral 2、Claude Haiku 4.5 など）で観察された。

意義と主張

本論文は、ドメイン知識の注入が、一般的なコード生成と形式仕様合成の間のギャップを効果的に埋めるモデル非依存の手法であると主張している。著者らは、OS カーネル検証のボトルネックは LLM の推論能力（o1 や DeepSeek-R1 などの推論最適化モデルが標準的な指示追従モデルを上回らなかったため）ではなく、特定の翻訳知識の欠如にあると論じている。

ドメイン知識をファウショット例のみに依存するのではなく、参照ガイドとして構造化することで、BODHI は LLM がページテーブル数式や参照カウントなどの複雑なカーネルセマンティクスを正しく処理できるようにする。この研究は、人間のエキスパートがドメインガイドを構築し、LLM がそれを大規模に適用してほぼ完璧な仕様合成を達成するという、生産的な分業が存在することを示している。著者らは、このアプローチがガイド構築のコストとモデルの出力形式への準拠能力によって制限されることに注意を促しているが、モデルの再トレーニングなしに形式検証を改善する再現可能な道筋を提供している。