# Propagation of~Interval Belief Structures and~Imprecise Copulas for~Neural Network Verification

arXiv: https://arxiv.org/abs/2606.30105 · HTML: https://mlsanity.com/paper/2606.30105/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 28 references that are in the map.
- First posted on arXiv 29 Jun 2026.

## Builds on (most cited first, 4 of 4)

- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Scalable Quantitative Verification For Deep Neural Networks](https://mlsanity.com/paper/2002.06864/) (2020)
- [CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks](https://mlsanity.com/paper/2109.10696/) (2021)
- [PROVEN: Certifying Robustness of Neural Networks with a Probabilistic Approach](https://mlsanity.com/paper/1812.08329/) (2018)

## Built on by (most cited first, 1 of 1)

- [Ceci n'est pas une pipe: AI systems as semantic abstractions](https://mlsanity.com/paper/2607.09489/) (2026)

## Abstract (arXiv)

Quantitative verification of neural networks requires reasoning about probabilities under substantial uncertainty in both input distributions and their dependence structure. In realistic settings, this information is often only partially specified, and assuming precise probabilistic models can lead to unreliable results. We propose a sound framework for quantitative verification under imprecise probabilistic information, combining interval belief structures to represent marginal uncertainty with imprecise copulas to model uncertain dependence. We develop a propagation method for imprecisely coupled interval belief structures through feed-forward neural networks. Using mixed imprecise copula volumes, we derive sound push-forward constructions through affine transformations and activation functions. The resulting output can provide guaranteed lower and upper bounds on probabilistic safety properties, valid for all probability models compatible with the specified imprecise inputs.