Description du sujet de thèse

Autonomous systems perceive the external environment via sensors such as cameras and lidars and use machine learning algorithms (e.g., neural networks) to recognize patterns and objects. Since autonomous systems have wide applications in safety-critical domains where unexpected system's behaviors are critical, a key question is how we can trust perception-based system to behave as expected.

However, expressing formal requirements for systems based on perception is challenging as the input of the ML component is rich and unstructured (e.g., a sequence of images).

This thesis will:
- explore the problem of specifying formal requirements for perception-based system using temporal logics and filling the gap between raw features and "semantic" specifications.
- investigate automated reasoning algorithms (e.g., based on model checking) for automatically validating the requirements
- investigate automated reasoning algorithms for verify semantic-based specifications on neural networks.

A full description of the thesis is available on http://sergiomover.eu/saif_phd.pdf.

Contexte de travail

LIX (Laboratoire d'Informatique de l'Ecole Polytechnique) is a joint research unit with two supervisory institutions, École Polytechnique, a member of the Institut Polytechnique de Paris (cluster of universities composed of Ecole Polytechnique, Télécom Paris, ENSTA Paris, Télécom Sud Paris, ENSAE), and the Centre National de la Recherche Scientifique (CNRS), and one partner, Inria Saclay, with shared buildings and mixed teams.

LIX is organized in four poles: “Computer Mathematics”, “Data Analytics and Machine Learning”, “Efficient and Secure Communications”, “Modeling, Simulation and Learning” and “Proofs and Algorithms”.

The Ph.D. student will be part of the Cosynus team in the “Proofs and Algorithms” pole. The members of the Cosynus team work on the semantics and static analysis of software systems, sequential, concurrent or distributed, and hybrid/control systems and cyber-physical systems.

The Ph.D. student will benefit from the exciting environment of LIX, specifically the Computer Science Department of Ecole Polytechnique (DIX), in which he or she will be able to give courses, and the Department of Computer Science, Data and Artificial Intelligence of Institut Polytechnique de Paris (IDIA). He or she will also interact with the project members of the SAIF project (Safe Artificial Intelligence through Formal Methods), of the French National Research Programme on Artificial Intelligence PEPR IA.

Le poste se situe dans un secteur relevant de la protection du potentiel scientifique et technique (PPST), et nécessite donc, conformément à la réglementation, que votre arrivée soit autorisée par l'autorité compétente du MESR.

Contraintes et risques

No specific restrictions or risks.