POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems

要約

タイトル：ニューラルネットワーク管理システムの効率的かつ正確な形式的到達可能性解析のためのPOLAR-Express

要約：
– NNコントローラの役割を果たすニューラルネットワーク（NN）は、難しい制御問題で印象的な実証結果を示しています。
– ただし、NNコントローラの潜在的な採用は、特に安全重視のアプリケーションで使用される場合、これらのニューラルネットワーク管理システム（NNCS）の安全性に対する懸念を引き起こします。
– この作品では、NNCSの安全性を検証するための効率的で正確な形式的到達可能性解析ツールであるPOLAR-Expressを紹介します。
– POLAR-Expressは、Taylorモデル算術を使用して、ニューラルネットワーク層を超えてTaylorモデル（TM）を伝播させ、ニューラルネットワーク関数の過大評価を計算します。
– POLAR-Expressは、連続的な活性化関数を持つ任意のフィードフォワードニューラルネットワークを分析するために適用できます。
– ReLU活性化関数を超えてTMをより効率的かつ正確に伝播させるための新しいアプローチも提供します。
– さらに、POLAR-Expressは、レイヤーごとのTMの伝播に対する並列計算サポートを提供し、その効率性とスケーラビリティを以前のプロトタイプであるPOLARよりも大幅に改善します。
– diverse set of benchmarksを使用して、6つの他の最先端ツールとの比較において、POLAR-Expressは到達可能な集合の分析において最高の検証効率と緊密性を達成しています。

要約(オリジナル)

Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also gives rise to a growing concern over the safety of these neural-network controlled systems (NNCSs), especially when used in safety-critical applications. In this work, we present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of NNCSs. POLAR-Express uses Taylor model arithmetic to propagate Taylor models (TMs) across a neural network layer-by-layer to compute an overapproximation of the neural-network function. It can be applied to analyze any feed-forward neural network with continuous activation functions. We also present a novel approach to propagate TMs more efficiently and precisely across ReLU activation functions. In addition, POLAR-Express provides parallel computation support for the layer-by-layer propagation of TMs, thus significantly improving the efficiency and scalability over its earlier prototype POLAR. Across the comparison with six other state-of-the-art tools on a diverse set of benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI