Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

論文概要

本論文は、非線形動的制御システムに対するニューラル制御バリア関数（Neural Control Barrier Functions: Neural CBFs）の事後検証（post-hoc verification）における計算ボトルネックを解決するための、スケーラブルな検証フレームワークを提案しています。既存の手法はニューラルネットワークのサイズやシステムの次元が増大すると計算が困難になるという課題を抱えていましたが、提案手法は線形境界伝播（Linear Bound Propagation: LBP）とMcCormick 緩和を組み合わせることで、大規模なネットワークの検証を可能にしています。

1. 問題設定と背景

• 背景: 自律制御システム（ドローン、ロボットアームなど）の安全性保証には、制御バリア関数（CBF）が有効です。近年、表現力に優れたニューラルネットワークを CBF として学習する手法（Neural CBF）が注目されています。
• 課題: 学習されたニューラルネットワークが実際に有効な CBF であることを証明する「検証」プロセスが計算コストのボトルネックとなっています。
  • 既存の手法（SMT ソルバーや混合整数計画問題 MIP を用いる手法）は、非線形な条件を厳密に扱うため、ネットワークサイズが大きくなると計算が破綻します。
  • また、ReLU 以外の任意の非線形活性化関数を持つネットワークの勾配を効率的に評価する手法が不足していました。
• 目的: 任意の非線形活性化関数に対応し、大規模なニューラルネットワークでも検証可能な、効率的かつ保守的（conservative）な検証手法の確立。

2. 提案手法の核心

提案手法は、CBF の条件を満たすための厳密な非線形方程式を解くのではなく、線形の上界と下界を導出することで、検証を線形計画問題（または SAT 問題）の形式に帰着させるアプローチです。

A. 勾配に対する線形境界伝播（LBP）の拡張

• 従来の LBP はニューラルネットワークの出力値の境界を計算するものでしたが、CBF の条件には**勾配（ヤコビアン）**の情報が必要です。
• 本論文では、LBP を拡張し、ネットワークの勾配 $\frac{\partial B_\theta}{\partial x}$ に対する線形上界・下界を計算する手法を提案しました。
• 技術的工夫:
  • 各層のヤコビアン（活性化関数の微分と重み行列の積）を再帰的に境界付けます。
  • 層間の積（バilinear 項）を処理するために、McCormick 緩和を適用します。
  • これにより、ネットワークの勾配を $Ax + b$ の形式で近似する線形境界を得ることができます。

B. 動的システムと CBF 条件の線形緩和

• 対象システムのダイナミクス $f(x), g(x)$ に対しても、1 次テイラー展開とラグランジュ誤差評価を用いて線形境界を導出します。
• CBF の条件式（リー微分を含む式）における非線形項（$\nabla B \cdot f$ や $\nabla B \cdot g \cdot u$）を、導出した線形境界と McCormick 緩和を用いて線形近似（上界・下界）に変換します。
• これにより、元の非線形な検証条件 $\phi$ を、線形な代替式 $\phi_{linear}$ に置き換えます。$\phi_{linear}$ が満たされれば、元の条件も満たされることが保証されます。

C. 適応的領域分割（Refinement Strategy）

• 線形近似は領域が広いと過剰に保守的（誤差が大きい）になるため、検証が不確定になる場合があります。
• 提案手法では、状態空間を単体（Simplex）メッシュに分割し、検証が不確定な領域をその「最長辺」に沿って分割する適応的リファインメント戦略を採用しています。
• この分割は並列化可能であり、GPU を活用して多数の単体に対して同時に境界計算と SAT 判定を行うことで、大規模な検証タスクを効率的に処理します。

3. 主要な貢献

1. LBP と McCormick 緩和に基づく新規検証手法:
   • 高コストな SMT ソルバーに依存せず、線形境界伝播と緩和を用いてニューラル CBF を検証する手法を確立しました。これにより、より大規模なネットワークの検証が可能になりました。
2. 並列化可能な適応的リファインメント戦略:
   • 状態空間を単体メッシュで分割し、必要に応じて分割する戦略を開発しました。これにより、線形近似の過剰な保守性を低減し、GPU による並列計算を可能にしています。
3. 大規模ネットワークへのスケーラビリティの実証:
   • 既存の SMT ベースの手法（dreal など）と比較し、より大きなネットワーク（例：[64, 64] 以上の層を持つネットワーク）を短時間で検証できることを数値実験で示しました。

4. 実験結果

• ベンチマーク: 2D-Control, Cart-Pole, Darboux, Barrier 2/3/4 などの標準的な非線形制御問題および新規ベンチマークを使用。
• 活性化関数: Tanh 関数を使用（ReLU ベースの既存手法との比較は困難なため、SMT ソルバー dreal と比較）。
• 結果:
  • Barriers 2, 3, 4: 提案手法はすべて 100% 検証成功。dreal は Barrier 4 でタイムアウト、Darboux でもタイムアウトしました。
  • Cart-Pole: 約 300 万の領域分割を行いましたが、提案手法では約 2146 秒で検証完了しました（dreal は適用不可または非常に遅延）。
  • 性能: 提案手法は、SMT ソルバーに比べて検証時間を劇的に短縮し、より複雑な制御入力を含む問題（$\sup_{u \in U}$ の項を含む）を扱えることを示しました。

5. 意義と結論

• 実用性の向上: 学習されたニューラル CBF の安全性保証を、大規模なモデルに対しても現実的な時間で行えるようになりました。これにより、より複雑な動的システムや制約条件を持つ実世界への応用が可能になります。
• 汎用性: 任意の非線形活性化関数（Tanh, Sigmoid, ReLU など）と、制御入力を含む任意のアフィンシステムに対応可能です。
• 将来展望: 不変性（invariance）だけでなく、到達性（reachability）や回避（avoidance）などの仕様証明への拡張が今後の課題として挙げられています。

総じて、本論文はニューラルネットワークを用いた制御安全性保証の分野において、計算効率とスケーラビリティの両面から大きな飛躍をもたらす重要な成果です。