We welcome applications for a PhD student position on extending applicability of formal verification for safety properties of Deep Reinforcement Learning based applications (DRL based applications).
Qualifications
- See the CUGS announcement for the main qualifications.
- Experience with independently identifying non-trivial goals, to plan the work and to conduct it.
- Interest and maturity in terms of Mathematical proofs, Logic and Probabilities are central to the project.
- Experience with software development of mid-to-large projects is important as the techniques generated by the project will result in developing/coding/modifying open source tools to showcase the results.
Observe that:
- Current state of the art can only handle "very small" neural networks. The project is about scaling up the size by coming up with new techniques to extend applicability of formal verification.
- Important: the project IS NOT about training and using DNN models. It is about verifying DNN models behave correctly in DRL Applications.
The PhD Thesis Project
Mission: The VeriDRL project will extend the applicability of ML centered formal verification techniques to scale to realistic Deep Reinforcement Learning (DRL) systems. For this, it will focus on small systems meant to run on embedded devices. It will develop new verification techniques and account for stochastic behaviors. The project will also investigate possibilities to synthesize correct DRL systems.
Motivation: Interest in control applications of reinforcement learning in general, and in those meant to run on small embedded devices in particular, is increasing. In such a system, the behavior of the environment might be known a priori or might need to be explored. A DRL solution will read the state of the system, perform an action according to the some policy, and obtain as a result a new state of the environment and a new reward. Given the central role of such policies and their direct impact on safety-critical systems (e.g., autonomous drones or insulin pumps), the verification problem of the resulting systems is particularly relevant.
Scientific challenge: Recent development in ML verification mainly focus on simple properties such as local robustness of classification for given inputs. Those targeting verification of DRL systems come with many challenges and opportunities for research:
- Scalability: Verification of DRL policies requires developing adapted and more scalable verification approaches for DNNs as they will target sequences of actions, not just the output to a single input.
- Stochastic behavior: controlled systems are often assumed to exhibit a stochastic behavior as capturing all details of their behavior is out-of-reach.
- Exploration: in fact a model for the controlled system might not even be available and one is left with samples of possible interactions. A question is then what guarantees can one enforce during exploration?
More information
This project will be supervised by Ahmed Rezine (main supervisor) and Soheil Samii (assistant supervisor). More information can be found here. Feel free to contact Ahmed for further information about the call.