신경 피드백 시스템의 도달-회피 명세 검증을 위한 새로운 전략

A New Strategy for Verifying Reach-Avoid Specifications in Neural Feedback Systems

정방향 도달 가능성 분석은 신경 피드백 시스템(신경망으로 제어되는 동적 시스템)의 도달-회피 속성을 검증하는 데 있어 가장 주된 접근 방식이다. 이러한 현상은 기존 역방향 도달 가능성 분석 방법들의 제한된 확장성에서 기인한다. 본 연구에서는 이러한 시스템에 대해 역방향 도달 가능 집합의 상위 및 하위 근사를 모두 계산하는 새로운 알고리즘을 제안한다. 더 나아가, 우리는 신경 피드백 시스템을 위한 통합 검증 프레임워크를 제공하기 위해 이 역방향 알고리즘들을 기존의 정방향 분석 기법들과 통합한다.

Forward reachability analysis is the predominant approach for verifying reach-avoid properties in neural feedback systems (dynamical systems controlled by neural networks). This dominance stems from the limited scalability of existing backward reachability methods. In this work, we introduce new algorithms that compute both over- and under-approximations of backward reachable sets for such systems. We further integrate these backward algorithms with established forward analysis techniques to yield a unified verification framework for neural feedback systems.