Speaker: Mark Chevallier
Title: You can survive the maze of death
Every turn you take in the maze of death might lead to fortune or disaster. And you don’t know which way to go! But we can prove, beyond any doubt, that by following some simple rules, you will be able to learn the absolute best way to navigate the maze. Want to know the rules? Better listen to the talk.
Speaker: Lauren DeLong
Title: Proactive Side Effect Prediction: Using AI to Race Against Time
Imagine going to the doctor to treat an eye infection, then ending up with itchy hives, or going for pain relief, but now your medicine causes stomach cramps! Such side effects can upset patients, dampen trust in doctors, and cost medical companies loads of money. To predict these side effects before they happen, we used network prediction methods, similar to those which generate friend recommendations for you on social media. Novel predictions can help to identify harmful side effects before a patient like you might experience them.
Speaker: Ramon Fernández-Mir
Title: Prove that your car won’t crash
In this talk, we explain how you can convince your computer (and yourself) that an autonomous system will behave safely.
Speaker: Jorge Gaete Villegas
Title: Explaining machine answers to human questions.
The field of artificial intelligence has accomplished much in recent years and its applications are everyday more embedded into our daily life. But can we really trust these systems and their predictions? Are we willing to put in the hands of a machine things like the healthcare of our loved ones? In this talk I explain our quest to provide a bridge between AI and decision makers via explanations.
Speaker: Zonglin Ji
Title: Human Action Recognition
Recognising human actions from a video has been considered a challenging task as it requires identifications of both spatial and temporal features to consider. In this project, I have built a classification model using deep learning that can distinguish and classify 100 plus different actions in daily life from a human skeleton-based dataset.
Speaker: Imogen Morris
Title: Euler the Mathemagician
Euler was infamous for using ‘impossible’ numbers that are smaller than any other number, yet bigger than zero, and using his almost magical intuition to arrive at the right answer, like a magician pulling a rabbit out of a hat. Using a proof-assistant, and a modern theory of infinitely-small numbers, I aim to show the real magic was in Euler’s reasoning.
Speaker: Jake Palmer
Title: Trusting the Transfer: From Scotland to the Antipodes
Single Transferable Vote (STV) is a family of algorithms for counting ranked ballots in multi-winner elections, typically carried out by hand. We verify using a general characterisation of STV that, regardless of the existing or not-yet-existing variant used, it is correct and terminates. This extends to covering Meek’s method of STV — a computer-counting variant that relies on the convergence of a vector under iteration of a specific function — used in several places including some elections in New Zealand.
Speaker: Adarsh Prabhakaran
Title: The silent epidemic: Role of networks in tobacco control.
Smoking behaviour can spread in a population through social ties. We are trying to model the spread of smoking and develop strategies to control the spread using an Agent-based model on a network.
Speaker: Richard Schmoetten
Title: Foundations for Physics
The physical theories describing the subatomic world have been experimentally verified to famously high degrees of accuracy. Yet conceptual problems remain: in fact, it is doubtful that the standard formulation of these theories is entirely well-defined. I aim to study one candidate remedy to these troubles, the Haag-Kastler axioms, and investigate well-founded models of reality with the help of a proof assistant.
Speaker: Filip Smola
Title: Flowing Resources
Resources are important to the activities we all do. We can use them to talk about what we are working with or what we are working towards. And then we can look at whole processes of activities and see how these resources flow through them. I am working to make a computer understand what we mean by these resources, so that together we can better understand the processes they control.
Speaker: James Vaughan
Title: Here be Dragons – Navigating Formal Mathematics with Knowledge Graphs
Unfortunately, the formal mathematics contained within interactive theorem provers is a world of its own. Although there is definite correspondence between these digitised theories and their pen-and-paper counterparts, it is not obvious to simple machines. Using knowledge graphs, we may bring back the human context to formal proofs for the benefit of both mathematicians and machines.