技術的概要：LLM ベースのプログラム分析におけるエージェント的解釈

1. 問題定義

大規模言語モデル（LLM）は、ソースコードを超えた情報（ドキュメント、セキュリティ勧告、バージョン固有のメタデータ、非公式の API 契約など）にアクセスすることで、プログラム分析において独自の能力を発揮します。しかし、「ワンショット」方式による全体プログラム分析に LLM を依存させることは、本質的に以下の 3 つの主要な理由により脆いものです：

1. 文脈感受性：実証的研究によれば、モデルの性能は文脈の長さやタスクの複雑さが増すにつれて低下し、結果はプロンプト内の情報の順序に大きく依存します。重要な証拠（例：特定のセキュリティ勧告）が提供されても、それが確実に活用されるとは限りません。
2. 永続的状態の欠如：単一の LLM 応答には、どの特定の主張が支持されたか、反証されたか、あるいは未解決のまま残されたかを追跡する永続的状態が存在しません。これにより、自己矛盾する推論や、自身の結論を支持できない推論を処理することが困難になります。
3. 依存構造の欠如：単一のショットによる回答にはフィードバックのメカニズムが存在しません。後の発見により、以前の質問のスコープが不適切であったり、上流コンポーネントが異なる仮説下で再検討を必要としたりする場合、非構造化された回答はこのような反復的な洗練を促進できません。

したがって、特にソースコードや形式的仕様には関連事実が完全に含まれていない証拠依存型のプログラム分析において、アドホックな LLM プロンプトと完全に指定された静的分析の間のギャップを埋めるフレームワークが必要です。

2. 手法：エージェント的解釈

本論文は、LLM 駆動の推論に格子ベースの静的分析の規律を適用するエージェント的解釈（Agentic Interpretation）というフレームワークを提案します。この手法は、高レベルの分析目標をプログラムポイントやコンポーネント境界にアンカーされた局所的な主張に分解し、有限高さの格子とワークリストアルゴリズムを通じてその進化を管理します。

2.1 中核コンポーネント

• 評価グラフ（$G^*$）：プログラムから導出されたグラフ（$G_{prog}$）を拡張したもので、以下を含みます：
  • 補助ノード：単一のプログラムポイントにマッピングされない、コンポーネント間相互作用や目標を表すノード。
  • 文脈エッジ：ノード $n$ における主張が評価される際、先行ノードからの現在の評価状態と証拠を受け取ることを保証する、前方フローのエッジ。
  • フィードバックエッジ：下流の評価が変更された際に上流ノードの再評価をトリガーする、後方フローのエッジ（例：否定された構成主張が、不透明なコンポーネントにおけるターゲット検索をトリガーする）。
• 評価ドメイン（格子）：主張の証拠状態を要約する有限高さの結合半格子（$A$）。
  • 論文では、AGraded格子を例示しています：$\{ \perp, w, s \} \times \{ \perp, w, s \}$。ここで、最初の座標は支持証拠を、2 番目の座標は反証証拠を表します。値は欠如（$\perp$）から弱（$w$）、強（$s$）の範囲をとります。
  • この格子は、具体的なプログラム状態に関する抽象ドメインではなく、証拠状態に関する認識論的（epistemic）ドメインです。主張が支持または反証されたかどうか、およびその証拠の強さを記録します。
• ワークリストハネス：分析状態を管理する制御ループ。
  • 文脈化：ノード $n$ に対して、ハネスはソースコード、高レベルの目標、先行ノードの現在の評価を用いてプロンプト文脈（$\Gamma_n$）を構築します。
  • ノード変換器：LLM エージェントは 2 つの操作を実行します：
    1. 評価：既存の主張を文脈に対して評価し、更新された評価と証拠記録を返します。
    2. 生成：文脈に基づいて、新しい関連主張を提案します。
  • 伝播：新しい評価と古い評価の結合が格子順序において厳密な増加をもたらす場合、そのノードの拡張された後続ノードは再評価のためにキューに追加されます。

2.2 分析プロセス

このプロセスは、不透明なサードパーティコンポーネント（JSON パーサーと署名検証器）を持つプログラムのセキュリティレビューを通じて説明されます。

1. 初期化：ワークリストには、すべてのプログラムノードと補助ノードがシードされます。
2. 反復的洗練：
   • フェーズ I：コンポーネントの初期独立評価（例：パーサーと検証器のドキュメントレビュー）。
   • フェーズ II：証拠の構成。フレームワークはコンポーネント間主張（例：「コンポーネントは共同して安全性を確保しているか？」）を評価します。もし構成主張が弱く反証された場合、フィードバックエッジが上流コンポーネントの再調査をトリガーします。
   • フェーズ III：フィードバック駆動型の洗練。否定された構成からの文脈（例：「プロセッサは検証を行わない」）は、LLM に広範なレビューではなく、特定の脆弱性（例：プロトタイプ汚染）のためのターゲット型検索を実行するよう導きます。
   • フェーズ IV：安定化。強化された上流証拠が前方に伝播し、グローバル目標の強い反証につながります。評価においてこれ以上の厳密な増加が発生しなくなった時点でワークリストは空になります。

3. 主要な貢献

本論文は、以下の 3 つの主要な貢献を行います：

1. フレームワークの提案：エージェント的解釈を、証拠依存型のプログラム分析のための構造化されたアプローチとして導入し、LLM が必要だが直接プロンプトでは不十分である適切な問題領域を特定します。
2. 形式的モデル：評価グラフ、評価ドメイン、ノード変換器、ワークリストアルゴリズムを定義し、中核モデルを形式化します。
3. 設計空間の特性化：設計空間を探求します。
   • 評価格子：粗い格子（例：存在/非存在）と微細な格子（例：強さ、信頼性の根拠）の間のトレードオフについて議論します。証拠の強さと信頼性の根拠（例：「モデルのみ」対「確認済み」）を個別に追跡するAStratifiedというドメインを導入します。
   • 主張管理：主張の正規化、粒度、スコープに対処します。
   • クエリ設計：評価クエリ（支持/反証）と生成クエリ（新しい主張の提案）を区別します。
   • 終了性：非決定性の LLM 応答が存在する場合でも、更新が結合（join）を通じて単調であれば、有限高さの格子と有界な主張生成に対してアルゴリズムが終了することを証明します。

4. 結果と限界

• 結果：本論文は、不透明なコンポーネントを持つハンドラのセキュリティレビューという実例を提供し、フレームワークが目標を分解し、フィードバックループを活用して検索を洗練し、最終評価に安定する様子を実証しています。また、複数のソースからの弱い証拠を組み合わせることで強い反証を導き出し、グローバルなセキュリティ目標が侵害されていることをフレームワークが検出できる様子を示しています。
• 限界：
  • 本論文は進行中の作業を記述しています。実用的な実装や実験的評価は含まれていません。
  • このフレームワークは終了性と有界性を保証しますが、従来の意味での健全性（soundness）は保証しません（つまり、LLM の結論が正しいことを証明するものではありません）。LLM の証拠的役割を明示的かつ監査可能にします。
  • このフレームワークは、証拠を常に誤って判断するエージェントを修正することはできません。そのような誤りを可視化するだけです。
  • 終了性の証明は、主張が取り消されることはなく、評価が結合を通じてのみ増加するという仮定に依存しています。信念の修正（評価の低下）のメカニズムは、有界な置換またはエポカルな再計算を必要とする将来の作業として議論されています。

5. 意義

この研究の意義は、プログラム分析における LLM ベースの推論に構造的規律をもたらそうとする点にあります。「生成と検証」パラダイム（LLM の出力に対する形式的検証器を必要とする）や「ヒューリスティック・オラクル」パラダイム（LLM が健全性に影響を与えない）から離れ、エージェント的解釈は中間地帯をターゲットとします。

これは、以下の証拠依存型分析において重要です：

• 関連事実が形式化できない場合（例：非公式の API 契約、セキュリティ勧告）。
• 完全な検証器が存在しない場合。
• 分析が多様な非コードソースからの情報を統合する必要がある場合。

このフレームワークは、LLM をブラックボックスの生成器から、より大きな分析システムの有界かつ監査可能なコンポーネントへと変換します。これにより、分析が制御された原理的な方法で進行し、関心の分離が可能になります。LLM は証拠を提供し、格子ベースのハネスは分析が有界かつ追跡可能であることを保証します。このアプローチは、プログラム分析におけるエージェントシステムのための形式的基盤を持つ技術の設計に関する将来の議論を鼓舞することを目指しています。