A Unified Framework for Probabilistic Verification of AI Systems via
Weighted Model Integration
- URL: http://arxiv.org/abs/2402.04892v1
- Date: Wed, 7 Feb 2024 14:24:04 GMT
- Title: A Unified Framework for Probabilistic Verification of AI Systems via
Weighted Model Integration
- Authors: Paolo Morettin, Andrea Passerini and Roberto Sebastiani
- Abstract summary: Probability formal verification (PFV) of AI systems is in its infancy.
We propose a unifying framework for the PFV of AI systems based onWeighted Model Integration (WMI)
This reduction enables the verification of many properties of interest, like fairness, robustness or monotonicity, over a wide range of machine learning models.
- Score: 13.275592130089953
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
Related papers
- Investigating the Role of Instruction Variety and Task Difficulty in Robotic Manipulation Tasks [50.75902473813379]
This work introduces a comprehensive evaluation framework that systematically examines the role of instructions and inputs in the generalisation abilities of such models.
The proposed framework uncovers the resilience of multimodal models to extreme instruction perturbations and their vulnerability to observational changes.
arXiv Detail & Related papers (2024-07-04T14:36:49Z) - LoRA-Ensemble: Efficient Uncertainty Modelling for Self-attention Networks [52.46420522934253]
We introduce LoRA-Ensemble, a parameter-efficient deep ensemble method for self-attention networks.
By employing a single pre-trained self-attention network with weights shared across all members, we train member-specific low-rank matrices for the attention projections.
Our method exhibits superior calibration compared to explicit ensembles and achieves similar or better accuracy across various prediction tasks and datasets.
arXiv Detail & Related papers (2024-05-23T11:10:32Z) - A General Framework for Learning from Weak Supervision [93.89870459388185]
This paper introduces a general framework for learning from weak supervision (GLWS) with a novel algorithm.
Central to GLWS is an Expectation-Maximization (EM) formulation, adeptly accommodating various weak supervision sources.
We also present an advanced algorithm that significantly simplifies the EM computational demands.
arXiv Detail & Related papers (2024-02-02T21:48:50Z) - Multi-Agent Verification and Control with Probabilistic Model Checking [4.56877715768796]
Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems.
It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control.
In recent years, probabilistic model checking has also been extended to integrate ideas from game theory.
arXiv Detail & Related papers (2023-08-05T09:31:32Z) - GLUECons: A Generic Benchmark for Learning Under Constraints [102.78051169725455]
In this work, we create a benchmark that is a collection of nine tasks in the domains of natural language processing and computer vision.
We model external knowledge as constraints, specify the sources of the constraints for each task, and implement various models that use these constraints.
arXiv Detail & Related papers (2023-02-16T16:45:36Z) - Enhancing SMT-based Weighted Model Integration by Structure Awareness [10.812681884889697]
Weighted Model Integration (WMI) emerged as a unifying formalism for probabilistic inference in hybrid domains.
We develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure.
arXiv Detail & Related papers (2023-02-13T08:55:12Z) - On Robust Numerical Solver for ODE via Self-Attention Mechanism [82.95493796476767]
We explore training efficient and robust AI-enhanced numerical solvers with a small data size by mitigating intrinsic noise disturbances.
We first analyze the ability of the self-attention mechanism to regulate noise in supervised learning and then propose a simple-yet-effective numerical solver, Attr, which introduces an additive self-attention mechanism to the numerical solution of differential equations.
arXiv Detail & Related papers (2023-02-05T01:39:21Z) - SMT-based Weighted Model Integration with Structure Awareness [18.615397594541665]
We develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure.
This allows our algorithm to avoid generating redundant models, resulting in substantial computational savings.
arXiv Detail & Related papers (2022-06-28T09:46:17Z) - Efficient Model-Based Multi-Agent Mean-Field Reinforcement Learning [89.31889875864599]
We propose an efficient model-based reinforcement learning algorithm for learning in multi-agent systems.
Our main theoretical contributions are the first general regret bounds for model-based reinforcement learning for MFC.
We provide a practical parametrization of the core optimization problem.
arXiv Detail & Related papers (2021-07-08T18:01:02Z) - A general framework for modeling and dynamic simulation of multibody
systems using factor graphs [0.8701566919381223]
We present a novel general framework grounded in the factor graph theory to solve kinematic and dynamic problems for multi-body systems.
We describe how to build factor graphs to model and simulate multibody systems using both, independent and dependent coordinates.
The proposed framework has been tested in extensive simulations and validated against a commercial multibody software.
arXiv Detail & Related papers (2021-01-08T06:45:45Z) - Bayesian Stress Testing of Models in a Classification Hierarchy [0.0]
Building a machine learning solution in real-life applications often involves the decomposition of the problem into multiple models of various complexity.
We propose a Bayesian framework to model the interaction amongst models in such a hierarchy.
We show that the framework can facilitate stress testing of the overall solution, giving more confidence in its expected performance prior to active deployment.
arXiv Detail & Related papers (2020-05-25T18:22:07Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.