Institute seminar:

Streszczenie (autorskie):

Computing systems are becoming ever more complex, with automated decisions increasingly often based on deep learning components. A wide variety of applications are being developed, many of them safety-critical, such as self-driving cars and medical diagnosis. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning components. This lecture will describe progress with developing automated certification techniques for learnt software components to ensure safety and adversarial robustness of their decisions. I will discuss different dimensions of robustness, including bounded perturbations and causal interventions, as well as the role of uncertainty and explainability.

Streszczenie (autorskie):

Wyobraźmy sobie dwóch graczy w kasynie. Pierwszy z nich, notuje w zeszycie wyniki poprzednich losowań i na ich podstawie stara się przewidzieć kolejne. Drugi hazardzista, do swoich przewidywań dodatkowo używa monety, która służy mu jako "losowa porada". Przy założeniu, że mowa o uczciwym kasynie, obaj hazardziści powinni mieć taką samą szansę wygrania. Co jednak, jeśli wyniki losowań są z góry zdeterminowane i jedynie z każdą chwilą ujawniane hazardzistom? Czy możliwa jest sytuacja, w której pewien probabilistyczny hazardzista będzie lepszy od każdego deterministycznego? W trakcie referatu odpowiem na to pytanie twierdząco, w ramach pewnego konkretnego modelu z algorytmicznej losowości. Wynik został uzyskany wraz Laurentem Bienvenu i Valentino Delle Rose w ramach projektu OPUS realizowanego w IPI PAN.

Streszczenie (autorskie):

Formal verification of multi-agent systems is hard, both theoretically and in practice. In particular, studies that use a single verification technique typically show limited efficiency, and allow to verify only toy examples. Here, we propose some new techniques and combine them with several recently developed ones to see what progress can be achieved for a real-life scenario. Namely, we use fixpoint approximation, domination-based strategy search, partial order reduction, and parallelization to verify heterogeneous scalable models of the Selene e-voting protocol. The experimental results show that the combination allows to verify requirements for much more sophisticated models than previously.