On the Probabilistic Learnability of Compact Neural Network Preimage Bounds

TL;DR

This paper introduces a probabilistic, scalable method using ensemble of randomized decision trees to approximate neural network preimages with high-confidence guarantees, overcoming computational hardness limitations.

Contribution

It proposes RF-ProVe, a novel bootstrap-based approach that provides statistically guaranteed preimage bounds for neural networks, scalable to high-dimensional problems.

Findings

Provides formal statistical guarantees on region purity and coverage.

Demonstrates scalability where exact methods are infeasible.

Offers high-confidence approximations of neural network preimages.

Abstract

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.