Accessibility statement

2019/20 seminar archive

On hyper-bent Boolean functions

Wednesday 19 February 2020

This talk will give a complete survey on hyper-bent Boolean functions and present very recent results.

Interactions among Cryptography, Quantum Computation, Artificial Intelligence and Applied Algebra

Wednesday 12 February 2020

Delaram Kahrobaei presents her research on Cryptography, Quantum Computation, Artificial Intelligence and Applied Algebra.

Formal Methods in UTRC

Wednesday 5 February 2020

Georgios Giantamidis presents his research on formal methods workflows.

Autumn 2019

4 December: Automated Modelling for Discrete Optimisation Problems
Peter Nightingale (CS, UoY)

Abstract: 
In the last 20 years, remarkable progress has been made on general-purpose solvers for discrete satisfaction and optimisation problems. Solvers for propositional satisfiability (SAT) have become much stronger, and progress has also been made on constraint programming (CP) and integer linear programming. Modern off-the-shelf solvers can now solve surprisingly large and difficult instances of NP-complete problems. However, the way in which a problem is modelled (represented) for the solver is critical. I will give an overview of an automated modelling pipeline that is able to refine an abstract specification down to a concrete model tailored for a SAT or CP solver. I will give some examples where reformulation of a model during refinement has a substantial effect on the performance of the target solver.


13 November 2019: CONNER: A Concurrent Learner in Description Logic
Dimitar
 Kazakov and Eyad Algahtani (CS, UoY)
Recording: [link]

Abstract: 
The class of ML known as Inductive Logic Programming (ILP) draws on the expressivity and rigour of subsets of First Order Logic to represent both data and models. When Description Logics (DL) are used, the approach can be applied directly to knowledge represented as ontologies. ILP output is a prime candidate for explainable artificial intelligence; the expense being computational complexity. We have recently demonstrated how a critical component of ILP learners in DL, namely, cover set testing, can be sped up through the use of concurrent processing on a GPU. Here we describe the first prototype of an ILP learner in DL that benefits from this use of concurrency. The result is a fast, scalable tool that can be applied directly to large ontologies. An example from the Chemistry domain will also be used to demonstrate how ILP can be combined with unsupervised learning into a hybrid approach capable of learning relational knowledge from unlabelled data.

23 October: The potential for harm in the convergence of gambling and video games
David Zendle (CS, UoY)
Recording: [link]

Abstract: There is significant concern amongst both academics, policymakers, and regulators that a blurring of lines between video games and gambling activities may lead to harm amongst gamers. These concerns have thus far largely revolved around loot boxes: Gambling-like transactions in video games that have been linked to both problem gambling and disordered gaming. However, a variety of other gambling-like and gambling-related practices have recently emerged in video games. These range from betting on esports, to playing social casino games, to more obscure practices like token wagering and real-money video gaming.In this talk, we will outline some of the diverse ways that video games and gambling are intersecting, before moving on to discuss how our research attempts to answer key questions when it comes to both prevalence of these activities, and their potential for harm.


16 October: Seeing is Believing? Media Integrity in a Post-Truth World
Nasir Memon, NYU
Recording: [link]

Abstract: The emergence of “fake news” along with sophisticated techniques using machine learning to create realistic looking media such as DeepFakes, has led to a renewed interest in digital media forensics. In this talk, Professor Nasir Memon will broadly discuss how media is generated and manipulations have been traditionally detected. He will then look at new approaches using machine learning for creating media that are leading us to a world where images and video cannot be believed any more as they can evade traditional detection techniques. Professor Memon will end by discussing approaches that are being developed to return integrity and trust in digital media.

Bio: Nasir Memon is Vice Dean for Academics and Student Affairs and a Professor of Computer Science and Engineering at the New York University Tandon School of Engineering. He is an affiliate faculty at the Computer Science department in NYU's Courant Institute of Mathematical Sciences, and department head of NYU Tandon Online. He introduced cyber security studies to NYU Tandon in 1999, making it one of the first schools to implement the program at the undergraduate level. He is a co-founder of NYU's Center for Cyber Security (CCS) at New York as well as NYU Abu Dhabi. He is the founder of the OSIRIS Lab, CSAW, The Bridge to Tandon Program as well as the Cyber Fellows program at NYU. He has received several best paper awards and awards for excellence in teaching. He has been on the editorial boards of several journals, and was the Editor-In-Chief of the IEEE Transactions on Information Security and Forensics. He is an IEEE Fellow and an SPIE Fellow for his contributions to image compression and media security and forensics. His research interests include digital forensics, biometrics, data compression, network security and security and human behavior.


16 October: Dictionary Attacks on Biometric Systems
Nasir Memon, NYU
Recording: [link]

Abstract: Contrary to the prevailing belief, we show that user authentication based on biometrics is vulnerable to dictionary attacks. We show the problem is particularly significant for partial prints used in smartphones and increasingly adopted for authentication tasks ranging from unlocking the devices screen up to payment authorization. We also show that speaker verification systems are also vulnerable to dictionary attacks. We then discuss ways to mitigate such attacks.

9 October: Solving (Too) Hard Problems with SAT Solvers
Matti Järvisalo, University of Helsinki
Recording: [link]

Abstract: In theory, the propositional satisfiability problem (SAT) is NP-complete and no non-brute-force algorithms for it are known. In practice, SAT is a success story of modern computer science. Today, practical implementations of complete decision procedures for SAT, i.e., SAT solvers, act as "practical NP-oracles" in best-performing practical algorithmic approaches to a wide range of hard problems. Furthermore, SAT solver can readily provide verifiable proofs when no solutions exist, which is important for various applications. In this talk, I aim to give an overview of modern SAT solving and (as time permits) to give an idea of how SAT solvers can be used incrementally for solving search and optimization problems with beyond-NP complexity.

Bio: Matti Järvisalo is Associate Professor at the Computer Science Dept, University of Helsinki where he leads the Constraint Reasoning and Optimization Group. He is one of the authors of "Clause Elimination for SAT and QSAT" which won the 2019 IJCAI-JAIR Best Paper Prize as an outstanding paper published in JAIR in the preceding five calendar years.


4 October: Fun with human-machine collaboration for computer vision
Vittorio Ferrari, Google Research Zurich
Recording: [link] (no soundtrack due to an AV fault)

Abstract: Training computer vision models typically requires tedious and time consuming manual annotation, which hinders scaling, especially for complex tasks such as full image segmentation. In this talk I will present recent human-machine collaboration techniques from my team, where the machine assists a human in annotating the training data and training a new model. These can substantially reduce human effort and also yield more interesting interfaces to interact with. The talk will explore several cases, including segmentation of individual objects, joint segmentation of all objects and background regions in an image, using speech together with mouse inputs, and annotating object classes using free-form text written by undirected annotators.
 
Biography: Vittorio Ferrari is a Senior Staff Research Scientist at Google Zurich, where he leads a research group on visual learning. He received his PhD from ETH Zurich in 2004, then was a post-doc at INRIA Grenoble (2006-2007) and at the University of Oxford (2007-2008). Between 2008 and 2012 he was an Assistant Professor at ETH Zurich, funded by a Swiss National  Science Foundation Professorship grant. In 2012-2018 he was faculty at the University of Edinburgh, where he became a Full Professor in 2016 (now he is a Honorary Professor).

Spring 2020

31 January: Symbolic Regression for Constructing Accurate Generalized Linear Models
Dr Jiří Kubalík (Czech Institute of Informatics, Robotics and Cybernetics, Czech Technical University in Prague, hosting: Dimitar Kazakov) 

Abstract: Reinforcement Learning (RL) algorithms can be used to optimally solve dynamic decision-making and control problems. With continuous-valued state and input variables, RL algorithms must rely on function approximators to represent the value function and policy mappings. Commonly used numerical approximators, such as neural networks or basis function expansions, have certain drawbacks: they are black-box models offering no insight in the mappings learnt, they require significant trial and error tuning of their meta-parameters and the results obtained with these methods suffer from the lack of reproducibility.

In this talk, we will see how symbolic regression (SR) can be used to construct smooth approximators for RL. We show how to construct state-space as well as input-output process models of unknown systems. Then, we demonstrate three off-line methods to automatically construct an analytic representation of the value function based on the state transition model. Sometimes, the training data may not provide sufficient guidance towards desired models, for instance, when the data set does not sufficiently cover the input space. Standard SR techniques then yield models that are partially incorrect, for instance, in terms of their steady-state characteristics or local behavior. We will introduce a novel SR algorithm, which allows for including prior knowledge in the model construction process and therefore it compensates for data insufficiencies.


22 January: Trusted Autonomous Systems: Verification Meets Falsification
Sergiy Bogomolov, Newcastle (hosting: Ana Cavalcanti)

Abstract: Cyber-physical systems (CPS) are networks of physical and digital components and present a next generation of large-scale highly-interconnected networked embedded systems. On the one hand, CPS open enormous opportunities as they form the core of emerging smart devices and services which are going to revolutionize many traditional industries such as automotive, traffic management, power generation and delivery, as well as manufacturing. On the other hand, highly autonomous systems pose special engineering challenges as any unexpected behaviour might lead to large financial losses or even human deaths.

In this talk, we address this challenge and propose automatic techniques to analyze CPS. For this purpose, we use the concept of hybrid automata which has proven to be particularly useful to model CPS.

Falsification algorithms for hybrid automata aim at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current
falsification algorithms still suffers from their high time complexity. In contrast to falsification, verification algorithms aim at providing guarantees that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision.

In this talk, we present an approach which leverages the power of symbolic reachability algorithms to improve the scalability of falsification techniques. Recent approaches to falsification reduce the problem to a nonlinear optimization problem. We propose to reduce the search space of the optimization problem by adding linear state constraints computed by a reachability algorithm. We showcase the efficiency of our approach on a number of standard hybrid systems benchmarks demonstrating the performance increase in speed and the number of falsifiable instances.

Bio: Sergiy Bogomolov is on the faculty of the School of Computing at the Newcastle University. He is broadly interested in algorithms and techniques to support design and development workflow of trustworthy and resilient autonomous systems. For this purpose, he uses and develops techniques on the interface of hybrid automata verification and AI planning. His Ph.D. and M.Sc. degrees are from the University of Freiburg, Germany.