Vérification de Propriétés Probabilistes Pour

**Vérification de propriétés probabilistes pour l'Intelligence Artificielle // Verification of probabilistic properties for Artificial Intelligence**:

- Réf **ABG-126167**
**ADUM-59248**
- Sujet de Thèse- 08/10/2024- Autre financement public- École polytechnique- Lieu de travail- Palaiseau Cedex - France- Intitulé du sujet- Vérification de propriétés probabilistes pour l'Intelligence Artificielle // Verification of probabilistic properties for Artificial Intelligence- Mots clés- méthodes formelles, intelligence artificielle, probabilités imprécises, réseaux bayésiens
formal methods, artificial intelligence, imprecise probabilities, Bayesian networks**Description du sujet**:
Objectifs : L'approche de [1] s'est avérée à la fois plus générale et plus efficace en termes de calcul que l'état de l'art. Cependant, de nombreux défis restent à relever quant à l'applicabilité aux problèmes du monde réel.
Comme point de départ, nous considérerons les extensions suivantes:

- l'abstraction actuelle des boîtes de probabilité repose sur une discrétisation en escalier à pas constant qui s'adaptera difficilement à la dimension d'entrée des réseaux ; nous aimerions explorer d'autres abstractions ;
- l'indépendance est actuellement supposée entre les entrées du réseau ; nous prévoyons de gérer également des distributions d'entrée multivariées, par exemple en utilisant des copules [4] comme par ex. [2].

Un objectif à plus long terme est d'étudier l'extension de l'approche à l'analyse des réseaux de neurones bayésiens, où les poids et les biais du réseau sont également définis par des distributions de probabilité multivariées (imprécises). Cela étend le cas des distributions d'entrées multivariées, mais dans une dimension beaucoup plus élevée, nécessitant probablement une nouvelle vision de l'approche.
- contribution à l'analyse d'équité ou plus généralement à l'explicabilité du comportement du réseau [3].

Références
[1] Eric Goubault and Sylvie Putot. A zonotopic dempster-shafer approach to the quantitative verification of neural networks. In Proceedings of FM 2024, Milan, Italy, 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.
[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.

Artificial Intelligence is now embedded into a number of everyday life appli
- cations. More and more, we depend on neural networks even in 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.
- faction can be bounded, and the regions of the input space the more likely to lead to property violation identified.
Objectives: 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, we will consider the following extensions:

- 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 plan 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) probabil
- ity distributions. This extends the case of multivariate input distributions, but in much higher dimension, probably requiring a fresh view on the approach.
- contribution to the fairness analysis or more generally the explanability of the network behavior [3].

References
[1] Eric Goubault and Sylvie Putot. A zonotopic dempster-shafer approach to the quantitative verification of neural networks. In Proceedings of FM 2024, Milan, Italy, 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.
[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, copula