Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Probabilistic ML Verification via Weighted Model Integration

Paolo Morettin, Andrea Passerini, Roberto Sebastiani

TL;DR

This work proposes a unifying framework for the PFV of ML systems based on Weighted Model Integration (WMI), a relatively recent formalism for probabilistic inference with algebraic and logical constraints and substantiates the generality of the approach on prototypical tasks involving the verification of group fairness, monotonicity, robustness to noise, probabilistic local robustness and equivalence among predictors.

Abstract

In machine learning (ML) verification, the majority of procedures are non-quantitative and therefore cannot be used for verifying probabilistic models, or be applied in domains where hard guarantees are practically unachievable. The probabilistic formal verification (PFV) of ML models is in its infancy, with the existing approaches limited to specific ML models, properties, or both. This contrasts with standard formal methods techniques, whose successful adoption in real-world scenarios is also due to their support for a wide range of properties and diverse systems. We propose a unifying framework for the PFV of ML systems based on Weighted Model Integration (WMI), a relatively recent formalism for probabilistic inference with algebraic and logical constraints. Crucially, reducing the PFV of ML models to WMI enables the verification of many properties of interest over a wide range of systems, addressing multiple limitations of deterministic verification and ad-hoc algorithms. We substantiate the generality of the approach on prototypical tasks involving the verification of group fairness, monotonicity, robustness to noise, probabilistic local robustness and equivalence among predictors. We characterize the challenges related to the scalability of the approach and, through our WMI-based perspective, we show how successful scaling techniques in the ML verification literature can be generalized beyond their original scope.

Probabilistic ML Verification via Weighted Model Integration

TL;DR

This work proposes a unifying framework for the PFV of ML systems based on Weighted Model Integration (WMI), a relatively recent formalism for probabilistic inference with algebraic and logical constraints and substantiates the generality of the approach on prototypical tasks involving the verification of group fairness, monotonicity, robustness to noise, probabilistic local robustness and equivalence among predictors.

Abstract

In machine learning (ML) verification, the majority of procedures are non-quantitative and therefore cannot be used for verifying probabilistic models, or be applied in domains where hard guarantees are practically unachievable. The probabilistic formal verification (PFV) of ML models is in its infancy, with the existing approaches limited to specific ML models, properties, or both. This contrasts with standard formal methods techniques, whose successful adoption in real-world scenarios is also due to their support for a wide range of properties and diverse systems. We propose a unifying framework for the PFV of ML systems based on Weighted Model Integration (WMI), a relatively recent formalism for probabilistic inference with algebraic and logical constraints. Crucially, reducing the PFV of ML models to WMI enables the verification of many properties of interest over a wide range of systems, addressing multiple limitations of deterministic verification and ad-hoc algorithms. We substantiate the generality of the approach on prototypical tasks involving the verification of group fairness, monotonicity, robustness to noise, probabilistic local robustness and equivalence among predictors. We characterize the challenges related to the scalability of the approach and, through our WMI-based perspective, we show how successful scaling techniques in the ML verification literature can be generalized beyond their original scope.
Paper Structure (15 sections, 27 equations, 7 figures, 4 tables, 1 algorithm)

This paper contains 15 sections, 27 equations, 7 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction and motivation
  2. Related Work
  3. Background on Weighted Model Integration
  4. WMI-based ML verification
  5. Our unified theoretical perspective
  6. Modeling arbitrary distributions (D1)
  7. Modeling deterministic ML systems (D2)
  8. Modeling $\mathcal{R}_{I}$ and $\mathcal{R}_{O}$ (D3)
  9. Use case: an income classifier
  10. Scalability
  11. Experiments
  12. Probabilistic local robustness
  13. Probabilistic equivalence of predictors
  14. Conclusion and future work
  15. Ground truth distribution and training

Figures (7)

  • Figure 1: A scenario where global $\epsilon$-robustness is not achievable. The dashed red line and the blue area respectively depict the decision boundary and an arbitrarily small probability of the marginal $P(x)\xspace$.
  • Figure 2: (Left) The hybrid region defined in Ex. 1. (Center) The weighted formula in Ex. 2. (Right) An equivalent XADD representation of the weight.
  • Figure 3: Two structured densities supported by our framework: DETs (left) and SPNs (right).
  • Figure 4: (Left) A simple distribution $\Delta = (x \in [0,1])$ and $w(x) = x$. (Right) the distribution obtained by self-composition, enabling the computation of queries like $P(x' \in [x-\epsilon,x+\epsilon])\xspace$.
  • Figure 5: Graphical model of the generating distribution. The observed variables in the sampled data are circled. The dependency $female \rightarrow hw$ is only present in the biased dataset.
  • ...and 2 more figures

Theorems & Definitions (2)

  • Example 1
  • Example 2