Research Seminars 2018

Time Series Graphical Modelling via Partial Coherence and Lessons from EEG Analysis

We consider time series methodology for building a representative brain connectivity graph from a group of individuals with the same medical diagnosis (positive syndrome schizophrenia). Our approach to time series graphical modelling utilises partial coherence between pairs of series: it being zero for all frequencies corresponds to a missing edge in the graph. If partial coherence methodology is to be successfully used on EEG data then careful consideration must be given to practical issues such as mixed spectra and poorly condition spectral matrices. The treatment of spectral lines is discussed. Dealing with poor conditioning via spectral matrix shrinkage reveals very different influences on partial coherence estimates may result, depending on the loss function chosen. We use a test statistic to test for edge inclusion which is formed as an integrated functional of the estimated spectral matrix. This avoids the necessity of multiple testing over frequencies. Moreover, since its asymptotic distribution is known, p-values can be associated to the particular graph edge for all individuals in the group, allowing us to find the proportion of individuals whose associated statistic rejects the hypothesis of no edge. Using this information, a group-specific connectivity graph may be constructed.

A Personal Perspective on SAT and CSP: Tractability, Complexity, Quantification, Proofs

I will give a guided, personal tour of some theoretical results on SAT, CSP, and their quantified versions. In particular, I will study the impact of the variable interactions on the complexity; here, the graph-theoretic measure of treewidth, and generalizations thereof, play a key role. In this context, I will also present results on the existence of proofs certifying unsatisfiability of problem instances. Parallels between the quantified and non-quantified cases will be highlighted, and open problems and directions will be offered. I will end with a general discussion of QBF proof systems and proof complexity.

Random resolution and approximate counting

Resolution is a propositional proof system that is bad at formalizing arguments involving counting, even approximately. I will discuss some upper and lower bounds on random resolution, which roughly speaking adds to resolution the ability to use any axiom, as long as it is true most of the time. This is partly motivated by a question about a related first-order proof system of bounded arithmetic with approximate counting.

The Minimum Circuit Size Problem: A Survey and Recent Results

In the Minimum Circuit Size Problem (MCSP), the input is the truth table of a Boolean function F, and a parameter s, and the output is YES iff F has circuits of size at most s. Intuitively speaking, MCSP is a problem that asks about the compressibility of strings. MCSP is a fundamental problem that has been studied since the 1950s, and yet remains mysterious. It is easy to see that MCSP is in NP, but there is no strong evidence for MCSP being solvable in polynomial time or MCSP being NP-complete. While MCSP is hard to classify in complexity-theoretic terms, it has deep connections to many areas of computer science, including circuit complexity, learning theory, cryptography and proof theory. I will informally survey work on MCSP, and sketch some recent results. I will try to make the talk accessible to a broad audience.

The Social Side of Security: Requirements, Regulations, and Breaches

Cybersecurity underpins the lives of ordinary people---their safety, work, health, and entertainment. Yet despite its importance, cybersecurity is often approached in a reactive manner---taking corrective actions to "patch" vulnerabilities after they are detected or exploited. In modern ICT systems, secure and privacy-aware governance can only be achieved by bridging the divide between technical solutions such as access control and the human and social factors associated with the users of such systems. In this talk, I will first review the building blocks for developing computational models for the social side of security, namely normative models used for representation of and reasoning about security and privacy requirements and regulations. I will then describe how such models can be combined with other AI techniques to reason about security breaches, understand tradeoffs, and revise requirements. Finally, I will conclude with some of the open areas and future directions that I would like to pursue such as digital forensics.

A logic for reasoning about graphs

Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about the properties that a given graph may or may not satisfy. In particular, our work is motivated by model-driven software development and by graph data bases. With this aim, in this seminar I will present a visual logic that allow us to describe graph properties, including properties about paths, which has the expressive power of first-order logic, if we do not consider path properties. The logic is equipped with a deductive tableau method that we have proved to be sound and complete. Moreover, we have shown that this logic is an institution.

Research in Deep Learning

A major advance in AI occurred in 2012 when AlexNet won the ImageNat competition with a deep network. The success was sufficiently better than previous years that deep networks were applied in many applications with great success. However, there is little understanding of why deep learning works. This talk will illustrate current research directions in the area at a level for a general scientific audience.

Implementing a Universal Nondeterministic Turing Machine Using DNA

Big Data Yesterday, Today, and Tomorrow

The general idea of Big Data is hardly new, although it has existed under many names. Of course, it is a moving target, since what once was Big Data can now be done on a smartphone. In 2013, New York Times reporter Steve Lohr published “The Origins of ‘Big Data’: An Etymological Detective Story,” attributing that phrase to John Mashey, who started using it in the early 1990s and made it a marketing theme at Silicon Graphics. In this talk John will explore the past of Big Data, describe its present state, and speculate on the future. The first and largest part of the talk reviews the long history of Big Data, starting with Hollerith machines and punch cards, the Big Data of the 1890s. Insights for the future can be gained by studying the evolution since then of hardware, software and applications, as well as never-ending, but always-changing “stack wars.” The second part examines key elements of current Big Data applications and relates them to their historical precursors.
Finally, the third part discusses challenges of the near-term future, then ends 5,000 years from now, quoting an apt science-fiction book.

Babbage and the abstraction of mechanism

Charles Babbage has been called the 'great-uncle' of modern computing, a claim that rests simultaneously on his demonstrable understanding of most of the architectural principles underlying the modern computer, and the almost universal ignorance of Babbage's work before 1970. There has since been an explosion of interest both in Babbage's devices and the impact they might have had in some parallel history, and in Babbage himself as a man of great originality who had essentially no influence at all on subsequent technological development.

In all this, one fundamental question has been largely ignored: how is it that one individual working alone could have synthesised a workable computer design over a short period, designing an object whose complexity of behaviour so far exceeded that of contemporary machines that it would not be matched for over one hundred years?

The key, as is well understood in modern engineering contexts, is to abstract away from the full complexity of a concrete system. The complexity barrier was faced by the electronics industry in the 1970's and 1980's, and triggered a switch from visual descriptions of large scale digital electronic devices to text-based Hardware Description Languages similar in style to that of a software programming language.
Babbage too faced an overwhelming complexity barrier, and his response was indeed to design a system of hardware abstractions which he called his Notation. The ideas allowed him to reason in the abstract about chains of cause and effect in his mechanisms, and he believed the Notation to be his crowning achievement.

His ideas were not taken up: one near contemporary rejected it because there could be many concrete machines that had the same notational description, which of course was precisely the point.
In this talk I will draw parallels between early electronic HDL's and Babbage's notation; display some strengths and weaknesses of Babbage's approach; and speculate on the underlying cause of the 150 year gap between Babbage's notation and the emergence of HDL based engineering design as a standard technique.

On the reachability problem in low-dimensional polynomial maps

In this talk, I will introduce nondeterministic polynomial maps and related reachability problems. Polynomial maps can be seen as generalization of Vector Addition Systems, where the register updates are not restricted to incrementing and decrementing the current value but can be defined by arbitrary polynomials. In the reachability problem for polynomial maps we are asked whether there exists a finite composition of polynomials such that the given initial register value is evaluated to zero.

We consider different parameters in polynomial maps and study their effect on the decidability status of the reachability problem. In particular, we will show that the reachability problem is undecidable for three-dimensional affine maps and is PSPACE-complete for one-dimensional polynomial maps. We also investigate the role of VAS-like updates of the form x=x+a for some integer a. Surprisingly, we see that if we exclude the updates of this form, the problem becomes decidable in any dimension.

Uncovering Colossus

In the early 1970s I began a study of the work of Charles Babbage’s earliest successors – having stumbled on the work of the Irish pioneer Percy Ludgate – and began to plan an overall historical account of the origins of the digital computers. I investigated the late Alan Turing's work, and learnt about a highly secret programmable electronic computer that had been developed in Britain during World War II. I revealed that this computer was named Colossus, and had been built in 1943 for Bletchley Park, the UK Government’s code-breaking establishment. I attempted unsuccessfully to get this machine declassified. However in 1974 and 1975, two books ('The Ultra Secret' and 'Bodyguard of Lies') were published about Bletchley Park's war-time work on breaking German messages that had been encrypted using Enigma. These books caused a great sensation, and provided me with an excuse to try again to get the Colossus Project declassified. This led to my receiving official permission to undertake a detailed investigation of the project. As a result I was permitted to reveal for the first time, at the 1976 Los Alamos Conference on the History of Computing, the work led by T. H. (Tommy) Flowers at the Post Office Dollis Hill Research Station on the construction of a series of special-purpose electronic computers for Bletchley Park, machines which all predated ENIAC, an American machine which had until then been regarded as the world's first electronic computer.

Resolution and the binary encoding of combinatorial principles

We investigate the size of refutations in Res(k), an extension of Resolution working on k-DNFs instead of clauses, for certain contradictions given in the less usual binary encoding. In particular, we prove lower bounds for binary k-Clique principle as well as for the Weak Pigeon-Hole Principle. Previously, a resolution lower bound was known for the former while the later was considered in the more usual unary encoding only. This is based on a joint work with Nicola Galesi (La Sapienza, Roma) and Barnaby Martin (Durham). The first half of the talk will be a kind of general introduction to Propositional Proof Complexity, and thus accessible to everyone.

Structural biology and drug discovery: Fighting the emergence of resistance in cancer and mycobacterial infections

The emergence of drug resistance is a challenge that is facing drug discovery in both cancer and infectious disease. Next generation sequencing has shown that mechanisms of resistance to the same drug in different tumours or pathogens can vary extensively. The challenge will be one in personalised or precision medicine. One approach is to exploit state-of-the-art methods to bring new drugs for different targets to the market, but this will be difficult to finance if patient populations are small. Structure-guided fragment-based screening techniques have proved effective in lead discovery - Astex, the company I cofounded, has a breast cancer on the market and eight in clinical trials. The method is effective not only for classical enzyme targets but also for less “druggable” targets such as protein-protein interfaces. Our approach involves a fast initial screening using biophysical techniques of a library of around 1000 compounds, followed by a validation step involving more rigorous use of related methods to define three-dimensional structure, kinetics and thermodynamics of fragment binding. The use of high throughput approaches does not end there, as it becomes a rapid technique to guide the elaboration of the fragments into larger molecular weight lead compounds. I will discuss progress in using these approaches for targets in cancer (protein-protein interfaces) and in Mycobacterium Tuberculosis and Mycobacterium Abscessus infections.

I will also review our new computational approaches using both statistical potentials and machine learning methods for understanding mechanisms of resistance. These have demonstrated that resistance does not only arise from direct interference of the resistance mutation to drug binding but can also result allosteric mechanisms, often modifying target interactions with other proteins. These lead to new ideas about repurposing and redesigning drugs and even in reclassifying patients in clinical trials.