- Full-time contract covered by NAWA grant PPN/PPO/2018/1/00029 , monthly salary around 5800 PLN for 3,5 years + many benefits (13th salary and open possibility of applying for the basic PhD scholarship sponsored by the department and other scholarships and grants (e.g. from Polish national science fund NCN) ).
- Interdisciplinary research on verification of cyber-physical systems controlled using neural networks + reliable AI + reinforcement learning. Full description below
- Publications on major CS conferences including CAV, ICML, IEEE CDC, NIPS verification workshop track.
- I encourage combining the PhD studies with internships in industry/international laboratories. I closely collaborate with worldwide renowned institutions (including UC San Diego, Stony Brook, Rutgers, TU Wien).

- passion for research,
- proficient in programming (C++/Python).

Please reach me with any questions, apply by sending CV to my gmail account.

Best, Jacek Cyranka

Question we address: How to show that an autonomous vehicle (e.g. self-driving car) never collides with an obstacle?

Motivation

*Cyber-Physical systems* denote various mechanizm that are controlled
or monitored by computer algorithms
The recent trend in CPS engineering autonomous *cyber-physical systems (CPS)*
is to deploy a *deep neural network (DNN)* as a CPS controller.
Some safety critical industrial applications include

- Self driving cars developed by most of the major car makers
- Autonomous space-ships, developed for example by NASA
- Robotic arms developed for medical surgeries

The main concern about CPS development is the safety.
Provably verifying safety properties of CPS is crucial for the engineering practice.
Errors in CPS can lead to disastrous consequences, prominent examples include the Ariane 5 rocket crash in 1996.
It is often crucial, especially when DNN controllers are in use, to
demonstrate that for example an autonomous mobile never collides with obstacles on some given race track,
or a spaceship reaches its destination and lands succesfully.
Widely available computational power makes this question answerable
using specialized computer algorithms.

Such algorithms are blending together modern techniques from several areas of
computer science and mathematics, including *interval arithmetic,
numerical analysis, differential equations and machine learning*.

Lagrangian reachability

In this context I have led research on a scalable algorithm for verification of safety
of DNN controlled CPS based on the concept of *Lagrangian Reachability* [1,2].
The current research is assuming that the mathematical model of CPS
is given as *differential equations*. Definition of arbitrary complicated
CPS, its controller, parameters and initial set are parsed from an input file.
To verify e.g. safety property of the provided input system, the solution set starting
at the provided initial state set must be bounded. Due to the model complexity and
nonlinearity the solutions are not in closed form. Hence, the algorithm (LRT) to be sound
must combine numerical methods and advanced algorithms. To guarantee conservativeness
all numerical computations are performed using interval arithmetic.

Currently international research team involving researchers including *UC San Diego, Texas Tech and
TU Wien* have been working on implementing scalable LRT algorithm in C++. Current efforts are
on verifying that a simple neural circuit inspired by C-Elegans worm trained using
reinforcement learning [3] is able to stabilize a cart-pole, perform parallel parking, and
some related control tasks.
One appealing design strategy for controllers is to use *deep neural networks (DNNs)*.
Safety properties of such controllers, however, remain largely unknown. I
remark that this research falls into the topic of *reliable/explainable AI*,
which is emerging as one of the most important problems in modern engineering.

Model free control based on

Reinforcement Learning

Our current algorithm, although being state of the art assumes that the model is given as
differential equations. Recent effort of engineering is however focused on *model-free*
techniques where optimal control is performed by utilizing data input only, e.g. sensor readings or
video camera input. Image input can be handled by using convolutional neural networks (CNNs).

As a future research, we will work on extending our techniques to the settings, where the exact model is not given / not known at all. It will require however establishing reliable reinforcement methods, e.g. policy gradient and safe AI in general. We will be utilizing major machine learning packages, and implement in Python.

__References:__

[1] Jacek Cyranka, Md. Ariful Islam, Greg Byrne, Paul Jones, Scott A. Smolka, Radu Grosu, *Lagrangian Reachability*, CAV 2017

[2] Jacek Cyranka, Md. Ariful Islam, Scott A. Smolka, Sicun Gao, Radu Grosu, *Tight Continuous-Time Reachtubes for Lagrangian Reachability*, IEEE CDC 2018

[3] Mathias Lechner, Radu Grosu, Ramin M. Hasani, *Worm-level Control through Search-based Reinforcement Learning*, NIPS 2017

- CAV
- ICML
- NeurIPS (verification workshop track)
- IEEE CDC

__Collaborators include:__

- Radu Grosu (TU Wien)
- Arif Islam (Texas Tech)
- Scott Smolka (Stony Brook)
- Sicun Gao (UCSD)