Towards Probabilistic Verification of AI Systems via Weighted Model Integration
Abstract
The probabilistic formal verification (PFV) of AI systems 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 AI systems 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 machine learning 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.