신경 피드백 시스템 검증을 위한 FABRIC 전략

The FABRIC Strategy for Verifying Neural Feedback Systems

신경 피드백 시스템, 즉 신경망에 의해 제어되는 동적 시스템에서 도달 가능 영역(reach-avoid) 사양을 검증하는 데 있어 순방향 도달 가능성 분석이 주된 방법으로 사용되어 왔으며, 이에 대한 다양한 연구가 진행되었습니다. 반면, 이러한 시스템에 대한 역방향 도달 가능성 분석은 알려진 기술의 확장성 제한으로 인해 상대적으로 덜 주목받아 왔습니다. 본 연구에서는 이러한 간극을 해소하기 위해, 비선형 신경 피드백 시스템의 역방향 도달 가능 영역에 대한 과대 근사(over-approximation) 및 과소 근사(under-approximation)를 계산하는 새로운 알고리즘을 제시합니다. 또한, 이러한 역방향 도달 가능성 기술을 기존의 순방향 분석 기술과 통합하는 방법을 설명하고 구현합니다. 결과적으로 얻어지는 알고리즘을 순방향 및 역방향 도달 가능성 통합 검증(Forward and Backward Reachability Integration for Certification, FaBRIC)이라고 명명했습니다. 저희는 제시하는 알고리즘을 대표적인 벤치마크 데이터셋에 적용하여 성능을 평가한 결과, 기존 최고 성능을 훨씬 능가하는 것을 확인했습니다.

Forward reachability analysis is a dominant approach for verifying reach-avoid specifications in neural feedback systems, i.e., dynamical systems controlled by neural networks, and a number of directions have been proposed and studied. In contrast, far less attention has been given to backward reachability analysis for these systems, in part because of the limited scalability of known techniques. In this work, we begin to address this gap by introducing new algorithms for computing both over- and underapproximations of backward reachable sets for nonlinear neural feedback systems. We also describe and implement an integration of these backward reachability techniques with existing ones for forward analysis. We call the resulting algorithm Forward and Backward Reachability Integration for Certification (FaBRIC). We evaluate our algorithms on a representative set of benchmarks and show that they significantly outperform the prior state of the art.