Tightening the Evaluation of PAC Bounds Using Formal Verification Results

TL;DR

This paper proposes a novel method that leverages formal verification of neural networks to tighten PAC bounds, providing more practical and accurate probabilistic guarantees of model generalisation.

Contribution

It introduces a new approach combining formal verification with PAC bounds to improve their tightness for neural network models.

Findings

Verification-informed bounds are tighter than classical bounds.

Region-based verification improves the practical applicability of PAC bounds.

The method offers a scalable way to evaluate neural network generalisation.

Abstract

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.