提出高效生成概率包络的新方法,验证神经网络在扰动输入下的安全概率。
Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

- 用回归树划分状态空间生成概率包络
- 通过边界感知采样精准定位安全边界
- 迭代优化确保安全概率的严格上下界,适合高可靠系统验证
神经网络的概率验证问题关注当输入服从概率分布时,输出满足安全约束的概率。该问题在输入受扰动(常建模为随机变量)时尤为重要。本文提出一种新型神经网络概率验证框架,通过高效生成安全与不安全的概率包络,计算安全概率的保证范围。主要创新包括:(1) 使用回归树的状态空间划分策略生成概率包络;(2) 边界感知采样方法,利用样本识别输入空间中的安全边界,用于后续构建回归树;(3) 带概率优先级的迭代精化,以计算安全概率的保证范围。在ACAS Xu和火箭着陆控制器等多个基准测试中评估了方法的准确性和效率,结果明显优于现有最先进方法。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。