Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification

Abstract

We improve the efficacy of bound-propagation-based neural network verification by reducing the computational effort required by state-of-the-art propagation methods without incurring any loss in precision. We propose a method that infers the stability of ReLU nodes at every step of the back-substitution process, thereby dynamically simplifying the coefficient matrix of the symbolic bounding equations. We develop a heuristic for the effective application of the method and discuss its evaluation on common benchmarks where we show significant improvements in bound propagation times.

Cite

Text

Kouvaros et al. "Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification." AAAI Conference on Artificial Intelligence, 2025. doi:10.1609/AAAI.V39I26.34949

Markdown

[Kouvaros et al. "Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification." AAAI Conference on Artificial Intelligence, 2025.](https://mlanthology.org/aaai/2025/kouvaros2025aaai-dynamic/) doi:10.1609/AAAI.V39I26.34949

BibTeX

@inproceedings{kouvaros2025aaai-dynamic,
  title     = {{Dynamic Back-Substitution in Bound-Propagation-Based Neural Network Verification}},
  author    = {Kouvaros, Panagiotis and Brückner, Benedikt and Henriksen, Patrick and Lomuscio, Alessio},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2025},
  pages     = {27383-27391},
  doi       = {10.1609/AAAI.V39I26.34949},
  url       = {https://mlanthology.org/aaai/2025/kouvaros2025aaai-dynamic/}
}