PhD positions on Formal Methods for the Safety of Artificial Intelligence

AI is now embedded into a number of everyday life applications. More and more, we depend on neural networks to make even critical situations, such as control and motion planning for autonomous cars, and it is of primary importance to be able to verify their correct behavior.

For some applications, e.g. perception in autonomous systems, through classifiers, we can only hope for probabilistic safety. Moreover, in real-world systems, precise models representative of the data are not always available. For instance, several probabilistic models may be plausible for describing of a problem, or a probabilistic model may be known but with uncertain parameters. Therefore, we need to consider both probabilistic information and epistemic uncertainty. Recently was introduced in [1] an approach based on imprecise probabilities or probability boxes, which generalize probabilistic and epistemic uncertainties by defining sets of probability distributions, for the quantitative verification of neural networks. This approach provides qualitative measures of how likely the outputs of a neural network are to exhibit a certain behavior, given some assumptions on the inputs specified as imprecise probabilities. Based on an abstraction and propagation of sets of probability distributions in neural networks, the probability of a property satisfaction can be bounded, and the regions of the input space the more likely to lead to property violation identified.

The approach of [1] proved to be both more general and more computationally efficient than the state of the art. However many challenges remain on the way to the applicability to real-world problems. As a starting point to the problem, the following extensions can be studied:

• the current abstraction of probability boxes relies on a constant stepsize staircase discretization which will hardly scale with the input dimension of the networks; we would like to investigate other abstractions;
• independence is currently assumed between the inputs of the network; we would like to handle also multivariate input distributions, for instance using copulas [4] as in e.g. [2].

A longer-term objective is to study the extension of the approach to the analysis of Bayesian neural networks, where the weights and bias of the network are also defined by multivariate (imprecise) probability distributions. This extends the case of multivariate input distributions, but in much higher dimension, probably requiring a fresh view on the approach. Finally, the project will investigate the application to one or both of the following:

• application to the safety of autonomous systems, such as robustness of perception and decision in the vision of drones with imprecise probabilistic information on trajectories;
• contribution to the fairness analysis and more generally the explanability of the network behavior [3].

[1] Eric Goubault and Sylvie Putot. A zonotopic Dempster-Shafer approach to the quantitative verification of neural networks. In Formal Methods: 26th International Symposium, FM 2024, Milan, Italy, September 9–13, 2024, Proceedings, Part I, page 324–342, Berlin, Heidelberg, 2024. Springer-Verlag.
[2] Ander Gray, Marcelo Forets, Christian Schilling, Scott Ferson, and Luis Benet. Verified propagation of imprecise probabilities in non-linear odes. International Journal of Approximate Reasoning, 164, 2024. Publisher Copyright: © 2023.
[3] Rabia Saleem, Bo Yuan, Fatih Kurugollu, Ashiq Anjum, and Lu Liu. Explaining deep neural networks: A survey on the global interpretation methods. Neurocomputing, 513:165–180, 2022.
[4] Bernhard Schmelzer. Random sets, copulas and related sets of probability measures. International Journal of Approximate Reasoning, 160:108952, 2023.