효율적인 확률적 헐 생성 기반 신경망의 확률적 검증

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

신경망의 확률적 검증 문제는 입력이 확률 분포로 주어질 때, 출력 공간에서 안전 제약 조건을 만족할 확률을 조사하는 것입니다. 입력이 확률 변수로 모델링된 잡음에 영향을 받는 경우, 이 문제를 해결하는 것은 매우 중요합니다. 본 논문에서는 안전 확률에 대한 보장된 범위를 효율적으로 계산하기 위해 안전 및 안전하지 않은 확률적 헐을 찾는 새로운 신경망 확률적 검증 프레임워크를 제안합니다. 우리 접근 방식은 세 가지 주요 혁신으로 구성됩니다. (1) 회귀 트리를 사용하여 확률적 헐을 생성하는 상태 공간 분할 전략, (2) 안전 경계를 식별하기 위해 회귀 트리 구축에 사용되는 샘플을 활용하는 경계 인식 샘플링 방법, (3) 안전 확률에 대한 보장된 범위를 계산하기 위한 확률적 우선순위를 사용하는 반복적 개선. 제안하는 방법의 정확성과 효율성은 ACAS Xu 및 로켓 착륙 컨트롤러를 포함한 다양한 벤치마크에서 평가되었으며, 그 결과는 최첨단 기술에 비해 뚜렷한 장점을 보였습니다.

The problem of probabilistic verification of a neural network investigates the probability of satisfying the safe constraints in the output space when the input is given by a probability distribution. It is significant to answer this problem when the input is affected by disturbances often modeled by probabilistic variables. In the paper, we propose a novel neural network probabilistic verification framework which computes a guaranteed range for the safe probability by efficiently finding safe and unsafe probabilistic hulls. Our approach consists of three main innovations: (1) a state space subdivision strategy using regression trees to produce probabilistic hulls, (2) a boundary-aware sampling method which identifies the safety boundary in the input space using samples that are later used for building regression trees, and (3) iterative refinement with probabilistic prioritization for computing a guaranteed range for the safe probability. The accuracy and efficiency of our approach are evaluated on various benchmarks including ACAS Xu and a rocket lander controller. The result shows an obvious advantage over the state of the art.