Formal verification under uncertainty

Being able to ensure that AI systems behave as intended is essential for their adoption in many areas. This series covers formal methods for the verification of safety, fairness, and other relevant properties of (probabilistic) ML systems. We document the progress in research domains such as neuro-symbolic verification, probabilistic model-checking, and weighted model integration.

Formal Verification

Formal verification within the domain of artificial intelligence is an essential discipline focusing on the reliable, safe, and equitable operation of AI systems. This interdisciplinary field intersects with domains such as probabilistic modeling, neural network analysis, and algorithmic safety mechanisms. A concise overview of its primary aspects is provided below:

Probabilistic Model Checking: This method involves calculating the likelihood of specific outcomes within AI models [Kat16P], including Markov chains [Bai03M], Bayesian networks [Jan22P], probabilistic programs [Bat23P], or Markov decision processes [Har23P]. Through the assessment of these probabilities, researchers are able to predict and verify the behavior of AI systems under conditions of uncertainty. Fault tree analysis is commonly employed in this context to identify potential system failures [Vol18F, Jun16U].

Neural Network Verification: This procedure verifies whether a neural network model conforms to specified logical conditions. Neuro-symbolic approaches are at the forefront in this area, utilizing reference networks that encapsulate high-level concepts to enhance specification compliance [Xie22N].

Shielding: This strategy involves training an AI agent without constraints followed by the implementation of a safe fallback policy. This policy is activated when the agent’s proposed action is identified as potentially harmful, thus ensuring operational safety without compromising the learning process [Xia21B].

Methods and Applications

From a methodological perspective, formal verification in AI utilizes tools such as Satisfiability Modulo Theories (SMT) [Ehl17F], semi-definite programming [Faz20S, Kat17R], and weighted model integration [Mor21H] to analyze and ensure adherence to complex specifications. Abstract interpretation assists in understanding and verifying the properties of AI systems by approximating their behaviors.

In terms of applications, formal verification aims to enhance the robustness, safety, and fairness of AI systems. These objectives are crucial for the deployment of AI across various sectors, requiring dependable methods to ensure that AI behavior aligns with ethical and operational standards. A significant ongoing challenge in this field is the expansion of verification capabilities to encompass more complex systems and nuanced properties, as well as to increase the scalability of verification methods. This evolution underscores the need for innovative approaches to ensure that AI systems perform as intended, even in complex and unpredictable scenarios.

Software

The state of software and competition in formal verification for AI is characterized by rapid evolution, demonstrating the community’s dedication to advancing the field. Competitions such as the Verification of Neural Networks Competition (VNNComp) [Mul22T] and QComp [Bud21C] serve as critical platforms for researchers and practitioners to test and benchmark their methods against both real-world and synthetic challenges. These competitions not only highlight progress but also promote innovation by presenting complex scenarios requiring novel solutions.

Among the software tools having significant impact, $\alpha$-$\beta$-CROWN is notable for its efficacy in neural network verification, providing tight and scalable bounds for neural network properties through abstract interpretation. Marabou offers another robust platform for neural network verification, based on SMT [Kat19M]. Caisar provides a unified interface that facilitates the use of the aforementioned frameworks and others, offering a comprehensive platform for neural network verification [Gir22C]. On the probabilistic side, Storm is distinguished for its thorough support for probabilistic model checking, capable of managing various models such as Markov chains and Markov decision processes with precision and efficiency [Hen22P].

These tools and competitions illustrate the dynamic interplay between theory and practice in formal verification. They not only highlight the current capabilities and achievements in ensuring AI system reliability and safety but also emphasize the ongoing need for innovative approaches to address the increasingly complex landscapes of AI applications. As the field expands, the continuous development and refinement of these tools, along with the insights gained from competitive benchmarking, are crucial for pushing the boundaries of verifiable properties, ensuring that AI systems are both powerful and trustworthy.

Research feed

Training

Verifying Systems in the Face of Uncertainty

A 1-day workshop introducing the concept of probabilistic model checking and its applications with the library Storm.

Pill

Neuro Symbolic Verification of Deep Neural Networks

The neuro-symbolic approach to verification of neural networks uses reference networks to represent high level concepts. This allows the …

Formal Verification Under Uncertainty

Sep 26, 2022

Pill

Probabilistic Inference With Algebra and Logic Constraints

Hybrid probabilistic inference allows performing probabilistic inference with algebra and logic constraints. Recent advances with emphasis …

Formal Verification Under Uncertainty

Sep 23, 2022

Pill

BarrierNet: A Safety-Guaranteed Layer for Neural Networks

A strategy for encoding constraints on the state space of a control problem as a differentiable layer for neural network based controllers …

Formal Verification Under Uncertainty

Jan 24, 2022

Other series in Safety and reliability in ML systems

Robustness in ML

The robustness of a model is a measure of its stability with respect to perturbations of the input. We investigate and review recent …

Safety and Reliability in ML Systems

Anomaly detection

Many industrial applications of automated decision-making involve the detection of anomalous behaviour. Precisely defining what this means …

Safety and Reliability in ML Systems

Check all of our work

References

[Kat17R]

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks, Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer.

2017

Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The …

[Xie22N]

Neuro-Symbolic Verification of Deep Neural Networks, Xuan Xie, Kristian Kersting, Daniel Neider.

Jul 2022

Formal verification has emerged as a powerful approach to ensure the safety and reliability of deep neural networks. However, current verification tools are limited to only a handful of properties that can be expressed as first-order constraints over the inputs and output of a network. While adversarial robustness and fairness fall under this category, many real-world properties (e.g., "an …

[Bai03M]

Model-checking algorithms for continuous-time Markov chains, C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen.

Jun 2003

Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this …

[Bat23P]

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.

Jan 2023

Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties by generating inductive invariants on source-code level. Our implementation shows promise: It finds invariants for …

[Har23P]

A Practitioner's Guide to MDP Model Checking Algorithms, Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger.

Jan 2023

Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) is key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can …

[Hen22P]

The probabilistic model checker Storm, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk.

Aug 2022

We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm has three major distinguishing features. It supports multiple input languages for Markov models, including the Jani and Prism modeling languages, dynamic fault trees, generalized stochastic Petri nets, and the …

[Jan22P]

Parameter Synthesis in Markov Models: A Gentle Survey, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen.

Jan 2022

This paper surveys the analysis of parametric Markov models whose transitions are labelled with functions over a finite set of parameters. These models are symbolic representations of uncountable many concrete probabilistic models, each obtained by instantiating the parameters. We consider various analysis problems for a given logical specification $$\varphi $$φ: do all parameter instantiations …

[Jun16U]

Uncovering Dynamic Fault Trees, Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Mariëlle Stoelinga.

Jun 2016

Fault tree analysis is a widespread industry standard for assessing system reliability. Standard (static) fault trees model the failure behaviour of systems in dependence of their component failures. To overcome their limited expressive power, common dependability patterns, such as spare management, functional dependencies, and sequencing are considered. A plethora of such dynamic fault trees …

[Kat16P]

The Probabilistic Model Checking Landscape, Joost-Pieter Katoen.

Jul 2016

Randomization is a key element in sequential and distributed computing. Reasoning about randomized algorithms is highly non-trivial. In the 1980s, this initiated first proof methods, logics, and model-checking algorithms. The field of probabilistic verification has developed considerably since then. This paper surveys the algorithmic verification of probabilistic models, in particular …

[Vol18F]

Fast Dynamic Fault Tree Analysis by Model Checking Techniques, Matthias Volk, Sebastian Junges, Joost-Pieter Katoen.

Jan 2018

This paper presents a new state-space generation approach for dynamic fault trees (DFTs) that exploits several successful reduction techniques from the field of model checking. The key idea is to aggressively exploit the DFT structure-detecting symmetries, spurious nondeterminism, and don't cares. Benchmarks show a gain of more than two orders of magnitude in terms of state-space generation and …

[Bai03M]

Model-checking algorithms for continuous-time Markov chains, C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen.

Jun 2003

[Bat23P]

Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja.

Jan 2023

[Bud21C]

On Correctness, Precision, and Performance in Quantitative Verification, Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang.

2021

Quantitative verification tools compute probabilities, expected rewards, or steady-state values for formal models of stochastic and timed systems. Exact results often cannot be obtained efficiently, so most tools use floating-point arithmetic in iterative algorithms that approximate the quantity of interest. Correctness is thus defined by the desired precision and determines performance. In this …

[Ehl17F]

Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks, Rüdiger Ehlers.

2017

We present an approach for the verification of feed-forward neural networks in which all nodes have a piece-wise linear activation function. Such networks are often used in deep learning and have been shown to be hard to verify for modern satisfiability modulo theory (SMT) and integer linear programming (ILP) solvers.The starting point of our approach is the addition of a global linear …

[Faz20S]

Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming, Mahyar Fazlyab, Manfred Morari, George J. Pappas.

Dec 2020

Certifying the safety or robustness of neural networks against input uncertainties and adversarial attacks is an emerging challenge in the area of safe machine learning and control. To provide such a guarantee, one must be able to bound the output of neural networks when their input changes within a bounded set. In this paper, we propose a semidefinite programming (SDP) framework to address this …

[Gir22C]

CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness, Julien Girard-Satabin, Michele Alberti, François Bobot, Zakaria Chihani, Augustin Lemesle.

Jun 2022

We present CAISAR, an open-source platform under active development for the characterization of AI systems' robustness and safety. CAISAR provides a unified entry point for defining verification problems by using WhyML, the mature and expressive language of the Why3 verification platform. Moreover, CAISAR orchestrates and composes state-of-the-art machine learning verification tools which, …

[Har23P]

A Practitioner's Guide to MDP Model Checking Algorithms, Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger.

Jan 2023

[Hen22P]

The probabilistic model checker Storm, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk.

Aug 2022

[Jan22P]

Parameter Synthesis in Markov Models: A Gentle Survey, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen.

Jan 2022

[Jun16U]

Uncovering Dynamic Fault Trees, Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Mariëlle Stoelinga.

Jun 2016

[Kat19M]

The Marabou Framework for Verification and Analysis of Deep Neural Networks, Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L. Dill, Mykel J. Kochenderfer, Clark Barrett.

2019

Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network’s properties by transforming these queries into …

[Kat17R]

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks, Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, Mykel J. Kochenderfer.

2017

[Mor21H]

Hybrid Probabilistic Inference with Logical and Algebraic Constraints: a Survey, Paolo Morettin, Pedro Zuidberg Dos Martires, Samuel Kolb, Andrea Passerini.

Aug 2021

Real world decision making problems often involve both discrete and continuous variables and require a combination of probabilistic and deterministic knowledge. Stimulated by recent advances in automated reasoning technology, hybrid (discrete+continuous) probabilistic reasoning with constraints has emerged as a lively and fast growing research field. In this paper we provide a survey of existing …

[Mul22T]

The third international verification of neural networks competition (VNN-COMP 2022): Summary and results, Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, Taylor T. Johnson.

2022

[Vol18F]

Fast Dynamic Fault Tree Analysis by Model Checking Techniques, Matthias Volk, Sebastian Junges, Joost-Pieter Katoen.

Jan 2018

[Xia21B]

BarrierNet: A Safety-Guaranteed Layer for Neural Networks, Wei Xiao, Ramin Hasani, Xiao Li, Daniela Rus.

Nov 2021

This paper introduces differentiable higher-order control barrier functions (CBF) that are end-to-end trainable together with learning systems. CBFs are usually overly conservative, while guaranteeing safety. Here, we address their conservativeness by softening their definitions using environmental dependencies without loosing safety guarantees, and embed them into differentiable quadratic …

[Xie22N]

Neuro-Symbolic Verification of Deep Neural Networks, Xuan Xie, Kristian Kersting, Daniel Neider.

Jul 2022