技術要約：非線形ダイナミクスの認証済みニューラル近似

問題定義

非線形力学系はサイバー物理システムにおいて基本的であるものの、直接的な検証や制御が困難である。一般的な戦略は、元のシステムを近似する抽象化（abstraction）――すなわち、簡略化されたモデルを構築することである。ニューラルネットワークは、状態空間を暗黙的に分割し、簡略化されたダイナミクスを学習できることから、この目的のための効果的なツールとして台頭している。

しかし、これらのニューラル抽象化をクリティカルなアプリケーションで安全に使用するためには、真のシステムに対する近接性に関する**形式的な保証（formal guarantees）**を備えていなければならない。具体的には、与えられた領域において、ニューラルネットワーク $N(x)$ が真のダイナミクス $f(x)$ を一定の誤差 $\epsilon$ 以内で近似していること（すなわち、$\|f(x) - N(x)\|_\infty \le \epsilon$）を証明する必要がある。

既存の検証手法は、非線形実算術を推論するために SMT（充足可能性モジュロ理論）ソルバー（例：dReal）に大きく依存している。これらは健全（sound）ではあるものの、深刻なスケーラビリティの限界に直面しており、多くの場合、合理的な時間内に大規模なネットワークや高次元のシステムを検証することに失敗する。この計算上のボトルネックが、複雑で高次元なシナリオにおけるニューラル抽象化の実用的な適用を制限している。

手法

著者らは、高価なSMTソルバーによる非線形算術への依存を排除する、新しいスケーラブルな検証フレームワークを提案する。代わりに、この手法は認証済み一次テイラーモデル（certified first-order Taylor models）と並列化可能な適応的分割戦略を活用する。

1. 認証済み一次テイラーモデル

非線形述語 $\exists x : \|f(x) - N(x)\| > \epsilon$ を直接検証するのではなく、本手法では一次テイラー展開を用いて、真のダイナミクス $f(x)$ を局所的に近似する。

• 局所線形化: 入力ドメイン $X$ はハイパーレクタングル（超矩形）に分割される。中心 $c$ を持つ各ハイパーレクタングル $H_\delta(c)$ 内において、ダイナミクスは線形関数と剰余項によって境界付けられる：
  $$f(x) \in (f(c) + J_f(c)(x - c)) \oplus R$$
  ここで、$J_f(c)$ はヤコビ行列であり、$R$ は（滑らかな関数のための）ラグランジュ誤差項、またはCROWN（ReLUネットワーク用）から導出された認証済み誤差範囲である。
• 線形ソルバーによる検証: この変換により、検証問題は線形不等式の充足可能性チェックへと変換される。著者らは、線形境界伝搬に基づくニューラルネットワーク検証ツールである Marabou 2.0 を使用して、これらの条件を検証する。これにより、非線形算術の推論に伴う計算コストを回避している。

2. 適応的証明書精緻化（Adaptive Certificate Refinement）

線形近似によって導入される保守性（誤差範囲 $R$ が緩すぎる場合）に対処するため、フレームワークは適応的な精緻化戦略を採用している。

• 分割基準: 以下の条件を満たす場合にハイパーレクタングルを分割する：
  1. テイラー剰余の境界が保守的すぎる場合（$R_{max} - R_{min} > \epsilon$）。
  2. ソルバーによって発見された潜在的な反例が、真の誤差条件を満たさない場合（線形化による「偽」の反例）。
• ターゲット分割: 分割軸は、近似誤差への入力次元の寄与度に基づいて選択され、非線形項に関与する次元を優先する。これにより、出力依存の精緻化が可能となり、出力次元ごとに異なるレベルの分割が必要となる場合がある。
• 並列化: 検証プロセスは、共有スタック（深さ優先探索）を使用して並列化され、ワーカープロセスのプールによってアクセスされる。各ワーカーは、ハイパーレクタングルを処理し、それを認証するか、あるいは分割してサブ領域をスタックに戻す。

3. 学習

ニューラルネットワークは、サンプリングされた入力に対する平均二乗誤差と最大 $L_\infty$ 誤差の両方を最小化するように学習される。損失関数には、検証のためのサンプル効率を向上させるために、最悪ケースの誤差に関する項が含まれている。

主な貢献

1. SMTフリーの検証: 認証済み線形化に基づく手法を導入することで、従来のアプローチの主要なボトルネックであった非線形実算術の推論を排除した。
2. 適応的並列精緻化: 入力ドメイン全体で非一様な精度を実現する適応的検証を可能にし、保守性を大幅に減少させつつ、健全性を損なわないスケーラブルな戦略を提供した。
3. スケーラビリティ: 高次元のシステム（最大7次元）や、最先端の手法よりも大幅に大きなニューラルネットワークを扱える能力。
4. 新規の応用: 以前は困難であった2つのシナリオへニューラル抽象化を拡張した：
   • ニューラルネットワーク圧縮: 圧縮されたネットワークが、より大きな「教師」ネットワークに対して $\epsilon$-close であることを検証する。
   • コープマン演算子の発見: ネットワークの出力が将来の状態のシーケンスを表す、軌道レベルの予測を検証する（最終層で100以上の状態）。

実験結果

本手法は、文献における確立されたベンチマーク（例：WaterTank、JetEngine、Van der Pol Oscillator）および新しい挑戦的なタスクを用いて評価された。

• 性能 vs 最先端手法: 文献のdRealベースの手法（Abate et al., 2022）と比較して、提案手法は大幅な高速化を示した。例えば、WaterTankベンチマークにおいて、提案手法は近似820倍高速であった。dRealは、ほとんどの大きなモデル（例：JetEngineの3x[64]アーキテクチャ、SteamGovernor）でタイムアウト（1時間の制限）したが、提案手法は、Low Thrust Spacecraft（7D）のような高次元システムを含む、テストされたすべてのモデルに対してドメインの100%を認証することに成功した。
• コープマン演算子: フレームワークは、コープマン理論に基づく軌道予測ネットワークの検証に成功した。このネットワークは検証データに対して低い平均二乗誤差を達成していたが、検証プロセスにより、誤差が許容範囲（$\epsilon=0.1$）を超える特定の反例が特定された。極めて重要なことに、本手法は入力ドメインの**99.03%**を認証し、単一の反例のみを返す手法にはない、モデルが信頼できる箇所に関する詳細な洞察を提供した。
• ニューラル圧縮: 本手法は、ローレンツ・アトラクタのダイナミクスを近似する圧縮ネットワーク（4.2Mから67kパラメータへ、98.4%の削減）を検証した。検証プロセスは350万個以上のハイパーレクタングルを処理し、約89時間で完了した。これは、大規模で非解析的なダイナミクスに対する実現可能性を示している。

意義と主張

本論文の主な意義は、ニューラル抽象化の検証におけるスケーラビリティのボトルネックを解決したことにあると主張している。検証の対象となるニューラルネットワーク（局所線形化と精緻化によって処理）と、非線形ダイナミクス（非線形実算術の推論）を切り離すことで、これまで困難であった複雑で高次元なシステムの形式的検証を可能にした。

著者らは、そのアプローチが形式的な誤差範囲を提供し、誤差を有界な摂動として解釈することで、ニューラル近似を安全なサロゲートとして利用できることを強調している。この健全性により、抽象化上で検証された特性（安全性や到達可能性など）を、具体的なシステムへと厳密に転送することが可能となる。また、本研究は、標準的な力学系を超えて、ネットワーク圧縮や演算理論のためのディープラーニング・アーキテクチャといった一般的な関数近似タスクにも適用可能であることを示しており、その汎用性を浮き彫りにしている。