提出新方法提升神经网络概率验证效率与精度
BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks
- 基于预激活分裂的分支定界法，高效分割问题空间
- 在中高维输入下，验证精度优于现有最优方法
- 适合需要高可信度验证的AI系统研发人员
分支定界结合预激活分裂已被证明在确定性神经网络验证中非常有效。本文将其扩展至概率验证场景，提出BaB-prob方法：通过分裂预激活值迭代划分原问题为子问题，并利用线性边界传播计算各子问题的概率上界。我们证明了该方法对前馈ReLU神经网络具有正确性与完备性。进一步引入不确定性水平概念，设计两种高效预激活分裂策略，得到BaB-prob-ordered与BaB+BaBSR-prob。在未训练网络、MNIST与CIFAR-10模型以及VNN-COMP 2025基准测试中评估，结果表明，在中高维输入问题上，本方法持续优于当前最先进方法。
原文摘要 · Abstract (English)
Branch-and-bound with preactivation splitting has been shown highly effective for deterministic verification of neural networks. In this paper, we extend this framework to the probabilistic setting. We propose BaB-prob that iteratively divides the original problem into subproblems by splitting preactivations and leverages linear bounds computed by linear bound propagation to bound the probability for each subproblem. We prove soundness and completeness of BaB-prob for feedforward-ReLU neural networks. Furthermore, we introduce the notion of uncertainty level and design two efficient strategies for preactivation splitting, yielding BaB-prob-ordered and BaB+BaBSR-prob. We evaluate BaB-prob on untrained networks, MNIST and CIFAR-10 models, respectively, and VNN-COMP 2025 benchmarks. Across these settings, our approach consistently outperforms state-of-the-art approaches in medium- to high-dimensional input problems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。