NESA: 関係型ニューロ記号静的プログラム分析の技術的サマリー

本論文は、NESA (Relational Neuro-Symbolic Static Program Analysis) と呼ばれる新しい静的プログラム分析手法を提案しています。これは、大規模言語モデル（LLM）の能力と記号的（シンボリック）な解析を組み合わせる「ニューロ記号アプローチ」を採用し、従来の静的解析が抱える「コンパイル依存」と「カスタマイズの難易度」という 2 つの課題を解決すると同時に、LLM 固有の「幻覚（ハルシネーション）」を軽減することを目的としています。

以下に、問題定義、手法、主要な貢献、評価結果、および意義について詳細にまとめます。

---

1. 背景と問題定義

従来の静的プログラム解析は、コード最適化、バグ検出、デバッグに不可欠ですが、実社会での普及には以下の 2 つの大きな障壁が存在します。

1. コンパイルへの依存: 主要な解析ツール（FlowDroid, Infer など）は、ソースコードから中間表現（IR）を生成するコンパイルプロセスに依存しています。これにより、開発中の不完全なコードや、複雑なビルドシステムを持つプロジェクトでの解析が困難になります。
2. カスタマイズの難易さ: 特定の要件に合わせた解析を行うためには、IR やコンパイラ内部の深い知識が必要であり、開発者が容易にツールをカスタマイズできません。既存のクエリ言語（CodeQL など）でも学習コストが高く、専門知識が求められます。

一方、LLM はコンパイルなしでコードの意味を理解できる可能性がありますが、ハルシネーション（誤った情報の生成） が頻発し、静的解析のような高精度が求められるタスクでは誤検知や見落としの原因となります。

2. 提案手法：NESA

NESA は、LLM の意味理解能力と、パーサに基づく決定論的な構文解析を組み合わせる関係型ニューロ記号アプローチです。

2.1 分析ポリシー言語（Analysis Policy Language）

ユーザーは、Datalog の制限された形式を用いて「分析ポリシー」を定義します。これにより、複雑な解析タスクをより単純な部分問題に分解します。

• 記号関係（Symbolic Relations）: AST（抽象構文木）やパーサから決定論的に導出される構文情報（例：変数名、行番号、制御フロー順序、関数引数など）。これらはハルシネーションを発生させません。
• ニューラル関係（Neural Relations）: LLM のプロンプトによって導出される意味情報（例：データ依存関係、汚染伝播、ゼロ値の伝播など）。
• 拡張関係（Intensional Relations）: 上記の関係から導出される最終的な解析結果（例：スライス対象の行、バグの存在）。

ユーザーは、自然言語での定義と数例のコード例（Few-shot examples）を「ニューラル関係仕様」として提供することで、LLM に特定の意味属性を抽出させることができます。

2.2 評価プロセスとハルシネーション軽減戦略

NESA は、ワークリストアルゴリズムに基づき分析ポリシーを評価しますが、LLM のハルシネーションとコストを抑制するために 2 つの重要な戦略を採用しています。

1. 遅延プロンプティング（Lazy Prompting）:

   • 規則の評価において、ニューラル関係を填充する前に、まず記号関係や拡張関係のタプルを決定します。
   • これにより、LLM に提示する問題の範囲（バウンドド項）を狭め、特定の値の組み合わせのみを問うように制限します。これにより、LLM が生成するタスクの複雑さが下がり、ハルシネーションが大幅に減少します。
   • 例：すべてのデータ依存関係を列挙するのではなく、「特定の式 $e_2$ に対して、$e_1$ が依存しているか？」という狭義の問いに限定します。

2. 増分プロンプティング（Incremental Prompting）:

   • 固定点計算の反復処理において、同じタプルに対して LLM を繰り返し呼び出すことを防ぎます。
   • すでに生成済みのタプルを記憶し、新しいタプルのみを LLM に要求することで、トークンコストと時間を削減します。

3. 主要な貢献

1. コンパイル不要かつカスタマイズ可能な分析フレームワークの提案:

   • 中間表現（IR）の生成を必要とせず、自然言語と少量の例示に基づいてユーザーが分析ポリシーを定義できます。
   • Datalog 風のルールと LLM の組み合わせにより、構文解析と意味解析を体系的に統合しました。

2. ハルシネーション軽減のための評価戦略:

   • 「遅延プロンプティング」と「増分プロンプティング」を導入し、LLM の誤りを最小化するとともに、計算コストを最適化しました。

3. 広範な実験による性能検証:

   • プログラムスライシング、6 種類のバグ検出（XSS, DBZ, NPD など）、および実世界の Android マルウェア（TaintBench）や大規模プロジェクト（h3, dynamips）での評価を行いました。

4. 評価結果

4.1 精度と再現率（Benchmark）

• プログラムスライシング: 精度 91.50%、再現率 84.61%（F1 スコア 0.88）。既存の学習ベースのスライサー（NS-Slicer）や、LLM を直接使うベースライン（GPT-3.5/4 など）を凌駕しました。
• バグ検出（Juliet Test Suite）:
  • XSS 検出：精度 98.95%、再現率 94.00%。
  • APT（絶対パス移動）：精度 94.74%、再現率 90.00%。
  • DBZ（ゼロ除算）：精度 54.62%、再現率 71.00%（パス条件の判定が難しいため精度は低下しますが、既存の LLM 単体アプローチよりはるかに優れています）。
  • UOWH（ソルトなしワンウェイハッシュ）：精度・再現率ともに 100%。
• 比較: 既存の産業用ツールや、LLM を直接プロンプトするベースラインと比較して、F1 スコアやコスト効率（バグ 1 件あたりのコスト）で優位性を示しました。

4.2 実世界での適用

• TaintBench（Android マルウェア）: 70 件の汚染脆弱性のうち 55 件を検出（精度 66.27%、再現率 78.57%）。産業用ツールより F1 スコアで 0.20 上回りました。
• 大規模プロジェクト（h3, dynamips）: 13 件の実在するメモリリークバグを発見し、すべて開発者によって修正されました。一方、純粋な LLM ベースのアプローチ（Cursor + Claude 3.7）はこのタスクで真のバグを検出できませんでした。

4.3 効率性

• 1 つの解析タスクあたりの平均コストは数セント程度で、実行時間は数秒から数十秒です。
• 増分プロンプティングにより、不要なプロンプト回数を最大 82% 削減しました。

5. 意義と結論

NESA は、LLM の柔軟な意味理解能力と、記号的手法の正確性・決定論的性質を融合させることで、静的解析の新たなパラダイムを示しました。

• 実用性の向上: コンパイル環境に依存せず、開発中のコードや複雑なビルドシステムに対しても適用可能です。
• カスタマイズの民主化: 専門的なコンパイラ知識がなくても、自然言語と例示を通じて分析ルールを定義でき、開発者が自社の要件に合わせてツールを容易にカスタマイズできます。
• 信頼性の確保: ハルシネーションを構造的に抑制する設計により、LLM を静的解析に実用的に適用できる可能性を証明しました。

将来的には、LLM のファインチューニングや、より小さなタスク特化モデルの導入、文脈依存解析への拡張などが検討課題として挙げられています。NESA は、LLM と静的解析の融合において、実用的で高精度な分析ツールの開発に向けた重要な一歩となります。