# Probabilistic ML Verification via Weighted Model Integration

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 27 of its 60 references that are in the map.
- First posted on arXiv 7 Feb 2024.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Concrete Problems in AI Safety](https://mlsanity.com/paper/1606.06565/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [On Evaluating Adversarial Robustness](https://mlsanity.com/paper/1902.06705/) (2019)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Measuring Neural Net Robustness with Constraints](https://mlsanity.com/paper/1605.07262/) (2016)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Verifying Properties of Binarized Deep Neural Networks](https://mlsanity.com/paper/1709.06662/) (2017)
- [Quantitative Verification of Neural Networks And its Security Applications](https://mlsanity.com/paper/1906.10395/) (2019)
- [Probabilistic Verification of Fairness Properties via Concentration](https://mlsanity.com/paper/1812.02573/) (2018)
- [Robustness of Neural Networks: A Probabilistic and Practical Approach](https://mlsanity.com/paper/1902.05983/) (2019)
- [Towards Verified Artificial Intelligence](https://mlsanity.com/paper/1606.08514/) (2016)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Robustness Verification of Tree-based Models](https://mlsanity.com/paper/1906.03849/) (2019)
- [Neuro-Symbolic Verification of Deep Neural Networks](https://mlsanity.com/paper/2203.00938/) (2022)
- [Robustness Certification of Generative Models](https://mlsanity.com/paper/2004.14756/) (2020)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [Verifying Robustness of Gradient Boosted Models](https://mlsanity.com/paper/1906.10991/) (2019)
- [Versatile Verification of Tree Ensembles](https://mlsanity.com/paper/2010.13880/) (2020)
- [Scaling up Hybrid Probabilistic Inference with Logical and Arithmetic Constraints via Message Passing](https://mlsanity.com/paper/2003.00126/) (2020)
- [Robustness Verification of Support Vector Machines](https://mlsanity.com/paper/1904.11803/) (2019)
- [Approximate Counting in SMT and Value Estimation for Probabilistic Programs](https://mlsanity.com/paper/1411.0659/) (2014)
- [Verifying Tree Ensembles by Reasoning about Potential Instances](https://mlsanity.com/paper/2001.11905/) (2020)
- [Enhancing SMT-based Weighted Model Integration by Structure Awareness](https://mlsanity.com/paper/2302.06188/) (2023)
- [SMT-based Weighted Model Integration with Structure Awareness](https://mlsanity.com/paper/2206.13856/) (2022)

## Abstract (arXiv)

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.