Kevin Buzzard: Will Computers prove theorems? Will computers one day replace human mathematicians? Is this just around the corner, or decades away? Can neural networks spot patterns which humans have missed? Currently language models are great for brainstorming big ideas but are very poor when it comes to details. Can integrating a language model with a theorem prover like Lean solve these problems? Is the modern mathematical literature riddled with errors, and is it feasible to hope that a machine might find and even fix them? Is it possible to teach a computer the proof of Fermat's Last Theorem? And what do mathematicians make of all this? I'll talk about how modern developments in AI and theorem provers are beginning to affect mathematics.

Leo De Moura: Formalizing the Future: Lean’s Impact on Mathematics, Programming, and AI How can mathematicians, software developers, and AI systems work together with complete confidence in each other’s contributions? The open-source Lean proof assistant and programming language provides an answer, offering a rigorous framework where proofs and programs are machine-checkable, shared, and extended by a broad community of collaborators. By removing the traditional reliance on trust-based verification and manual oversight, Lean not only accelerates research and development but also redefines how we collaborate.

In this talk, I will highlight how Lean is being used to tackle challenging problems in mathematics, software verification, and AI research that depends on formally sound reasoning. I will also introduce the Lean Focused Research Organization (FRO), a non-profit dedicated to expanding Lean’s capabilities and community. By showcasing real-world examples, ranging from advanced research projects to industry-driven applications, I illustrate how Lean empowers us to innovate in a more reliable, transparent, and truly collective manner.

Strachey Lecture: Privacy, Verification, Robustness: A Cryptographer's perspective on ML Cryptographic tools enable the safe use of technology platforms controlled by worst case computationally bounded adversaries.In this talk I will show how cryptographic paradigms and tools can be used to address trust issues in various phases of the machine learning pipeline. We will touch on approaches for achieving privacy, correctness, and robustness in presence of adversaries.

Strachey Lecture: From probabilistic bisimulation to representation learning via metrics - Professor Prakash Panangaden Bisimulation is a fundamental equivalence relation in process theory invented by Robin Milner and with an elegant fixed-point definition due to David Park. In this talk I will review the concept of bisimulation and then discuss its probabilistic analogue. This was extended to systems with continuous state spaces. Despite its origin in theoretical work, it has proved to be useful in fields like machine learning, especially reinforcement learning. Surprisingly, it turned out that one could prove a striking theorem: a theorem that pins down exactly what differences one can "see" in process behaviours when two systems are not bisimilar.

However, it is questionable whether a concept like equivalence is the right one for quantitative systems. If two systems are almost, but not quite, the same, bisimulation would just say that they are not equivalent. One would like to say in some way that they are "almost" the same. Metric analogues of bisimulation were developed to capture a notion of behavioral similarity rather than outright equivalence. These ideas have been adopted by the machine learning community and a bisimulation-style metric was developed for Markov decision processes. Recent work has shown that variants of these bisimulation metrics can be useful in representation learning. I will tell the tale of this arc of ideas in as accessible a way as possible.

The talk will emphasize the diversity of mathematical tools necessary for understanding blockchain protocols and their applications The talk will emphasize the diversity of mathematical tools necessary for understanding blockchain protocols and their applications (e.g., distributed computing, game theory, mechanism design, and continuous-time stochastic processes) and the immediate practical impact that mathematical work on this topic has had (e.g., Ethereum's EIP-1559 and LVR for automated market makers).

Professor Christel Baier delivers the Hillary Term 2024 Strachey Lecture Abstract: The classical stochastic shortest path (SSP) problems asks to find a policy for traversing a weighted stochastic graph until reaching a distinguished goal state that minimizes the expected accumulated weight. SSP problems have numerous applications in, e.g., operations research, artificial intelligence, robotics and verification of probabilistic systems. The underlying graph model is a finite-state Markov decision process (MDP) with integer weights for its state-action pairs. Prominent results are the existence of optimal memoryless deterministic policies together with linear programming techniques and value and policy iteration to compute such policies and their values. These results rely on the assumption that the minimum under all proper policies that reach the goal state almost surely exists. Early work on the SSP problems goes back to the 1960s-1990s and makes additional assumptions. Complete algorithms that only require the existence of proper policies combine these techniques with a pre-analysis of end components, an elegant graph-theoretic concept for MDPs that has been introduced by de Alfaro in the late 1990s. The talk will start with a summary of these results. The second part of the talk presents more recent results for variants of the classical SSP. The conditional and partial SSP drop the assumption that the goal state must be reached almost surely and ask to minimize the expected accumulated weight under the condition that the goal will be reached (conditional SSP) resp. assign value 0 to all paths that do not reach the goal state (partial SSP). Other variants take into account aspects of risk-awareness, e.g., by studying the conditional value-at-risk or the variance-penalized expected accumulated weight. While the classical SSP problem is solvable in polynomial time, such non-classical SSP problems are computationally much harder. For the general case, the decidability status of such non-classical SSP problems is unknown, but they have been shown to be at least as hard as the Skolem problem (and even as the positivity problem). However, for non-positive weights, the conditional, partial and variance-penalized SSP problem are solvable in exponential time with a PSPACE lower bounds for acyclic MDPs

Speaker bio:

Christel Baier is a full professor and head of the chair for Algebraic and Logic Foundations of Computer Science at the Faculty of Computer Science of the Technische Universität Dresden since 2006. Since 2022 she holds an honorary doctorate (Dr. rer. nat. h.c.) from RWTH Aachen. From the University of Mannheim she received her Diploma in Mathematics in 1990, her Ph.D. in Computer Science in 1994 and her Habilitation in 1999. She was an associate professor for Theoretical Computer Science at the University of Bonn from 1999 to 2006. She was member of the DFG (German Research Foundation) review board for computer science from 2012 to 2019, and is a member of the DFG senate commission on Research Training Groups since 2020. Since 2011 she is a member of Academia Europaea. Her research focuses on modeling, specification and verification of reactive systems, quantitative analysis of stochastic systems, probabilistic model checking, temporal and modal logics and automata theory.

In this term's Strachey lecture, Professor Monika Henzinger gives an introduction to differential privacy with an emphasis on differential private algorithms that can handle changing input data. Decisions are increasingly automated using rules that were learnt from personal data. Thus, it is important to guarantee that the privacy of the data is protected during the learning process. To formalize the notion of an algorithm that protects the privacy of its data, differential privacy was introduced. It is a rigorous mathematical definition to analyze the privacy properties of an algorithm – or the lack thereof. In this talk I will give an introduction to differential privacy with an emphasis on differential private algorithms that can handle changing input data.

Monika Henzinger is a professor of Computer Science at the Institute of Science and Technology Austria (ISTA). She holds a PhD in computer science from Princeton University (New Jersey, USA), and has been the head of research at Google and a professor of computer science at EPFL and the University of Vienna.

Monika Henzinger is an ACM and EATCS Fellow and a member of the Austrian Academy of Sciences and the German National Academy of Sciences Leopoldina. She has received several awards, including an honorary doctorate from TU Dortmund University, Two ERC Advanced Grant, the Leopoldina Carus Medal, and the Wittgensteinpreis, the highest science award of Austria.

The Strachey Lectures are generously supported by OxFORD Asset Management

It’s said that Henry Ford’s customers wanted “a faster horse”. If Henry Ford was selling us artificial intelligence today, what would the customer call for, “a smarter human”? That’s certainly the picture of machine intelligence we find in science fiction narratives, but the reality of what we’ve developed is far more mundane.

Car engines produce prodigious power from petrol. Machine intelligences deliver decisions derived from data. In both cases the scale of consumption enables a speed of operation that is far beyond the capabilities of their natural counterparts. Unfettered energy consumption has consequences in the form of climate change. Does unbridled data consumption also have consequences for us?

If we devolve decision making to machines, we depend on those machines to accommodate our needs. If we don’t understand how those machines operate, we lose control over our destiny. Much of the debate around AI makes the mistake of seeing machine intelligence as a reflection of our intelligence. In this talk we argue that to control the machine we need to understand the machine, but to understand the machine we first need to understand ourselves.

Neil Lawrence is the inaugural DeepMind Professor of Machine Learning at the University of Cambridge where he leads the University’s flagship mission on AI, AI@Cam. He has been working on machine learning models for over 20 years. He recently returned to academia after three years as Director of Machine Learning at Amazon. His main interest is the interaction of machine learning with the physical world. This interest was triggered by deploying machine learning in the African context, where ‘end-to-end’ solutions are normally required. This has inspired new research directions at the interface of machine learning and systems research, this work is funded by a Senior AI Fellowship from the Alan Turing Institute. He is interim chair of the advisory board of the UK’s Centre for Data Ethics and Innovation and a member of the UK’s AI Council. Neil is also visiting Professor at the University of Sheffield and the co-host of Talking Machines.

THE STRACHEY LECTURES ARE GENEROUSLY SUPPORTED BY OxFORD ASSET MANAGEMENT

An introduction to algorithmic aspects of symmetry and similarity, ranging from the fundamental complexity theoretic "Graph Isomorphism Problem" to applications in optimisation and machine learning Symmetry is a fundamental concept in mathematics, science and engineering, and beyond. Understanding symmetries is often crucial for understanding structures. In computer science, we are mainly interested in the symmetries of combinatorial structures. Computing the symmetries of such a structure is essentially the same as deciding whether two structures are the same ("isomorphic"). Algorithmically, this is a difficult task that has received a lot of attention since the early days of computing. It is a major open problem in theoretical computer science to determine the precise computational complexity of this "Graph Isomorphism Problem".

An overview of work on probabilistic soft logic (PSL), an SRL framework for large-scale collective, probabilistic reasoning in relational domains and a description of recent work which integrates neural and symbolic (NeSy) reasoning. Our ability to collect, manipulate, analyze, and act on vast amounts of data is having a profound impact on all aspects of society. Much of this data is heterogeneous in nature and interlinked in a myriad of complex ways. From information integration to scientific discovery to computational social science, we need machine learning methods that are able to exploit both the inherent uncertainty and the innate structure in a domain. Statistical relational learning (SRL) is a subfield that builds on principles from probability theory and statistics to address uncertainty while incorporating tools from knowledge representation and logic to represent structure. In this talk, I’ll overview our work on probabilistic soft logic (PSL), an SRL framework for large-scale collective, probabilistic reasoning in relational domains. I’ll also describe recent work which integrates neural and symbolic (NeSy) reasoning. I’ll close by highlighting emerging opportunities (and challenges!) in realizing the effectiveness of data and structure for knowledge discovery.

Bio:

Lise Getoor is a Distinguished Professor in the Computer Science & Engineering Department at UC Santa Cruz, where she holds the Jack Baskin Endowed Chair in Computer Engineering. She is founding Director of the UC Santa Cruz Data Science Research Center and is a Fellow of ACM, AAAI, and IEEE. Her research areas include machine learning and reasoning under uncertainty and she has extensive experience with machine learning and probabilistic modeling methods for graph and network data. She has over 250 publications including 13 best paper awards. She has served as an elected board member of the International Machine Learning Society, on the Computing Research Association (CRA) Board, as Machine Learning Journal Action Editor, Associate Editor for the ACM Transactions of Knowledge Discovery from Data, JAIR Associate Editor, and on the AAAI Executive Council.. She is a Distinguished Alumna of the UC Santa Barbara Computer Science Department and received the UC Santa Cruz Women in Science & Engineering (WISE) award. She received her PhD from Stanford University in 2001, her MS from UC Berkeley, and her BS from UC Santa Barbara, and was a professor at the University of Maryland, College Park from 2001-2013.

THE STRACHEY LECTURES ARE GENEROUSLY SUPPORTED BY OxFORD ASSET MANAGEMENT