Verification of Neural Reachable Tubes via Scenario Optimization and Conformal Prediction

要約

セーフティクリティカルなシステムを制御するための学習ベースのアプローチの人気が急速に高まっています。
したがって、その性能と安全性を確保することが重要です。
ハミルトン・ヤコビ (HJ) 到達可能性分析は、一般的な非線形システム ダイナミクス、境界のある敵対的システムの外乱、および状態と入力の制約を処理できるため、このような保証を提供するための一般的な形式的検証ツールです。
ただし、その計算とメモリの複雑さは状態の次元に応じて指数関数的に増加するため、大規模システムでは扱いにくくなります。
この課題を克服するために、DeepReach などのニューラル アプローチが、高次元システム用の到達可能なチューブと安全コントローラーを合成するために使用されてきました。
ただし、これらの到達可能な神経管を検証することは依然として困難です。
この研究では、堅牢なシナリオ最適化と等角予測に基づいて、神経到達可能管の確率的安全性保証を提供する 2 つの検証方法を提案します。
私たちの方法では、学習ベースのアプローチでは避けられない神経管の外れ値エラーに対する回復力と、確率的安全保証の強度との間の直接のトレードオフが可能です。
さらに、機械学習コミュニティで不確実性の定量化に広く使用されている手法であるスプリットコンフォーマル予測が、シナリオベースのアプローチに縮小され、到達可能な神経管の検証だけでなく、より一般的に 2 つの手法が同等になることを示します。
私たちの知る限り、私たちの証明は、等角予測とシナリオ最適化の間の強い関係を示す文献としては初めてです。
最後に、到達可能な神経管内の誤差分布を使用して、より大きな安全なボリュームを回復する、外れ値を調整した検証アプローチを提案します。
我々は、複数車両の衝突回避と立ち入り禁止区域でのロケット着陸という高次元の問題に対する、提案されたアプローチの有効性を実証します。

要約(オリジナル)

Learning-based approaches for controlling safety-critical systems are rapidly growing in popularity; thus, it is important to assure their performance and safety. Hamilton-Jacobi (HJ) reachability analysis is a popular formal verification tool for providing such guarantees, since it can handle general nonlinear system dynamics, bounded adversarial system disturbances, and state and input constraints. However, its computational and memory complexity scales exponentially with the state dimension, making it intractable for large-scale systems. To overcome this challenge, neural approaches, such as DeepReach, have been used to synthesize reachable tubes and safety controllers for high-dimensional systems. However, verifying these neural reachable tubes remains challenging. In this work, we propose two verification methods, based on robust scenario optimization and conformal prediction, to provide probabilistic safety guarantees for neural reachable tubes. Our methods allow a direct trade-off between resilience to outlier errors in the neural tube, which are inevitable in a learning-based approach, and the strength of the probabilistic safety guarantee. Furthermore, we show that split conformal prediction, a widely used method in the machine learning community for uncertainty quantification, reduces to a scenario-based approach, making the two methods equivalent not only for verification of neural reachable tubes but also more generally. To our knowledge, our proof is the first in the literature to show a strong relationship between conformal prediction and scenario optimization. Finally, we propose an outlier-adjusted verification approach that uses the error distribution in neural reachable tubes to recover greater safe volumes. We demonstrate the efficacy of the proposed approaches for the high-dimensional problems of multi-vehicle collision avoidance and rocket landing with no-go zones.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google