Explications Formelles dapos;Intelligence Artificielle

Description de l'offre : Læ candidat·e prendra part au développement de l’analyseur formel PyRAT, développé au sein du laboratoire. Cet analyseur à l’état de l’art de la vérification formelle de réseaux de neurones est le siège d’autant de thématiques de recherches que d’applications industrielles pour le laboratoire. À ce titre, læ candidat·e évoluera à la frontière entre les mondes de la recherche scientifique et du développement logiciel industriel. Les missions de læ candidat·e sont les suivantes : · Étude active et restitution de l’état de l’art de la vérification formelle de logicielle, en particulier celle portant sur les programmes d’Intelligence Artificielle, et les explications de programmes d’Intelligence Artificielle. · Participation aux discussions et décisions scientifiques et techniques sur les améliorations à apporter dans l’analyseur PyRAT. Implémentation de ces améliorations. · Développement du lien entre la thématique de vérification formelle et celle d’explicabilité formelle. Application et amélioration de PyRAT pour l’explicabilité formelle. · Participation aux divers projets académiques, européens ou industriels autour de PyRAT et de l’explicabilité formelle et application aux cas d’usages étudiés. · Rédaction de rapports techniques et/ou de publications scientifiques portant sur l’analyseur formel PyRAT. · Support au développement de l’analyseur formel PyRAT, notamment par la rédaction de documentation, tutoriels, organisation de sessions de développement communes, relecture de contributions extérieures. · Participation à des congrès (nationaux et internationaux) pour disséminer les travaux sur l’analyseur PyRAT et l’explicabilité formelle.

Profil du candidat : Doctorat en informatique