Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound

David Boetius, Stefan Leue, Tobias Sutter

arXiv · PDF · Open in the Atlas

Code that ran

We lifted 3 functions out of this paper's own repositories and ran 3 of them in a sandbox. "Ran" means the function executed on a synthesized input and returned a value. It is not a reproduction of the paper's results.

Repositories linked to this paper

• sen-uni-kn/probspecs — marked official in Papers with Code; named in the paper

Some links come from the archived Papers with Code dataset (CC BY-SA 4.0): attribution and licence.

Abstract

Probabilistic verification problems of neural networks are concerned with formally analysing the output distribution of a neural network under a probability distribution of the inputs. Examples of probabilistic verification problems include verifying the demographic parity fairness notion or quantifying the safety of a neural network. We present a new algorithm for solving probabilistic verification problems of neural networks based on an algorithm for computing and iteratively refining lower and upper bounds on probabilities over the outputs of a neural network. By applying state-of-the-art bound propagation and branch and bound techniques from nonprobabilistic neural network verification, our algorithm significantly outpaces existing probabilistic verification algorithms, reducing solving times for various benchmarks from the literature from tens of minutes to tens of seconds. Furthermore, our algorithm compares favourably even to dedicated algorithms for restricted probabilistic verification problems. We complement our empirical evaluation with a theoretical analysis, proving that our algorithm is sound and, under mildly restrictive conditions, also complete when using a suitable set of heuristics.

For agents

The same record, over MCP at https://syntology.ai/mcp:

get_harvested_code_for_paper("2405.17556")
get_code_for_paper("2405.17556")
have("2405.17556")

Connect an agent — have() is free.