TY - GEN
T1 - A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks
AU - Goubault, Eric
AU - Putot, Sylvie
N1 - Publisher Copyright:
© The Author(s) 2025.
PY - 2025/1/1
Y1 - 2025/1/1
N2 - The reliability and usefulness of verification depend on the ability to represent appropriately the uncertainty. Most existing work on neural network verification relies on the hypothesis of either set-based or probabilistic information on the inputs. In this work, we rely on the framework of imprecise probabilities, specifically p-boxes, to propose a quantitative verification of ReLU neural networks, which can account for both probabilistic information and epistemic uncertainty on inputs. On classical benchmarks, including the ACAS Xu examples, we demonstrate that our approach improves the tradeoff between tightness and efficiency compared to related work on probabilistic network verification, while handling much more general classes of uncertainties on the inputs and providing fully guaranteed results.
AB - The reliability and usefulness of verification depend on the ability to represent appropriately the uncertainty. Most existing work on neural network verification relies on the hypothesis of either set-based or probabilistic information on the inputs. In this work, we rely on the framework of imprecise probabilities, specifically p-boxes, to propose a quantitative verification of ReLU neural networks, which can account for both probabilistic information and epistemic uncertainty on inputs. On classical benchmarks, including the ACAS Xu examples, we demonstrate that our approach improves the tradeoff between tightness and efficiency compared to related work on probabilistic network verification, while handling much more general classes of uncertainties on the inputs and providing fully guaranteed results.
KW - Dempster-Shafer structures
KW - neural networks
KW - p-boxes
KW - probability bounds
KW - zonotopes
UR - https://www.scopus.com/pages/publications/85204540676
U2 - 10.1007/978-3-031-71162-6_17
DO - 10.1007/978-3-031-71162-6_17
M3 - Conference contribution
AN - SCOPUS:85204540676
SN - 9783031711619
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 324
EP - 342
BT - Formal Methods - 26th International Symposium, FM 2024, Proceedings
A2 - Platzer, André
A2 - Rozier, Kristin Yvonne
A2 - Pradella, Matteo
A2 - Rossi, Matteo
PB - Springer Science and Business Media Deutschland GmbH
T2 - 26th International Symposium on Formal Methods, FM 2024
Y2 - 9 September 2024 through 13 September 2024
ER -