Description

Cette thèse s’inscrit dans le contexte de l’intégration croissante des réseaux neuronaux dans des systèmes embarqués critiques pour la sécurité, notamment en avionique, dans les drones, l’automobile ou le spatial. Ces réseaux sont utilisés pour remplacer des tables de décision complexes (ex. ACAS-Xu), pour des tâches de perception comme l’atterrissage basé sur la vision (jeu de données LARD) ou pour la gestion de situations d’urgence (atterrissage autonome de drone). Ces applications imposent de fortes contraintes en matière de mémoire, de puissance de calcul et de latence, tout en exigeant un haut niveau de sûreté et de conformité aux normes de certification telles que DO-178C, DO-254 et ISO 26262.

Le déploiement de réseaux neuronaux dans ces contextes soulève trois défis majeurs : (1) les contraintes matérielles des plateformes embarquées (CPU, DSP, FPGA, ASIC), (2) la nécessité de garantir formellement l’absence de comportements dangereux, et (3) l’exigence de déterminisme et de prévisibilité pour la certification. Les approches actuelles de quantification – consistant à convertir des calculs en virgule flottante vers des représentations en virgule fixe plus efficaces – optimisent souvent les performances, mais négligent la vérification formelle et la maîtrise des temps d’exécution, créant un écart entre efficacité algorithmique et déploiement certifiable.

L’objectif principal de la thèse est de proposer une méthodologie de co-conception intégrant quantification, vérification formelle et implémentation embarquée prévisible pour des réseaux neuronaux critiques. Plus précisément, il s’agit de développer des méthodes de quantification « sensibles à la vérification », fondées sur l’analyse statique et garantissant formellement les bornes de sortie, afin de réduire mémoire et calcul tout en facilitant la preuve de sûreté. Ces réseaux quantifiés seront ensuite analysés à l’aide de techniques de vérification formelle (SMT, MILP, interprétation abstraite) pour démontrer le respect de propriétés de sécurité.

Parallèlement, la thèse visera un déploiement déterministe et certifiable sur différentes plateformes embarquées (CPU, DSP, FPGA), en exploitant le parallélisme, le pipelining et les ressources matérielles spécifiques afin de garantir des temps d’exécution bornés et reproductibles. L’ensemble sera validé expérimentalement sur plusieurs cas d’usage représentatifs (ACAS-Xu, atterrissage basé sur la vision, atterrissage d’urgence de drone), en évaluant mémoire, latence, consommation énergétique, sûreté et prévisibilité.

Les résultats attendus incluent de nouvelles méthodes de quantification compatibles avec la vérification formelle et la certification, des outils adaptés aux réseaux neuronaux quantifiés embarqués, ainsi que des démonstrations d’implémentations déterministes sur plateformes contraintes. La thèse ambitionne ainsi de fournir un cadre méthodologique généralisable à d’autres domaines critiques pour la sécurité, comme l’aéronautique, l’automobile et le spatial.

Compétences requises

étudiant en M2 ou école d'ingénieur. Connaissances dans plusieurs des sujets suivants : réseaux de neurones, vérification formelle, architecture informatique, arithmétique des ordinateurs

Bibliographie

[1] Dorra Ben Khalifa, Matthieu Martel. Efficient Implementation of Neural Networks Usual Layers on Fixed-Point Architectures. LCTES2024: 12-22
[2] Wang et al. (2023). Formal specification and SMT verification of quantized neural network for autonomous vehicles.
[3] Guérignon, C. (2021). Implementation of quantized neural networks on FPGA: methods and applications. PhD Thesis.
[4] Winandy, Dion, Manni, Garoche et al. (2025). Automated Fixed-Point Precision Optimization for FPGA Synthesis. IEEE Open Journal of Circuits and Systems, vol. 6.

Mots clés

réseaux de neurones, vérification formelle, quantification, systèmes embarqués