Probabilistic Verification of Neural Networks via E... | AI Research

Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation
This paper addresses the challenge of verifying the safety of deep neural networks (DNNs) when their inputs are subject to random disturbances, such as Gaussian noise. While traditional verification methods often provide deterministic answers, they struggle to account for the probabilistic nature of real-world inputs. The authors propose a new framework that estimates a guaranteed range for the probability that a neural network will satisfy safety constraints. By efficiently identifying "safe" and "unsafe" regions in the input space, the framework provides a rigorous bound on the likelihood of safe operation.

A New Approach to Probabilistic Verification

The core of this research is the generation of "probabilistic hulls"—bounded sets in the input space where the safety of the neural network can be guaranteed. By calculating the probability of these hulls, the framework establishes an upper and lower bound for the total safe probability. The authors move away from uniform partitioning, which is often computationally expensive and inefficient in high-dimensional spaces, in favor of a more targeted search strategy.

Regression Trees and Boundary Awareness

The framework introduces three primary innovations to improve efficiency: * Regression Tree-Guided Subdivision: Instead of splitting the input space uniformly, the method uses regression trees to partition the space. This allows the system to focus on regions that are likely to be purely safe or unsafe, avoiding unnecessary calculations in undecided areas. * Boundary-Aware Sampling: To effectively split the space, the system identifies the "safety boundary"—the transition point between safe and unsafe outputs. It uses a combination of distributional and uniform sampling to find points near this boundary, which are then used to guide the regression tree construction. * Iterative Refinement: The algorithm prioritizes the refinement of unknown regions that hold the highest probability mass. This incremental approach ensures that the most significant areas of the input space are verified first, leading to faster convergence.

Performance and Accuracy

The authors evaluated their framework using several benchmarks, including the ACAS Xu aircraft collision avoidance system and a rocket lander controller. The results demonstrate that this method is both more accurate and significantly faster than existing state-of-the-art techniques, achieving up to a 10x speedup compared to basic branch-and-bound approaches.

Key Considerations

The framework is designed to work with feedforward neural networks and provides a conservative estimate of safety. By iteratively subdividing the input space until the total probability of the remaining "unknown" regions falls below a specified threshold, the method guarantees that the actual safe probability of the network will fall within the calculated interval. This provides a reliable way to quantify uncertainty in safety-critical systems where inputs are modeled by random variables.