The probabilistic formal verification (PFV) of AI systems is in its infancy. So far, approaches have been limited to ad-hoc algorithms for specific classes of models and/or properties. We propose a unifying framework for the PFV of AI systems based onWeighted Model Integration (WMI), which allows to frame the problem in very general terms. Crucially, 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. We support the generality of the approach by solving multiple verification tasks with a single, off-the-shelf WMI solver, then discuss the scalability challenges and research directions related to this promising framework.

翻译：人工智能系统的概率形式验证仍处于起步阶段。目前的方法局限于针对特定模型类别和/或属性的专用算法。我们提出了一种基于加权模型集成的AI系统概率形式验证统一框架，该框架能够以高度通用的方式表述问题。至关重要的是，这种转化使得在不做强分布假设的情况下，能够对多种机器学习模型验证包括公平性、鲁棒性或单调性在内的诸多关键属性。我们通过使用单一的现成加权模型集成求解器解决多个验证任务来支撑该方法的通用性，随后讨论了这一富有前景的框架所面临的可扩展性挑战及研究方向。