論文「Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code」の技術的サマリー

本論文は、大規模言語モデル（LLM）を「ゴーストコード（Ghost Code）」の生成に利用することで、従来の記号実行（Symbolic Execution）の限界を克服するハイブリッドフレームワーク**「Gordian」**を提案するものです。SMT ソルバの苦手とする複雑な数値計算や動的メモリ構造を、LLM の推論能力とソルバの厳密な制約解決能力を組み合わせることで効率的に処理します。

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

---

1. 問題定義：記号実行のボトルネック

記号実行は、抽象的な入力を用いてプログラムの動作を論理制約に変換し、SMT ソルバを用いて解析する強力な技術ですが、以下の根本的な限界に直面しています。

1. ソルバ敵対的なコード断片: 非線形算術、三角関数、浮動小数点演算など、SMT ソルバが解くのが困難（または不可能）な制約を生成するコード。
2. 複雑な数値推論: 深い実行パスにおいて、多数の関数をまたぐ一貫した入力選択が必要な場合、LLM 単体では長距離の依存関係を維持できず、SMT ソルバ単体では制約が解けない。
3. 無限のヒープ構造: ポインタや動的データ構造（リスト、木構造など）を扱う際、ヒープの構成（エイリアシング関係や形状）の組み合わせが爆発し、経路探索が不可能になる。

近年、LLM をソルバの代替として用いる試み（ConcoLLMic など）がありますが、これらは深い実行パスにおけるグローバルな一貫性を維持できず、実世界の複雑なコードベースでは十分なカバレッジを達成できていません。

2. 提案手法：Gordian

Gordian は、LLM を記号実行の「代替」ではなく、「補助」として位置づけ、SMT ソルバの能力を補完する軽量なゴーストコードを生成・注入するハイブリッドアプローチを採用しています。

2.1 核心的なアイデア

LLM にプログラム解析を依頼し、ソルバが苦手とするコード断片に対して、以下の 3 種類のゴーストコードを生成させます。これらは実行時の機能には影響を与えず、ソルバの推論を支援するためにのみ挿入されます。

1. コードの逆転（Inversion）:

   • 目的: 非線形演算や三角関数など、直接の逆関数が存在しない複雑なコード断片を逆方向に実行可能にする。
   • 手法: LLM に逆関数（または数値探索アルゴリズム、例：黄金分割探索）を生成させ、制約を「後方（Suffix）」から「前方（Prefix）」へ伝播させる。
   • アルゴリズム: 双方向制約伝播（Bidirectional Constraint Propagation）。SMT ソルバで後方の制約を満たす値を求め、逆関数で入力値を推定し、前方の制約と整合性を取るよう最適化を繰り返します。

2. ソルバ親和的な代理モデル（Surrogate Modeling）:

   • 目的: 複雑な挙動（外部ライブラリ呼び出し、暗号処理など）を、ソルバが扱いやすい論理（線形算術やビットベクトルなど）に近似する。
   • 手法: LLM に元の機能（出力や分岐）を保持しつつ、ソルバが解きやすい簡略化されたコード（スタブ）を生成させ、元のコードを置換します。

3. 意味的ヒープ分割（Semantic Heap Partitioning）:

   • 目的: ポインタ爆発を抑制し、意味的に重要なデータ構造の形状に探索を限定する。
   • 手法: LLM にドメイン固有の知見に基づき、ヒープの「意味的トポロジー（例：リング構造、特定の長さのリストなど）」を定義させる。記号実行時に、これらのトポロジーに基づいてヒープを部分的に具体化し、残りを記号のまま探索します。

2.2 実装とワークフロー

• ベースエンジン: KLEE 記号実行エンジン上で実装。
• プロセス:
  1. LLM が困難なコード断片を特定し、適切なゴーストコードを生成。
  2. 生成されたコードをプログラムに注入（コンパイルし直し）。
  3. 記号実行エンジンが実行し、ソルバと LLM 生成コードの協調によりパスを探索。
  4. 生成された入力値は、元のプログラムで再実行され、正解性（Soundness）が検証される（LLM の幻覚による誤りを防ぐ）。

3. 主要な貢献

1. LLM によるゴーストコード生成の提案: 記号実行を強化する新たなアプローチとして、SMT ソルバを支援するゴーストコードを LLM で自動生成する手法を初めて提案。
2. 3 つの実用的なゴーストコード変種:
   • 双方向制約伝播のための逆転コード。
   • 複雑な挙動をソルバ親和的に近似する代理モデル。
   • 動的データ構造の経路爆発を抑制する意味的ヒープ分割。
3. 包括的な評価: 合成ベンチマーク（LogicBombs）、実用的な数値ライブラリ（FDLibM）、構造化入力プログラム（libexpat, jq, bc）における広範な評価。

4. 評価結果

Gordian は、従来の記号実行（KLEE）および既存の LLM ベース手法（ConcoLLMic, Cottontail）と比較して、大幅な性能向上を示しました。

4.1 カバレッジの向上

• LogicBombs ベンチマーク: 従来の KLEE より平均 52–84% 向上。LLM ベース手法（ConcoLLMic）より 86–419% 向上。
  • 論理爆弾（Logic Bombs）のトリガー率：KLEE (32–39%) → Gordian (最大 94.3%)。
• FDLibM（数値ライブラリ）: 従来の KLEE より平均 22% 向上。ConcoLLMic より平均 183.5% 向上。
  • 浮動小数点の複雑な制約を扱う能力が顕著に向上。
• 構造化入力プログラム: KLEE より最大 108% 向上。Cottontail より平均 86% 向上。
  • 構造化データ（XML, JSON）の解析において、意味的な形状を考慮した探索が有効に機能。

4.2 トークン効率（コスト削減）

LLM の使用量を劇的に削減しました。

• トークン使用量: 既存の LLM ベース手法（ConcoLLMic）と比較して、平均 90–96% 削減（約 25 倍の効率化）。
• 理由: Gordian は LLM を継続的に呼び出すのではなく、困難な箇所でのみ少量のゴーストコードを生成し、残りの探索はソルバに任せるためです。

5. 意義と結論

Gordian は、LLM の「推論・生成能力」と SMT ソルバの「厳密な制約解決能力」を相補的に組み合わせることで、両者の弱点を克服しています。

• 実用性: 実世界の複雑なコード（数値計算、動的メモリ、構造化入力）において、到達困難なパスを効率的に発見可能にしました。
• コスト効率: 大規模な LLM 呼び出しを避け、最小限のトークンで最大の効果を得る設計は、実運用におけるコスト課題を解決します。
• 安全性: 生成された入力値は必ず元のプログラムで検証されるため、LLM の誤り（ハルシネーション）が解析結果の正しさを損なうことはありません。

本論文は、LLM を単なる「ソルバの代わり」ではなく、「ソルバを強化するコンポーネント」として統合する新たなパラダイムを示し、ソフトウェアテストおよび静的解析の分野における重要な進展です。