# Tightening the Evaluation of PAC Bounds Using Formal Verification Results

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 18 references that are in the map.
- First posted on arXiv 29 Jul 2024.

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

- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Computing Nonvacuous Generalization Bounds for Deep (Stochastic) Neural Networks with Many More Parameters than Training Data](https://mlsanity.com/paper/1703.11008/) (2017)
- [Stronger generalization bounds for deep nets via a compression approach](https://mlsanity.com/paper/1802.05296/) (2018)
- [Non-Vacuous Generalization Bounds at the ImageNet Scale: A PAC-Bayesian Compression Approach](https://mlsanity.com/paper/1804.05862/) (2018)
- [Enhancing Adversarial Training with Second-Order Statistics of Weights](https://mlsanity.com/paper/2203.06020/) (2022)
- [A PAC-Bayes Analysis of Adversarial Robustness](https://mlsanity.com/paper/2102.11069/) (2021)
- [PROVEN: Certifying Robustness of Neural Networks with a Probabilistic Approach](https://mlsanity.com/paper/1812.08329/) (2018)
- [Improving Robust Generalization by Direct PAC-Bayesian Bound Minimization](https://mlsanity.com/paper/2211.12624/) (2022)

## Abstract (arXiv)

Probably Approximately Correct (PAC) bounds are widely used to derive probabilistic guarantees for the generalisation of machine learning models. They highlight the components of the model which contribute to its generalisation capacity. However, current state-of-the-art results are loose in approximating the generalisation capacity of deployed machine learning models. Consequently, while PAC bounds are theoretically useful, their applicability for evaluating a model's generalisation property in a given operational design domain is limited. The underlying classical theory is supported by the idea that bounds can be tightened when the number of test points available to the user to evaluate the model increases. Yet, in the case of neural networks, the number of test points required to obtain bounds of interest is often impractical even for small problems. In this paper, we take the novel approach of using the formal verification of neural systems to inform the evaluation of PAC bounds. Rather than using pointwise information obtained from repeated tests, we use verification results on regions around test points. We show that conditioning existing bounds on verification results leads to a tightening proportional to the underlying probability mass of the verified region.