Level: M2

Contact: Serge Haddad

Context. With the development of machine learning and its daily applications, gaining confidence in the systems produced by such techniques has become a critical issue. A first problem consists in formalizing what is expected from the systems. Such requirements may be either generic or specific to the task to be achieved. For instance, adversarial robustness is a generic property [1]. It measures howmuch information is needed by an attacker to “falsify” the answer of a classifying system. On the other hand, assume the system proposes actions to be performed in the presence of an intruder, a specific property would be that there is no actionto be proposed when no intruder is detected.

In the internship, we will focus on neural networks since this is the most widely used and moreover it presents similar features to hybrid systems letting the possibility to adapt efficient techniques from this domain. Let us illustrate an example of specification formula:

{$ \forall \mathbf{x}, y \, \mathrm{Pre}(x) \wedge \mathrm{InOut}( x, y) \implies \mathrm{Post}(y )$}

where {$x$} (resp.{$y$}) is the input (resp. output) vector of the system, {$Pre$} is a precondition on the inputs and {$Post$} is a postcondition on the outputs. Thus checking the negation of a formula consists in solving some existential first-ordertheory [3].

The design of verification for neural networks is a challenging issue sincethe number of neurons generally is between few hundreds and millions (see [2]for a comparative study for piecewise linear neural networks). The techniquesare either sound and complete [6] or can proceed via astraction [5] thus rising the issue of incompleteness and how to tackle with it. There are now softwareframework dedicated to the verification of deep neural networks [4].

Goals. Thus the goals of this internship are twofold:

• Specifying a language or a logic that can express the main properties ex-pected to be satisfied by neural networks;
• Identifying specificities of formula related to these properties in order to de-sign new exact and/or approximate algorithms for verifying these properties.

References

1. Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A.V.,Criminisi, A.: Measuring neural net robustness with constraints. In: Lee,D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.)Advances in Neural Information Processing Systems 29: Annual Confer-ence on Neural Information Processing Systems 2016, December 5-10,2016, Barcelona, Spain. pp. 2613–2621 (2016),cc/paper/6339-measuring-neural-net-robustness-with-constraints
2. Bunel, R., Turkaslan, I., Torr, P.H.S., Kohli, P., Kumar, M.P.: Piecewise linearneural network verification: A comparative study. CoRRabs/1711.00455(2017),00455
3. Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: Anefficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kuncak,V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017,Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Com-puter Science, vol. 10426, pp. 97–117. Springer (2017). 1007/978-3-319-63387-9_5
4. Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P.,Thakoor, S., Wu, H., Zeljic, A., Dill, D.L., Kochenderfer, M.J., Barrett, C.W.:The marabou framework for verification and analysis of deep neural networks.In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st InternationalConference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Lecture Notes in Computer Science, vol. 11561, pp. 443–452. Springer(2019). 1007/978-3-030-25540-4_26
5. Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Dy, J.G., Krause, A. (eds.) Proceedingsof the 35th International Conference on Machine Learning, ICML 2018, Stockholm, Sweden, July 10-15, 2018. Proceedings of Machine Learn-ing Research, vol. 80, pp. 3575–3583. PMLR (2018),html
6. Tjeng, V., Tedrake, R.: Verifying neural networks with mixed integer programming. CoRRabs/1711.07356(2017),07356

Contact: Stefan Schwoon, Stefan Haar

Supervisory control of partially observable Petri nets has been studied int he literature mostly under a sequential and centralized perspective. With new application challenges from systems biology, it is time to to create a frameworkfor supervisory control of partially observable Petri nets, under the constraints of concurrency of the supervised processes (which are intrinsically non-sequential)and decentralization of observation and intervention.

The objectives targeted by the control must include reachability objectives in safe Petri nets; ideally, the results exceed this domain, to include reprogrammingof long-term behaviors of models arising in cell regulation. In this setting, thestakes are to steer the cell fate into a desired attractor or phenotype, whilestaying clear of fatal pathways (cancerous mutation, etc.)

The strengths of the well-known unfolding technique for safe Petri nets are expected to be instrumental in this work. The controller’s knowledge is a decentralized and asynchronous observation coming from a distributed set of observers. The tasks include:

• establish the semantics of supervisory control under these circumstances;
• determine an adequate game theoretic setting, and
• develop efficient techniques for synthezing controllers.

Contact: Stefan Schwoon, Stefan Haar

Supervisory control of partially observable Petri nets has been studied int he literature mostly under a sequential and centralized perspective. With new application challenges from systems biology, it is time to to create a frameworkfor supervisory control of partially observable Petri nets, under the constraints of concurrency of the supervised processes (which are intrinsically non-sequential)and decentralization of observation and intervention.

The objectives targeted by the control must include reachability objectives in safe Petri nets; ideally, the results exceed this domain, to include reprogrammingof long-term behaviors of models arising in cell regulation. In this setting, thestakes are to steer the cell fate into a desired attractor or phenotype, whilestaying clear of fatal pathways (cancerous mutation, etc.)

The strengths of the well-known unfolding technique for safe Petri nets are expected to be instrumental in this work. The controller’s knowledge is a decentralized and asynchronous observation coming from a distributed set of observers. The tasks include:

• establish the semantics of supervisory control under these circumstances;
• determine an adequate game theoretic setting, and
• develop efficient techniques for synthezing controllers.