Wednesday 19 February 2020
Wednesday 12 February 2020
Wednesday 5 February 2020
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.
23 October: The potential for harm in the convergence of gambling and video games
David Zendle (CS, UoY)
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
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
9 October: Solving (Too) Hard Problems with SAT Solvers
Matti Järvisalo, University of Helsinki
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)
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.