Verification of Unknown Dynamical Systems via Autoencoder Latent Space

技術的概要：オートエンコーダ潜在空間による未知ダイナミカルシステムの検証

問題定式化
連続空間ダイナミカルシステムの形式的検証は、自律システムが安全性や活性の仕様（しばしば線形時相論理（LTL）で表現される）を満たすことを保証するために不可欠である。標準的なアプローチは、モデル検査を可能にするために有限状態抽象化を構築することを含む。しかし、これらの手法は高次元設定において深刻なスケーラビリティの課題に直面しており、抽象化のサイズは状態空間の次元とともに指数関数的に増大する。この問題は、ダイナミクスが複雑で部分的に未知、あるいはブラックボックスである AI 搭載システム（例えば、LiDAR やカメラデータを処理するニューラルネットワークによって制御されるシステムなど）においてさらに悪化する。オートエンコーダなどのデータ駆動型の次元削減技術はスケーラビリティに対する潜在的な解決策を提供するが、通常は形式的な正しさの保証を欠いている。具体的には、高次元の仕様を学習された潜在空間にマッピングし、学習された潜在ダイナミクスが（非決定性を含む）元のシステムの挙動を忠実に表現していることを保証することは、依然として未解決の課題である。既存の手法は、しばしば柔軟性のために正しさを犠牲にするか、学習された表現には当てはまらないシステムのダイナミクスに関する強い仮定に依存している。

手法
提案されるフレームワークは、次元削減と抽象化ベースの検証を組み合わせることで、未知のダイナミクスを持つ高次元システムに対する形式的保証を提供し、これらの課題に対処する。このアプローチは以下の 4 つの主要な段階から構成される。

1. 凸オートエンコーダアーキテクチャ：潜在空間の解釈可能性を確保し、健全な推論を支援するために、著者は凸オートエンコーダを採用する。エンコーダは、特定の構造的制約を持つ入力凸ニューラルネットワーク（ICNN）に制限される。具体的には、厳密に単調な活性化関数（同相写像として機能するため）、単射的な最初の層とスキップ層、およびフルランクの重み行列である。この「接続入力 - 接続出力（CICO）」ネットワークと呼ばれるアーキテクチャは、潜在空間内の任意の連結集合の原像が、元の状態空間内の連結集合であることを保証する。この性質は、潜在次元がシステムの最小実現よりも低い場合に、写像の非単射性を処理する上で極めて重要である。

2. 潜在包含ダイナミクスの学習：次元削減により情報の損失が生じる可能性があるため、潜在空間内での進化は決定論的な差分方程式ではなく、包含ダイナミクス（集合値）としてモデル化される。著者は、集合値ダイナミクスに対するガウス過程回帰（GPR）の新しい定式化である「包含ガウス過程（Inclusion GPs）」を導入する。この手法は、ダイナミクスを、観測されていないパラメータ $c$ を含む差分方程式に従う高次元空間へ持ち上げる。この観測されていない座標を組み込んだ深層カーネルを学習することで、システムの進化を集合（具体的には潜在空間内の球）として予測し、再生核ヒルベルト空間（RKHS）解析に基づいた厳密な誤差限界を提供する。

3. 健全な有限抽象化の構築：学習された包含 GP を用いて、著者は潜在空間内に非決定性遷移システム（NTS）を構築する。

   • 領域マッピング：高次元の関心領域（安全、不安全、および目標集合）を潜在空間にマッピングする。エンコーダの凸性により、これらの集合のサンプリングベースの下近似と確率的な上近似（$\epsilon$-RandUp を使用）を効率的に行うことができる。
   • 遷移関係：抽象状態間の遷移は、回帰誤差と観測されていないパラメータ $c$ を考慮して、領域を包含 GP モデルを通じて伝播させることで計算される。これにより、抽象化が元のシステムのすべての可能な挙動を保守的に捉えることが保証される。
   • 正しさの保証：このフレームワークは、潜在 NTS 内の状態が到達 - 回避仕様を満たす場合、元の高次元システム内のすべての対応する軌道が、高い信頼度（$1-\delta$）でその仕様を満たすことを証明する。

4. 検証とデコード：標準的なモデル検査ツールを潜在 NTS に適用し、仕様を満たすことが保証される状態（$Q_{yes}$）、満たすことができない状態（$Q_{no}$）、および不確実な状態（$Q_?$）を特定する。エンコーダが凸であるため、満たす潜在状態を凸最適化を用いて元の高次元空間に効率的にデコードし、元のシステム内で安全であることが保証される初期状態の集合を特定することができる。

主な貢献
本論文は以下の 4 つの主要な貢献を行う。

1. 証明可能な正しさを有するマッピング：CICO エンコーダを用いて高レベルの仕様を潜在空間にマッピングする手法。形式的保証を維持しつつ、圧縮された表現に対する効率的な推論を可能にする。
2. 包含 GP：包含値（集合値）ダイナミクスに対するガウス過程回帰の新しい定式化。基礎となる観測されていないパラメータの明示的な知識を必要とせずに、差分包含によって支配される潜在ダイナミクスの学習を可能にする。
3. 健全な抽象化フレームワーク：包含 GP に基づいて潜在空間内で健全な有限抽象化を生成する完全なフレームワーク。正しさの証明とともに、元のシステムへの満足保証のマッピング手順を含む。
4. 実証的検証：LiDAR 入力を使用するニューラルネットワークによって制御される 26 次元システムを含む複数のシステムでのアプローチの実証。従来の抽象化手法と比較して、大幅なスケーラビリティの向上を示す。

結果
このアプローチは 3 つのケーススタディで評価された。

• 3D から 2D：最小実現システム。この手法は潜在空間全体を正常に検証したが、元の 3D 空間における従来のデータ駆動型抽象化は、遅い移動次元の不確実性により到達性の検証に失敗した。
• 6D から 2D：非線形観測を持つ過剰パラメータ化システム。この手法は、障害物がない場合の潜在空間の 100% を、障害物がある場合は 59.78% を検証した。対照的に、元の 6D 空間での抽象化を試みると状態爆発が発生し、時間制限内で目標自体以外の領域を検証できなかった。
• 26D から 2D：LiDAR 入力とニューラルネットワークコントローラを備えたロボットナビゲーションタスク。この手法は、システムのダイナミクスを最小限の非決定性で捉える 2D 潜在空間を正常に学習し、潜在空間の 50.0001% を検証した。これは、従来の手法では実行不可能な高次元観測空間を処理する能力を実証した。

重要性
本論文は、次元削減と形式的検証の間の重要なギャップを埋めると主張している。仕様のマッピングと学習された潜在ダイナミクスの両方に対して健全性の保証を提供することで、学習ベースの制御において一般的な問題である検証結果の偽陽性を排除する。著者は、このアプローチにより、既存の形式的手法では以前は達成不可能だった、未知のダイナミクスを持つ高次元システムのスケーラブルな検証が可能になると強調している。フレームワークは健全であるが、著者は控えめに限界を指摘しており、凸エンコーダへの制限（表現力の制限）や、ノイズの取り込みや制御合成に関する未解決の課題が含まれる。これらは今後の研究の方向性として特定されている。