Apologies, we have not been keeping seminar advertisements up to date over the past year. A full list of the seminars which have occurred can be found on the LAIV Seminars page.
Recordings of at least some of the seminars are available on the AISEC Youtube channel.
Abstract: In the last decades the research in most of the fields in computer science, from programming paradigms to cyber-physical systems and from robotics to learning, has been challenged to integrate various concepts of continuous mathematics into semantics. This is because the interaction of computational systems with the real world brought real-valued parameters in computation (rates, probabilities, differential equations, time, resources, etc). And in this context, the classic semantics centred on concepts of congruence (bisimulation, behavioural equivalence) became inadequate. We are not interested anymore in understanding systems or their behaviours up to identity, but we need instead to work with approximations of systems and of their behaviours, which scale properly in the structure of a computational system and allow us to understand approximated computation.
To answer this challenge, we have introduced quantitative equational reasoning, an algebraic theory that generalizes universal algebras by extending the classic concept of equation of type s=t to equations of type s=e t for some positive e, interpreted as an upper bound of the distance between the terms s and t. In this way, instead of axiomatizing congruences, we axiomatize algebraic structures on metric spaces. This gives us the concepts we need to develop a metric semantics for systems where the similarity between non-equivalent systems can be properly measured and approximated.
This talk is a tutorial on quantitative equational reasoning and will summarize a series of results that we have published in the last five years, joint work with Prakash Panangaden and Gordon Plotkin.
https://personal.cis.strath.ac.uk/r.mardare/
Abstract: Verifying the robustness of neural networks is a hot topic in Machine Learning at the moment. As is often common in active areas of research, there has been a proliferation in the number of definitions of robustness out there. However as of yet, the consequences of the differences in these definitions do not seem to be widely discussed in the literature.
In this talk I will compare four different definitions of robustness, and in particular look at: their motivation, mathematical properties, assumptions about the underlying distribution of data, and interpretability. In particular we highlight that if not used with care, the popular definition of classification robustness may result in a contradictory specification! This work is the result of the collaboration of various members of LAIV.
Abstract:Despite the increasing prevalence of probabilistic, data-driven approaches to robotic control and other tasks, many practitioners still wish to rigorously test whether their system conforms to some concrete specification. This specification includes not just the explicit task that the robot is expected to complete (along with e.g., safety constraints), but also the range of environments that a user can reasonably expect the task to be achieved in. This talk addresses both parts of such specifications:
First, we will tackle environment specifications by introducing ProbRobScene – a probabilistic specification language for declaratively expressing (and sampling) 3D simulated environments. Second, we will tackle task specifications by combining data-driven imitation learning with Linear Temporal Logic. Finally I’ll discuss some recent work which ties these two threads together, with the goal of creating a holistic framework for automated testing of robot manipulation systems in simulation.
Abstract:In this talk I am going to discuss active learning algorithms for weighted automata. I will first recall Angluin’s seminal L* algorithm for learning deterministic finite automata. After that I will introduce a variant of the L* algorithm for weighted automata over semirings. Our main result is that this algorithm works when applied to weighted automata over a principal ideal domain. In addition, I will discuss an instructive example that shows that the algorithm is not guaranteed to terminate over arbitrary semirings. Joint work with Gerco van Heerdt, Jurriaan Rot and Alexandra Silva.