Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

要約

近年、セーフティ クリティカルなシステムへのニューラル ネットワークの統合に大きな可能性が示されています。
ただし、ニューラル ネットワーク制御システム (NNCS) の安全性を効果的に検証するという課題は依然として残っています。
この論文では、帰納的不変法を活用した、NNCS の安全性検証への新しいアプローチを紹介します。
NNCS のコンテキストで帰納的不変量の候補の帰納性を検証することは、ニューラル ネットワークの規模と非線形性のため困難です。
私たちの構成手法では、帰納性証明義務をより小さく、より扱いやすい部分問題に分解することで、この検証プロセスを管理しやすくしています。
高レベルの方法に加えて、必要な分解述語を自動的に推論することによって、与えられた候補の帰納性を自動的に検証できるアルゴリズムを紹介します。
このアルゴリズムはベースライン手法を大幅に上回り、ケーススタディでは実行時間が大幅に短縮され、検証時間が数時間 (またはタイムアウト) から数秒に短縮されました。

要約(オリジナル)

The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. Verifying the inductiveness of a candidate inductive invariant in the context of NNCS is hard because of the scale and nonlinearity of neural networks. Our compositional method makes this verification process manageable by decomposing the inductiveness proof obligation into smaller, more tractable subproblems. Alongside the high-level method, we present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates. The algorithm significantly outperforms the baseline method and shows remarkable reductions in execution time in our case studies, shortening the verification time from hours (or timeout) to seconds.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google