# Formal Reasoning About Confidence and Automated Verification of Neural Networks

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 25 of its 46 references that are in the map.
- First posted on arXiv 10 Nov 2025.

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

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Very Deep Convolutional Networks for Large-Scale Image Recognition](https://mlsanity.com/paper/1409.1556/) (2014)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [A Dual Approach to Scalable Verification of Deep Networks](https://mlsanity.com/paper/1803.06567/) (2018)
- [Exactly Computing the Local Lipschitz Constant of ReLU Networks](https://mlsanity.com/paper/2003.01219/) (2020)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [A case for new neural network smoothness constraints](https://mlsanity.com/paper/2012.07969/) (2020)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [DNNV: A Framework for Deep Neural Network Verification](https://mlsanity.com/paper/2105.12841/) (2021)
- [Convex Bounds on the Softmax Function with Applications to Robustness Verification](https://mlsanity.com/paper/2303.01713/) (2023)
- [A Quantitative Geometric Approach to Neural-Network Smoothness](https://mlsanity.com/paper/2203.01212/) (2022)
- [Exposing Previously Undetectable Faults in Deep Neural Networks](https://mlsanity.com/paper/2106.00576/) (2021)
- [Verifying Global Two-Safety Properties in Neural Networks with Confidence](https://mlsanity.com/paper/2405.14400/) (2024)
- [Relaxing Local Robustness](https://mlsanity.com/paper/2106.06624/) (2021)
- [Architecturing Binarized Neural Networks for Traffic Sign Recognition](https://mlsanity.com/paper/2303.15005/) (2023)

## Abstract (arXiv)

In the last decade, a large body of work has emerged on robustness of neural networks, i.e., checking if the decision remains unchanged when the input is slightly perturbed. However, most of these approaches ignore the confidence of a neural network on its output. In this work, we aim to develop a generalized framework for formally reasoning about the confidence along with robustness in neural networks. We propose a simple yet expressive grammar that captures various confidence-based specifications. We develop a novel and unified technique to verify all instances of the grammar in a homogeneous way, viz., by adding a few additional layers to the neural network, which enables the use any state-of-the-art neural network verification tool. We perform an extensive experimental evaluation over a large suite of 8870 benchmarks, where the largest network has 138M parameters, and show that this outperforms ad-hoc encoding approaches by a significant margin.