Learning Lookahead Lemmas for Neural Network Verification

技術要約：ニューラルネットワーク検証のためのルックアヘッド・レマ（Lookahead Lemmas）の学習

問題提起
最先端のニューラルネットワーク検証器は、非線形活性化関数（具体的にはReLU）を再帰的に分割して部分問題を分析する、分岐限定法（branch-and-bound; BaB）の手順に依存しています。近年の進展により、分岐ヒューリスティックや、実行不可能な部分問題から導出されるブール・カット（boolean cuts）は改善されてきましたが、これらのアプローチは主に「反応的（reactive）」なものです。これらは、探索がすでに情報を取得するために支払ったコストを利用しています。現代のSATソルバが、情報の積極的な導出のために定期的に探索を一時停止する「インプロセッシング（inprocessing）」を利用しているのに対し、ニューラルネットワーク検証には、これに相当するメカニズムが欠けています。本論文は、BaB解決ループへの積極的な情報導出の統合という課題に取り組んでいます。

手法
著者らは、ルックアヘッド（lookahead）手順の変種によって駆動されるインプロセッシング・フレームワークを導入しています。ルックアヘッドを単に次の分岐変数を選択するためだけに使用するのではなく、このフレームワークでは、不安定なReLUのフェーズ（活性または非活性）に関する新しい論理レマ（lemma）を導出するために使用します。

本手法の核となるのは、以下の3つのコンポーネントです。

1. 含意グラフ（Implication Graph）の構築:
   フレームワークは、ノードが不安定なReLUのフェーズ固定（活性の場合は $r_i$、非活性の場合は $\neg r_i$）を表す有向含意グラフ $G = (V, E)$ を構築します。

   • ルックアヘッド・プローブ（Lookahead Probe）: 各不安定なReLUに対して、それを活性フェーズまたは非活性フェーズに固定した場合のシミュレーションを行います。制限された予算内での境界伝搬（Marabouの場合はDeepPoly、または$\alpha$-$\beta$-CROWNの場合は単一の$\alpha$-CROWNパス）を実行します。
   • レマの導出（Lemma Derivation）: フェーズの固定が実行不可能性（infeasibility）を招く場合、その補集合が**ユニット・レマ（unit lemma）**として記録されます。フェーズの固定が別の不安定なReLUを特定のフェーズに強制する場合、バイナリ含意（$r_i \to r_j$）が記録されます。
   • ハル境界（Hull Bounds）: 手順はまた、両方のフェーズ・シミュレーションから導出された境界のハル（hull）を取ることで、よりタイトな境界を計算します。

2. SAT閉包による探索空間の枝刈り:
   含意グラフは命題論理式 $\Sigma$ として扱われます。任意のBaBノードにおいて、ソルバは $\Sigma \cup R$ の充足可能性をチェックします。ここで $R$ は現在の探索パスに沿ってコミットされたフェーズ固定を表します。この結合が充足不能（unsatisfiable）である場合、さらなる境界伝搬や分割を行うことなく、その部分問題は即座に枝刈りされます。

3. 動的更新とカットの生存確認（Cut Vivification）:

   • 再プロービング（Reprobing）: 探索が進み、より多くのReLUが固定されるにつれて、探索空間は狭まります。フレームワークは、新しい分岐決定が強制されなくなり、確立されたフェーズの集合が増加した特定のインターバルにおいて、制限されたクエリに対してルックアヘッド手順を再実行する再プロービングをトリガーします。これにより、ルートでは証明できなかった新しい事実を用いて含意グラフが更新されます。
   • カットの生存確認（Cut Vivification）: 部分問題がUNSATと判定されたとき、標準的な検証器はブール・カット（例：BICCOSまたはPICID）をマイニングします。フレームワークは、含意を追跡することで、含意グラフを用いてこれらのカットを**生存確認（vivify）**します。これは、含意グラフの閉包に対してカットが充足不能である場合、カットから冗長なフェーズ固定を特定して削除するプロセスです。これにより、カットをその本質的な実行不能コアへと短縮します。このように短縮されたカットは、その後、含意グラフとともにグローバルな問題へと追加され、将来の枝刈りを強化します。

主な貢献

• インプロセッシング・フレームワーク: 本論文は、ニューラルネットワーク検証における初の完全なインプロセッシング・フレームワークを提案し、反応的な情報の利用から積極的な導出へと転換を図っています。
• ルックアヘッド由来のレマ: ルックアヘッド手順を、単なる分岐ヒューリスティックとしてではなく、ReLUのフェーズ関係の動的な含意グラフを生成するために適応させています。
• 既存の検証器との統合: このフレームワークは、2つの異なる最先端の検証器、Marabou（SMTベース、CPU）および $\alpha$-$\beta$-CROWN（境界伝搬ベース、GPU）において実装されています。
• カットの強化: 含意グラフを使用してブール・カットを生存確認し、それらを本質的な実行不能コアへと効果的に短縮するメカニズムを導入しています。

実験結果
フレームワークは、標準的なベンチマーク（MarabouについてはACASXu、MNIST、SafeNLP；$\alpha$-$\beta$-CROWNについてはCIFARおよびTinyImageNet）で評価されました。

• 性能向上: フレームワークは両方の検証器の性能を向上させました。具体的には、ベースラインの検証器と比較して、最大で34%多いインスタンスをUNSATとして証明しました。
• 効率性: ルックアヘッド・プロービングおよび再プロービングのオーバーヘッドは最小限でした。例えば、SafeNLPでは、プロービングは実時間の0.1%未満を占めていました。ピーク時でも19.2%であったMNISTにおいても、解決されたUNSATインスタンスの純増分（35個の追加インスタンス）がそのコストを上回りました。
• 堅牢性: このアプローチは、すべてのテストされたベンチマークにおいて、タイムアウトの回数と平均探索状態を減少させました。

意義と主張
本論文は、SATソルバにおけるインプロセッシングに類似した積極的な情報導出メカニズムを導入することにより、ニューラルネットワーク検証における重要なギャップを埋めることを主張しています。著者らは、新しい情報の導出を、分岐ヒューリスティックの副産物としてではなく、解決手順の不可欠な一部として扱うことを強調しています。

結果は、ルックアヘッドを活用して含意グラフを構築することが、探索空間をより効果的に枝刈りし、ブール・カットを強化できることを示しています。著者らは、現在の実装はバイナリ含意とユニット・レマに焦点を当てているものの、将来的には伝搬に冗長な節の導出や、線形制約へのリフティングを探索できる可能性があると述べています。また、グラフをクエリ間で持ち越すことが漸進的な検証（incremental verification）を向上させる可能性があることも示唆していますが、これは今後の研究課題として残されています。