Towards a Unified Framework for Probabilistic Verification of AI Systems

The probabilistic formal verification (PFV) of modern AI systems is made particularly challenging by the widespread use of machine learning (ML) models. On the one hand, the techniques developed by the formal methods community are not suited to the verification of ML models. On the other hand, the contributions in the ML community so far have been limited to ad-hoc algorithms for specific classes of models and/or properties. First, we propose a unifying framework for the PFV of AI/ML systems, trying to frame the problem in the most general terms possible. Then, we show how to solve the quantitative verification task by reducing it to Weighted Model Integration (WMI) computations. We conclude by describing a number of open problems and research directions related to this promising approach.