On the Probabilistic Learnability of Compact Neural Network Preimage Bounds
This provides a scalable solution for verifying neural network properties in high-dimensional spaces, addressing a bottleneck in safety-critical applications, though it is incremental as it builds on existing probabilistic approaches.
The paper tackles the scalability issue in computing preimage bounds for neural networks, which is #P-hard, by introducing a probabilistic method called RF-ProVe that uses random forests and active resampling to generate compact approximations with high-confidence guarantees and bounded error.
Although recent provable methods have been developed to compute preimage bounds for neural networks, their scalability is fundamentally limited by the #P-hardness of the problem. In this work, we adopt a novel probabilistic perspective, aiming to deliver solutions with high-confidence guarantees and bounded error. To this end, we investigate the potential of bootstrap-based and randomized approaches that are capable of capturing complex patterns in high-dimensional spaces, including input regions where a given output property holds. In detail, we introduce $\textbf{R}$andom $\textbf{F}$orest $\textbf{Pro}$perty $\textbf{Ve}$rifier ($\texttt{RF-ProVe}$), a method that exploits an ensemble of randomized decision trees to generate candidate input regions satisfying a desired output property and refines them through active resampling. Our theoretical derivations offer formal statistical guarantees on region purity and global coverage, providing a practical, scalable solution for computing compact preimage approximations in cases where exact solvers fail to scale.