技術要約：DNNのグローバルな堅牢性を検証するための微分ゾトープ（Differential Zonotopes）

1. 問題提起

深層ニューラルネットワーク（DNN）は、輸送やヘルスケアなどのセキュリティに極めて重要な領域でますます導入されており、そこでは入力の摂動に対する堅牢性が不可欠である。局所的な堅牢性（特定の入力の周囲の小さな摂動に対して予測が変化しないことを保証すること）は十分に研究されている安全特性であるが、グローバルな堅牢性はより厳格な要件である。グローバルな堅牢性は、ある一定の距離内にあるすべての入力ペアに対して、モデルの予測が一貫していることを要求する。

形式的に、グローバルな堅福性は、単一の実行トレースではなく、2つの普遍的に量子化された実行トレース間の関係を検証する必要があるため、**2-安全性（2-safety property）**である。この複雑さにより、グローバルな検証は局所的な検証よりも大幅に困難になっている。信頼度に基づくグローバルな堅牢性（決定境界を避けるために高信頼度の予測に保証を限定するもの）に関する既存の手法は、専用の充足可能性ソルバに依存しているが、スケーラビリティに課題があり、現在は数十個のニューロンを持つネットワークに限定されている。

2. 手法

本論文は、効率的にグローバルな堅牢性を検証するために、**微分ハロー・ゾトープ（differential halo zonotopes）**に基づいた新しい静的解析フレームワークを提案する。

2.1 微分ハロー・ゾトープ

核心となる技術的革新は、**ゾトープ（zonotope）**抽象ドメインの拡張である。標準的なゾトープは、中心と生成行列を用いて点の集合を表現する。グローバルな堅ろう性を検証するためには、著者らは異なる入力を持つ同一のDNNの2つの実行を同時に追跡しなければならない。

• 課題: 微分ゾトープ（以前は入力が同一であるDNNの等価性検証に使用されていたもの）のナイーブな適応は、グローバルな堅牢性の検証には失敗する。入力を同一として初期化するか、完全に独立した生成子を使用すると、不健全（unsound）になるか、過剰な近似（精度の喪失）を招く。
• 解決策: 著者らは、**微分ハロー・アフィン形式（differential halo affine forms）**を導入する。このエンコーディングは、摂動の境界 $\epsilon$ を2つの生成子に分配する：
  1. 相関を維持するために2つの実行間で共有されるプライマリ生成子（primary generator）。
  2. 摂動をモデル化するために各実行に対して独立したセカンダリ生成子（secondary generators）。
• メカニズム: この「ハロー（後光）」構造により、システムは2つの入力 $x$ と $y$ がバウンディングボックス $[l, u]$ 内にあり、かつ $|x - y| \le \epsilon$ を満たすという条件を、健全かつ精密にエンコードできる。微分ゾトープ $\mathcal{Z}_\Delta$ は、逐次的に2つの実行間の差を追跡し、個々のゾトープを減算するよりもタイトな発散の境界を得る。

2.2 対称的な信頼度に基づくグローバルな堅牢性

本論文は、既存の信頼度に基づくグローバルな堅牢性の定義（非対称なバリアント）における限界を指摘している。非対称な定義では、入力 $x$ の信頼度が高ければ、たとえ $y$ の信頼度が低くても、異なるクラス $y$ へと変化してはならないと要求する。著者らは、低信頼度の異なる予測（例：手動レビューをトリガーするようなケース）への変化は実用上許容可能であるため、この定義は過度に制限的であると主張している。

彼らは、対称的なバリアントを提案する：

• 定義: 距離 $\epsilon$ 以内にある任意の2つの入力 $x, y$ について、両方が閾値 $\tau$ を超える信頼度で分類されている場合、それらは同じクラスに属さなければならない。
• 利点: この緩和により、より広範なクラスのネットワークを「堅牢」として受け入れることが可能になるが、低信頼度の出力がフォールバックメカニズムによって処理される安全性の高いアプリケーションにおいても、意味のある性質を維持できる。

2.3 検証アルゴリズム

検証プロセス（ツール TwoSafe に実装）は以下のステップに従う：

1. 初期化: 入力空間と摂動制約を表す微分ハロー・ゾトープを構築する。
2. 伝播: ゾトープをDNNの層へと伝播させる。ReLU活性化関数については、非線形性を過剰近似するために新しい生成子を導入し、微分構造を維持する。
3. 特性チェック: 出力において、両方が信頼度閾値 $\tau$ を満たしながらもクラスが異なるような出力ペアが存在するかどうかを確認するために、線形計画法（LP）問題を定式化する。
4. 洗練: チェックが（過剰近似により）決定不能な場合、アルゴリズムは**生成子分割（generator splitting）**を実行する。標準的な入力分割とは異なり、これは摂動空間の被覆を失うことなく、微分ハロー・ゾトープの生成子を分割して近似を洗練させる。

3. 主な貢献

1. 微分ハロー・ゾトープ: 2つの摂動された入力を密に連携させて共同で伝播させ、その発散をタイトに境界付ける、ゾトープを拡張した新しい抽象ドメイン。これにより、個別の解析よりも高精度にグローバルな2-安全性プロパティを検証できる。
2. 対称的な信頼度に基づくグローバルな堅牢性: 高信頼度の予測間でのみ一貫性を要求する、グローバルな堅牢性の新しい定義。この定義は非対称なバリアントよりも厳密に制約が緩く、提案されたフレームワーク内での効率的な検証を可能にする。
3. 健全性の証明: 微分ゾトープに基づく静的解析の健全性の形式的証明であり、主要な結果はIsabelleで形式化されている。
4. TwoSafeツールと評価: アプローチを新しいツール TwoSafe に実装。これは、精度とスケーラビリティの両面において、最先端の基準（CGRベースライン）を大幅に上回る性能を示す。

4. 実験結果

著者らは、Law（小規模）、LHC（粒子分類）、ACAS Xu（衝突回避）、HAR（人間活動認識）の4つのベンチマークを用いてTwoSafeを評価した。

• スケーラビリティ: TwoSafeは、最大 500個のReLUニューロン および 561個の入力次元（HARベンチマーク）を持つネットワークにおいて、グローバルな堅牢性の検証に成功した。対照的に、ベースライン（CGR）はこれらの大規模なネットワークでタイムアウトするか、メモリを使い果たした。
• 精度: ベースラインは、特に多くの出力クラスを持つネットワークにおいて、粗いソフトマックス近似により、頻繁に**偽の反例（spurious counterexamples）**を報告した。TwoSafeはこれらの偽陽性を回避した。
• パフォーマンス: TwoSafeは大幅な高速化を示した。例えば、LHCベンチマークでは、ベースラインが2時間経過してもタイムアウトした場面において、TwoSafeは3秒未満で堅牢性を検証した。
• 対称 vs 非対称: 対称的な特性により、非対称な特性が決定不能であったり失敗したりするパラメータ領域においても、検証が可能となった。例えば、$\epsilon=0.01$ の場合のHARベンチマークにおいて、対称的な特性は検証可能であったが、非対称なバリアントはタイムアウトした。

5. 重要性と主張

本論文は、堅牢性の保証の強さと、検証ツールのスケーラビリティとの間に存在する固有の緊張関係を解消することを主張している。ローカルからグローバルな堅牢性検証へと移行し、微分ハロー・ゾトープを利用することで、従来よりもはるかに広く深いネットワークの検証が可能であることを示している。

対称的な信頼度に基づくグローバルな堅牢性の導入は、実用的な進歩として提示されている。これは、低信頼度の予測が現実世界のシステムにおいて異なる形で扱われることを認めることで、より広範なクラスのネットワークに適用可能な「意味のある堅牢性の概念」を提供するものである。本研究は、微分的な検証が2-安全性プロパティに適応された場合、従来の手法が扱ってきたものよりも1桁大きいネットワークまでスケールできることを確立しており、グローバルな堅牢性の認証を実世界のデプロイされたモデルに対して実現可能にしている。