技術的概要：安全検証のためのニューラルバリア証明の集合ベース訓練

1. 問題定義

連続時間ダイナミカルシステムの安全検証は、自動運転車両、UAV、ロボットマニピュレータなどの安全クリティカルな環境における自律エージェントにとって極めて重要である。あるシステムが安全であるとは、初期集合 $X_I$ から出発する軌跡が、不安全集合 $X_U$ に入ることを意味しない。

既存の検証手法は重大な限界に直面している：

• シミュレーションベース手法は、システム次元に対して指数的な実行時間の増大を招く。
• 到達可能性解析は、指数的な実行時間を回避するために集合ベースの計算を用いるが、計算集約的になり得る。
• バリア証明は、ゼロレベルセットを通じて $X_I$ と $X_U$ を分離するスカラー関数 $B$ を定義することで、安全性の形式的証明を提供する。しかし、ニューラルネットワークベースのバリア証明を合成する最近のアプローチは、反復的な訓練・検証サイクルに依存している。このサイクルでは、ニューラルネットワークが状態空間のサンプル上で訓練された後、外部ソルバ（例：SMT）を用いて形式的に検証される。検証が失敗した場合（反例が見つかった場合）、ネットワークは再訓練される。このプロセスは高コストであり、多くのサイクルを必要とする可能性があり、単一の処理内で有効な証明への収束を保証しない。

2. 手法：集合ベース訓練

著者らは、形式的検証をニューラルネットワークの訓練プロセスに直接統合し、個別の検証ステップの必要性を排除する、新しい集合ベース訓練アプローチを提案する。

中核概念

離散サンプル上で訓練し、後で検証するのではなく、この手法は健全な集合ベース損失関数を用いてニューラルネットワーク $B_\theta$ を訓練する。この損失関数は、個々の点ではなく、状態空間の集合全体（包絡）に対して計算される。損失がゼロに達すると、バリア証明の有効性が構成によって形式的に証明される。

主要な技術的構成要素

A. 健全な集合ベース損失関数
損失関数は、バリア証明に必要な 3 つの性質（定理 1）を符号化する：

1. 性質 P I（不安全状態）： $X_U$ 内のすべての状態は正の値に写像されなければならない。損失 $L_I$ は、$X_U$ の集合ベース像の下限にペナルティを課す。
2. 性質 P II（初期状態）： $X_I$ 内のすべての状態は非正の値に写像されなければならない。損失 $L_{II}$ は、$X_I$ の集合ベース像の上限にペナルティを課す。
3. 性質 P III（ゼロレベルセットのダイナミクス）： リー微分 $L_f B_\theta$ は、ゼロレベルセット $X_Z = \{x \mid B_\theta(x) = 0\}$ 上で負でなければならない。
   • $X_Z$ は未知であり非凸であるため、この手法は再帰的な分枝限定戦略（入力空間を分割し、零点のない領域を破棄する）を用いて、ゾノトープの和集合による $X_Z$ のtight な包絡を計算する。
   • 包絡内の各ゾノトープに対して、勾配の集合ベース前方伝播とシステムのダイナミクスを用いてリー微分を包絡する。
   • 損失 $L_{III}$ は、これらのリー微分包絡の上限にペナルティを課す。

総損失は $L = L_I + L_{II} + L_{III}$ である。もし $L=0$ ならば、システムは形式的に安全として検証される。

B. 集合ベース前方伝播
これらの損失を計算するために、この手法はニューラルネットワークの層を通じてゾノトープ（特定の種類の凸多面体）を伝播させる：

• 線形層： アフィン写像を通じて正確に計算される。
• 非線形層： 保守的な過大近似（例：範囲バウンディング）を用いて包絡される。
• 勾配とリー微分： 勾配の集合が後方へ伝播され、リー微分は勾配集合とフロー集合の内積として計算される。

C. アルゴリズム
訓練ループ（アルゴリズム 1）は、ネットワークを初期化し、$P_I$、$P_{II}$、$P_{III}$ に対する集合ベース損失を計算し、勾配降下法を通じてパラメータを更新し、総損失がゼロになった時点で終了する。

3. 主要な貢献

1. 単一処理合成： 反復的な訓練・検証サイクルを排除し、単一の集合ベース訓練処理でニューラルバリア証明を合成する新しいアプローチ。
2. 健全な損失関数： バリア証明のすべての性質を健全に符号化する集合ベース損失。ゼロの損失値は、安全性の形式的証明を構成する。
3. 反復的洗練： 性質 P III に必要なゼロレベルセットとリー微分を動的に包絡するための反復処理。
4. 広範な評価： 線形、多項式、非多項式のダイナミクスを網羅する 13 のベンチマーク（高次元システム（最大 9 次元）や複雑な集合構成を含む）における評価。

4. 実験結果

このアプローチは CORA ツールボックスを用いて実装され、最先端のツールと比較された：SynNBC と FOSSIL（反復的な訓練・検証）、および PRoTECT（和の二乗最適化）。

• 成功率： 提案手法は、すべての 13 のベンチマークで100% の成功率を達成した。
  • 対照的に、SynNBC と PRoTECT は非多項式のダイナミクスや、複数の初期/不安全集合を持つベンチマークで失敗した。
  • FOSSIL は高い成功率を達成したが、高次元システムでは性能が低下した（例：Peruffo 6D で 70%、Peruffo 8D で 80%）。
• 実行時間： 集合ベース訓練アプローチは FOSSIL よりも著しく高速であった。例えば、Peruffo（8 次元）ベンチマークにおいて、提案手法の平均所要時間は1.0 秒であったのに対し、FOSSIL は47.7 秒を要した。
• 訓練効率： この手法は通常、数回の訓練エポックで収束した。対照的に、FOSSIL は多くの場合、複数の訓練・検証サイクルを必要とし、各サイクルは最大 1,000 エポックを要する可能性があった。
• アブレーション研究：
  • ネットワークアーキテクチャ： 浅いネットワーク（単一の線形層）は線形システムには十分であったが、非多項式システムでは失敗した。複雑なダイナミクスには、より深いネットワークが必要であった。
  • ゼロレベルセット包絡： より複雑なダイナミクスは、性質 P III を満たすために、より複雑なゼロレベルセット包絡（より多くの分割/反復）を必要とした。

5. 意義と主張

本論文は、訓練フェーズと検証フェーズを統合することで、安全検証におけるパラダイムシフトを代表するアプローチであると主張している。

• 形式的保証： 形式的な安全性保証を提供しない標準的なニューラルネットワーク訓練とは異なり、この手法は損失がゼロであれば有効なバリア証明であることを保証する。
• スケーラビリティ： 演効は効率的な行列乗算に還元され、システム次元に対してよくスケーリングする多項式複雑性を生み出す。
• 汎用性： このアプローチはシステムのダイナミクスに対してほぼ非依存であり、区間ベースの手法が困難とする複雑な非線形（非多項式）ダイナミクスや複雑な集合表現（例：集合の和、非凸領域）を自然に処理する。
• 効率性： 高コストな反復サイクルを排除することで、この手法は高次元および非線形システムに対する形式的検証へのより効率的な道筋を提供する。

著者らは、集合ベース合成が、後続の検証を必要とせずにバリア証明を効率的に生成でき、特に高次元および非多項式システムにおいて先行研究を上回る性能を発揮すると結論付けている。