Towards Probabilistic Verification of ML models via Weighted Model Integration

The probabilistic formal verification (PFV) of machine learning models is a vibrant research field. Existing approaches have generally relied on ad-hoc algorithms for specific classes of models and/or properties. I will present a unifying theoretical framework for the PFV of ML models based on reducing the problem to Weighted Model Integration, a relatively recent formalism for probabilistic inference with algebraic and logical constraints. This reduction enables the verification of many properties of interest, like fairness, robustness or monotonicity, over a wide range of ML models, without making strong distributional assumptions. After introducing the framework, I will outline several research avenues and challenges related to its application to large AI systems.