Thèse Modélisation Compositionnelle et Vérification d'Archétypes de Réseaux Neuronaux Impulsionnels H/F - Doctorat.Gouv.Fr

Établissement : Université Côte d'Azur École doctorale : STIC - Sciences et Technologies de l'Information et de la Communication Laboratoire de recherche : I3S - Informatique, Signaux et Systèmes de Sophia-Antipolis Direction de la thèse : Elisabetta DE MARIA ORCID 0000000171169629 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-05-03T23:59:59 Les réseaux de neurones impulsionnels (SNN) constituent un cadre biologiquement plausible pour modéliser le calcul neuronal, où l'information est encodée par le timing précis d'impulsions discrètes plutôt que par des signaux continus. Si les simulations à grande échelle sont aujourd'hui courantes, elles ne fournissent généralement aucune garantie formelle sur le comportement des systèmes. À l'inverse, les méthodes formelles permettent d'analyser rigoureusement de petits systèmes, mais leur passage à l'échelle demeure un défi fondamental. Cette limite motive le développement d'approches compositionnelles reliant dynamiques locales et propriétés globales.

Les archétypes neuronaux offrent une base prometteuse. Il s'agit de petits réseaux à topologie fixée et dynamique biologiquement pertinente. Malgré des travaux existants sur leur vérification formelle et des schémas de composition préliminaires, une théorie générale et scalable de leur composition fait défaut. En particulier, il n'existe pas de cadre permettant de dériver systématiquement le comportement global à partir des composants.

Cette thèse vise à développer un tel cadre, basé sur le modèle Leaky Integrate-and-Fire (LI&F). L'objectif est d'étudier l'émergence de comportements complexes à partir d'un ensemble fini d'archétypes, et de formaliser ce processus via des règles de composition. Ces règles devront permettre de prédire ou contraindre les propriétés globales à partir des propriétés locales.

La vérification formelle sera au coeur de la méthodologie. Les archétypes et leurs compositions seront modélisés dans NuSMV, avec des propriétés exprimées en logique temporelle et vérifiées par model checking. Les propriétés étudiées incluront la réactivité, la synchronisation, la stabilité et les temps de réponse bornés. Un enjeu majeur sera d'assurer la tractabilité et le passage à l'échelle.

Le travail se déroulera en plusieurs phases : état de l'art, formalisation des archétypes dans le cadre LI&F, définition des opérateurs de composition, implémentation et vérification, puis évaluation sur des cas d'étude.

Collaboration avec de chercheurs de l'institut Neuromod

Collaboration with researchers from the Neuromod Institut

Le candidat doit être titulaire d'un Master (M2) ou d'un diplôme équivalent au moment du recrutement. Il doit avoir des connaissances en méthodes formelles et en algorithmique.