Generating Formal Safety Assurances for High-Dimensional Reachability

要約

自律システムに正式な安全性とパフォーマンスの保証を提供することがますます重要になっています。
ハミルトン・ヤコビ (HJ) 到達可能性分析は、一般的な非線形システム ダイナミクス、境界のある敵対的システムの外乱、および状態と入力の制約を処理できるため、これらの保証を提供するための一般的な形式的検証ツールです。
ただし、これには偏微分方程式を解く必要があり、その計算とメモリの複雑さは状態の次元に対して指数関数的に増加するため、大規模システムでの直接使用は困難になります。
最近提案された DeepReach と呼ばれる手法は、高次元の到達可能性問題に対して正弦波ニューラル PDE ソルバーを活用することでこの課題を克服します。その計算要件は、状態空間の次元ではなく、基礎となる到達可能なチューブの複雑さに応じて拡大します。
残念ながら、ニューラル ネットワークはエラーを起こす可能性があるため、計算された解は安全ではない可能性があり、正式な安全保証を提供するという重要な目標を達成するには至っていません。
この研究では、DeepReach ソリューションの誤差限界を計算する方法を提案します。
この誤差限界は、到達可能なチューブの補正に使用でき、その結果、真の到達可能なチューブの安全な近似が得られます。
また、一般的な非線形動的システムに対するこの誤差補正の確率的限界を計算するためのシナリオベースの最適化アプローチも提案します。
我々は、高次元のロケット着陸および複数車両の衝突回避問題に対して確率的に安全な到達可能なチューブを取得する際の、提案されたアプローチの有効性を実証します。

要約(オリジナル)

Providing formal safety and performance guarantees for autonomous systems is becoming increasingly important. Hamilton-Jacobi (HJ) reachability analysis is a popular formal verification tool for providing these guarantees, since it can handle general nonlinear system dynamics, bounded adversarial system disturbances, and state and input constraints. However, it involves solving a PDE, whose computational and memory complexity scales exponentially with respect to the state dimensionality, making its direct use on large-scale systems intractable. A recently proposed method called DeepReach overcomes this challenge by leveraging a sinusoidal neural PDE solver for high-dimensional reachability problems, whose computational requirements scale with the complexity of the underlying reachable tube rather than the state space dimension. Unfortunately, neural networks can make errors and thus the computed solution may not be safe, which falls short of achieving our overarching goal to provide formal safety assurances. In this work, we propose a method to compute an error bound for the DeepReach solution. This error bound can then be used for reachable tube correction, resulting in a safe approximation of the true reachable tube. We also propose a scenario-based optimization approach to compute a probabilistic bound on this error correction for general nonlinear dynamical systems. We demonstrate the efficacy of the proposed approach in obtaining probabilistically safe reachable tubes for high-dimensional rocket-landing and multi-vehicle collision-avoidance problems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google