http://talks.cam.ac.uk/show/rss/5408

Mike Gordon’s Higher-Order Logic (HOL) is one of the most important logical foundations for interactive theorem proving. The standard semantics of HOL , due to Andrew Pitts, employs a downward closed universe of sets, and interprets HOL ’s Hilbert choice operator via a global choice function on the universe.

In this talk, I introduce a natural Henkin-style notion of general model corresponding to the standard models. By following the Henkin route of proving completeness, I discover an enrichment of HOL deduction that is sound and complete w.r.t. these general models. Variations of my proof also yield completeness results for weaker deduction systems located between standard and (fully) enriched HOL deduction, relative to less constrained models.

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

CANCELLED

• Speaker: Andrei Popescu (University of Sheffield)
• Thursday 22 May 2025, 17:00-18:00
• Venue: Online; live-streamed at MR14 Centre for Mathematical Sciences.
• Series: Formalisation of mathematics with interactive theorem provers ; organiser: Anand Rao Tadipatri.

Add to your calendar or Include in your list

A classical result in differential geometry, ultimately leading to Frobenius theorem, states that the flows of two smooth vector fields X, Y commute for all times if and only if their Lie bracket [X,Y] vanishes. In this talk, we consider continuous, Sobolev vector fields with bounded divergence on the real plan, and we discuss an extension of the classical Frobenius theorem in the setting of Regular Lagrangian Flows. In particular, we improve the previous result of Colombo-Tione (2021), where the authors require the additional assumption of the weak Lie differentiability on one of the two flows. This is a joint project in collaboration with Martina Zizza.

• Speaker: Annalaura Rebucci, MPI Leipzig
• Monday 26 May 2025, 14:00-15:00
• Venue: MR13.
• Series: Partial Differential Equations seminar; organiser: Amelie Justine Loher.

Add to your calendar or Include in your list

Sign up on Eventbrite: https://medai_may2025.eventbrite.co.uk

Join us for the Cambridge AI in Medicine Seminar Series, hosted by the Cancer Research UK Cambridge Centre and the Department of Radiology at Addenbrooke’s. This series brings together leading experts to explore cutting-edge AI applications in healthcare—from disease diagnosis to drug discovery. It’s a unique opportunity for researchers, practitioners, and students to stay at the forefront of AI innovations and engage in discussions shaping the future of AI in healthcare.

This month’s seminar will be held on Wednesday 28 May 2025, 12-1pm at the Jeffrey Cheah Biomedical Centre (Main Lecture Theatre), University of Cambridge and streamed online via Zoom. A light lunch from Aromi will be served from 11:45. The event will feature the following talk:

AI for neuroimaging in dementia – Dr Timothy Rittman, Senior Clinical Research Associate, Department of Clinical Neurosciences, University of Cambridge

Timothy Rittman is an Alzheimer’s Research UK Senior Fellow, Senior Clinical Research Associate at the University of Cambridge and Honorary Consultant Neurologist at Addenbrookes Hospital. His research centres around neurodegenerative tauopathies, combining neuroimaging, cognitive assessments and neuropathology to understand how these diseases affect the whole brain. He also has an interest in translating methods from artificial intelligence and big data for use in memory clinics, and leads the Quantitative MRI in NHS Memory Clinics (QMIN-MC) study collecting real world data for validation of AI models. Tim co-leads the DEMON dementia network’s Imaging Working group and is an adviser to the World Young Leaders in Dementia. He is a consultant in the Addenbrookes Memory Clinic, and leads a clinic for people with Progressive Supranclear Palsy and Corticobasal Degeneration, in addition to co-leading a dementia genetics clinic.

Abstract: Novel biomarkers for early detection and prognosis in dementia are urgently needed, particularly with the advent of potentially disease modifying treatments. AI approaches to neuroimaging are promising, but require real world validation. This talk will cover the Quantitative MRI in NHS Memory Clinics (QMIN-MC) study, and how it is collecting real world data to bridge the gap between research and clinical application.

This is a hybrid event so you can also join via Zoom:

https://zoom.us/j/99050467573?pwd=UE5OdFdTSFdZeUtIcU1DbXpmdlNGZz09

Meeting ID: 990 5046 7573 and Passcode: 617729

We look forward to your participation! If you are interested in getting involved and presenting your work, please email Ines Machado at im549@cam.ac.uk

For more information about this seminar series, see: https://www.integratedcancermedicine.org/research/cambridge-medai-seminar-series/

• Speaker: Dr Timothy Rittman, Senior Clinical Research Associate, Department of Clinical Neurosciences, University of Cambridge
• Wednesday 28 May 2025, 11:45-13:00
• Venue: Jeffrey Cheah Biomedical Centre (Main Lecture Theatre), University of Cambridge.
• Series: Cambridge MedAI Seminar Series; organiser: Hannah Clayton.

Add to your calendar or Include in your list

The Hosts for this talk are Nicky Clayton and Max Knowles

The talk will look at evidence for felt experience (consciousness in a minimal sense) in a number of invertebrate animals. I’ll do this by going through a sequence of experiments (some well-known, some newer) on hermit crabs, octopuses, cuttlefish, bees, and fruit flies. I will emphasize interactions between different kinds of evidence, and the role of some fortuitous observations. A preprint by Hakwan Lau criticizing the whole enterprise will be discussed at the end.

• Speaker: Peter Godfrey Smith
• Friday 30 May 2025, 16:30-18:00
• Venue: Ground Floor Lecture Theatre, Department of Psychology.
• Series: Zangwill Club; organiser: Sara Seddon.

Add to your calendar or Include in your list

Abstract not available

• Speaker: Dr Huiqi Yang and Dr Nicola Thompson, Cambridge University Hopitals Trust
• Thursday 19 June 2025, 09:30-10:30
• Venue: Theo Chalmers Lecture Theatre (LT2) School of Clinical Medicine.
• Series: Cancer Research UK Cambridge Centre Lectures in Cancer Biology and Medicine; organiser: Justin Holt.

Add to your calendar or Include in your list

Sleep is essential for life. It serves a variety of purposes for ensuring brain health including memory consolidation, emotional processing and most importantly maintaining neural networks and synaptic plasticity. The newborn infant will spend over 16 hours asleep a day, the preterm infant even more. The nature, quality and quantity of sleep is very different to sleep at any other age, and sleep in the newborn is fundamental constructing networks in the brain and refining a picture of the outside world.

It is therefore important be able to investigate the relationship between functional connectivity and the sleep states in the developing brain, and how interrupted sleep could contribute to altered neurodevelopmental outcomes in vulnerable infants.

Our brains, however, do not develop in isolation; from the moment of birth the newborn infant will communicate with their primary caregiver. This interaction is fundamental in enabling the newborn infant to enter a secure internal state to interact and learn about the outside world. The earliest and universal form of caregiver-infant communication is affectionate touch.

This presentation will provide a rationale for studying sleep, functional connectivity and neural synchrony in the neonatal period and highlight two brain imaging technologies – diffuse optical tomography and dyadic electroencephalography – both of which have been used by our group to investigate dynamic functional connectivity in the newborn brain and neural synchrony between mother and infant during affectionate touch. As well as summarising work done so far, the presentation will summarise the potential (and challenges) of exploring sleep and touch in the preterm brain.

• Speaker: Professor Topun Austin, Consultant Neonatologist in Cambridge, and Honorary Professor of Neurophotonics at University College London
• Wednesday 28 May 2025, 11:30-12:30
• Venue: https://us02web.zoom.us/j/87076030035?pwd=XUpJuh8jiR0mae1AhkV79qbg8MtlSM.1.
• Series: ARClub Talks; organiser: Simon Braschi.

Add to your calendar or Include in your list

Abstract not available

• Speaker: Patrick Allen (McGill)
• Tuesday 17 June 2025, 13:00-14:00
• Venue: MR12.
• Series: Number Theory Seminar; organiser: Rong Zhou.

Add to your calendar or Include in your list

TBC

• Speaker: David Lilienfeldt (Leiden)
• Tuesday 10 June 2025, 13:00-14:00
• Venue: MR12.
• Series: Number Theory Seminar; organiser: Jef Laga.

Add to your calendar or Include in your list

TBC

• Speaker: Fred Diamond (KCL)
• Tuesday 03 June 2025, 13:00-14:00
• Venue: MR12.
• Series: Number Theory Seminar; organiser: Jef Laga.

Add to your calendar or Include in your list

I will introduce the All-atom Diffusion Transformer (ADiT), a unified generative modelling architecture capable of jointly modelling both periodic crystals and non-periodic molecular systems. ADiT is a latent diffusion model that embeds 3D atomic systems into a shared latent space, where it learns to sample new latents and map them to valid structures. ADiT achieves state-of-the-art performance for generative modelling across both molecules and materials, outperforming specialized system-specific methods while being significantly more scalable. I will show that scaling ADiT’s model parameters predictably improves performance, towards the goal of a unified foundation model for molecular design.

Link to paper: https://www.arxiv.org/abs/2503.03965

Bio: Chaitanya is a final year PhD student in Computer Science at the University of Cambridge, supervised by Prof. Pietro Liò. His research is about deep learning foundations for molecular modelling and design. He has previously interned at Prescient Design, Genentech and at FAIR Chemistry, Meta AI on the same.

In-person and virtual (link coming soon) - and will be recorded.

• Speaker: Chaitanya Joshi
• Tuesday 03 June 2025, 13:00-14:00
• Venue: Lecture Theatre 1, Computer Laboratory, William Gates Building.
• Series: Artificial Intelligence Research Group Talks (Computer Laboratory); organiser: Pietro Lio.

Add to your calendar or Include in your list

Accurate prediction of ground-state electronic energies is essential for understanding chemical reactivity, catalysis, and material properties. One of the most promising applications of quantum computers is the simulation of chemical systems. While imaginary time evolution (ITE) is widely used on classical hardware to obtain ground states, its implementation on quantum hardware is challenging due to its non-unitary nature.

Near-term approaches to this problem have relied on heuristics, compromising their accuracy. As we enter the early fault-tolerant era of quantum computing, there is growing interest in the development of more natively quantum algorithms. Since it is not possible to implement a non-unitary gate deterministically, we resort to probabilistic ITE (PITE) algorithms. These embed the ITE operator inside a larger unitary matrix, which is accessed via post-selection of “successful” mid-circuit measurements. In our previous work, we introduced a novel PITE algorithm that yields shorter circuits and is easier to implement than existing PITE approaches [1].

This talk will provide an introduction to quantum circuits, before focusing on the challenges associated with PITE algorithms. In particular, we will discuss the feasibility of implementing an Amplitude Amplification routine [2], as well as a new “boosting” procedure, which uses successive reflection operations to boost to lower energy states [3].

[1] C. Leadbeater, N. Fitzpatrick, D. M. Ramo, and A. J. W. Thom, Quantum Sci. Technol. 9, 045007 (2024). [2] H. Nishi, T. Kosugi, Y. Nishiya, and Y.-i. Matsushita, Phys. Rev. B 110 , 174302 (2024). [3] B. C. B. Symons, D. Manawadu, D. Galvin, and S. Mensa, Phys. Rev. Res. 6, L022041 (2024).

• Speaker: Chiara Leadbeater, University of Cambridge
• Wednesday 28 May 2025, 14:30-15:30
• Venue: Unilever Lecture Theatre, Yusuf Hamied Department of Chemistry.
• Series: Theory - Chemistry Research Interest Group; organiser: Lisa Masters.

Add to your calendar or Include in your list

Abstract not available

• Speaker: Dr Alex Epstein, University of Cambridge
• Wednesday 12 November 2025, 14:30-15:30
• Venue: Unilever Lecture Theatre, Yusuf Hamied Department of Chemistry.
• Series: Theory - Chemistry Research Interest Group; organiser: Lisa Masters.

Add to your calendar or Include in your list

Many people think of the New Testament as a set of Christian texts that provide information about the authors’ views on being Christian. There are problems with talking about “Christians” in connection with the New Testament, however. This talk will explore some of those problems, drawing on my research on the letters of the apostle Paul. It will discuss how reading through the lens of “Christians” can obscure the situation of women and enslaved persons in the ancient world. It will also explore how it may contribute to the phenomenon of accidental anti-Judaism among readers of the Bible today.

• Speaker: Dr Julia Snyder, Faculty of Divinity and Bye Fellow of Darwin College
• Tuesday 27 May 2025, 13:10-14:00
• Venue: Richard King room, Darwin College.
• Series: Darwin College Humanities and Social Sciences Seminars; organiser: Matthew Jones.

Add to your calendar or Include in your list

Abstract not available

• Speaker: Paul Hooper, Department of Mechanical Engineering, Imperial College
• Thursday 23 October 2025, 15:00-16:00
• Venue: Seminar Room West, Room A0.015, Ray Dolby Centre, Cavendish Laboratory.
• Series: Physics and Chemistry of Solids Group; organiser: Stephen Walley.

Add to your calendar or Include in your list

Deep learning models memorize training samples and, as such, they are vulnerable to various attacks directed to retrieve information about the training dataset. The goal of the talk is to quantify this phenomenon, as well as the corresponding defenses in terms of differentially private algorithms, through the lens of high-dimensional regression.

The first part of the talk considers empirical risk minimization, focusing on the memorization of spurious features that are uncorrelated with the learning task. We relate such memorization to two separate terms: (i) the stability of the model with respect to individual training samples, and (ii) the feature alignment between the spurious feature and the full sample. This shows that memorization weakens as the generalization capability increases and, through the precise analysis of the feature alignment, we describe the role of the model and of its activation function. We then discuss spurious correlations between non-predictive features and the associated labels in the training data. We provide a statistical characterization of how such correlations are learnt in high-dimensional regression, unveiling the role of the data covariance, the regularization strength and the over-parameterization.

The second part of the talk considers differentially private gradient descent, a popular algorithm with provable guarantees on the privacy of the training data. While understanding its performance cost with respect to standard gradient descent has received remarkable attention, existing bounds on the excess population risk degrade with over-parameterization. This leaves practitioners without clear guidance, leading some to reduce the effective number of trainable parameters to improve performance, while others use larger models to achieve better results through scale. We show that, for any sufficiently over-parameterized random features model, privacy can be obtained for free, i.e., the excess population risk is negligible not only when the privacy parameter \epsilon has constant order, but also in the strongly private setting \epsilon = o(1). This challenges the common wisdom that over-parameterization inherently hinders performance in private learning.

Bio: Marco Mondelli received the B.S. and M.S. degree in Telecommunications Engineering from the University of Pisa, Italy, in 2010 and 2012, respectively. In 2016, he obtained his Ph.D. degree in Computer and Communication Sciences at EPFL . In 2017-2019, he was a Postdoctoral Scholar in the Department of Electrical Engineering at Stanford University. In 2018, he was also a Research Fellow with the Simons Institute for the Theory of Computing, for the program on “Foundations of Data Science”. He has been a faculty member at the Institute of Science and Technology Austria (ISTA) since 2019, first as an Assistant Professor and, since 2025, as a Professor. His research interests include data science, machine learning, high-dimensional statistics, information theory, and coding theory. He is the recipient of a number of fellowships and awards, including the Jack K. Wolf ISIT Student Paper Award in 2015, the STOC Best Paper Award in 2016, the EPFL Doctorate Award in 2018, the Simons-Berkeley Research Fellowship in 2018, the Lopez-Loreta Prize in 2019, the Information Theory Society Best Paper Award in 2021 and the ERC Starting Grant in 2024.

• Speaker: Prof. Marco Mondelli, Institute of Science and Technology Austria
• Wednesday 28 May 2025, 14:00-15:00
• Venue: MR5, CMS Pavilion A.
• Series: Information Theory Seminar; organiser: Prof. Ramji Venkataramanan.

Add to your calendar or Include in your list

Diffusion models are the standard toolkit for generative modelling of 3D atomic systems. However, for different types of atomic systems – such as molecules and materials – the generative processes are usually highly specific to the target system despite the underlying physics being the same. We introduce the All-atom Diffusion Transformer (ADiT), a unified latent diffusion framework for jointly generating both periodic materials and non-periodic molecular systems using the same model: (1) An autoencoder maps a unified, all-atom representations of molecules and materials to a shared latent embedding space; and (2) A diffusion model is trained to generate new latent embeddings that the autoencoder can decode to sample new molecules or materials. Experiments on QM9 and MP20 datasets demonstrate that jointly trained ADiT generates realistic and valid molecules as well as materials, exceeding state-of-the-art results from molecule and crystal-specific models. ADiT uses standard Transformers for both the autoencoder and diffusion model, resulting in significant speedups during training and inference compared to equivariant diffusion models. Scaling ADiT up to half a billion parameters predictably improves performance, representing a step towards broadly generalizable foundation models for generative chemistry. Open source code: https://github.com/facebookresearch/all-atom-diffusion-transformer

hybrid and recorded

• Speaker: Chaitanya Joshi
• Tuesday 03 June 2025, 13:00-14:00
• Venue: somewhere, Computer Laboratory, William Gates Building.
• Series: Artificial Intelligence Research Group Talks (Computer Laboratory); organiser: Pietro Lio.

Add to your calendar or Include in your list

We present Aeneas, a verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to generate pure models for a large class of safe Rust programs which can contain shared and mutable borrows, functions returning borrows, traits and loops. Doing so, we allow the user to reason about the original Rust program through the theorem prover of their choice, and enable lightweight verification by eliminating memory reasoning, allowing them to instead focus on functional properties of their code. As of today, Aeneas has backends for F\*, Coq, HOL4 and most importantly Lean, for which we are investing efforts to develop custom tactics and automation. Aeneas is currently being used to verify optimised, low-level cryptographic code, that we will present as well.

• Speaker: Son Ho (Azure Research team)
• Friday 30 May 2025, 14:00-15:00
• Venue: SS03, Computer Laboratory.
• Series: Logic and Semantics Seminar (Computer Laboratory); organiser: Ioannis Markakis.

Add to your calendar or Include in your list

The alignment of large language models (LLMs) can often be brittle when faced with the complexities of real-world deployment. In this talk, I share our investigations on two scenarios where special care is required to ensure robust alignment.

The first scenario is multi-objective alignment, where balancing competing objectives is particularly challenging. Our recent work, Robust Multi-Objective Decoding (RMOD), an inference-time alignment algorithm, adaptively adjusts the weights of different objectives during response generation to ensure none are neglected. RMOD provides principled robustness with minimal overhead, consistently outperforming existing methods across several alignment benchmarks.

In the second part of the talk, I will address preference model misspecification in self-play alignment. While self-play is a promising alignment approach, naive implementations are vulnerable to inaccuracies in the preference model. To address this, our Regularized Self-Play Policy Optimization (RSPO) framework offers a versatile and modular method for regularizing the self-play alignment process. RSPO ’s ability to combine various regularizers results in strong performance gains on multiple evaluation sets, such as AlpacaEval-2 and Arena-Hard.

As a bonus, I will briefly introduce our recent investigation into the robustness of Mixture-of-Agent (MoA) systems, a popular multi-agent paradigm. We show that even a single malicious agent introduced into the mixture can nullify the benefits of the entire system.

• Speaker: Dr. Sangwoong Yoon (UCL)
• Friday 23 May 2025, 12:00-13:00
• Venue: ONLINE ONLY. Here is the Zoom link: https://cam-ac-uk.zoom.us/j/4751389294?pwd=Z2ZOSDk0eG1wZldVWG1GVVhrTzFIZz09.
• Series: NLIP Seminar Series; organiser: Suchir Salhan.

Add to your calendar or Include in your list

Abstract not available

• Speaker: Dr Mihai-Cosmin Marinica, CEA Saclay
• Wednesday 22 October 2025, 14:30-15:30
• Venue: Unilever Lecture Theatre, Yusuf Hamied Department of Chemistry.
• Series: Theory - Chemistry Research Interest Group; organiser: Lisa Masters.

Add to your calendar or Include in your list

Abstract

Machine learning rests on three pillars: algorithms, hardware, and data. In the context of close-range forest monitoring, we’ve already seen major advances in the first two—shifting from classical processing methods to neural networks, and from manual tools like tape measures to LiDAR-based laser scanning. These breakthroughs have enabled the development of faster and more accurate forest monitoring algorithms.

However, data remains a bottleneck. High-quality, annotated forest datasets are scarce and costly to produce, and their size still falls short of the scale required for robust machine learning. Meanwhile, the rise of graphics engines—and the success of synthetic data in domains like self-driving and robotics—makes us wonder: can forests benefit from a similar approach? The key challenge lies in whether synthetic forest environments can capture the representations needed for generalisation to real-world data.

In this talk, I’ll focus on the task of instance segmentation of individual trees—a core bottleneck in many field applications. I’ll present my current progress in generating synthetic forest plots and point cloud data using Unreal Engine, and evaluate their performance against a state-of-the-art model trained on a leading real-world dataset. I’ll also discuss upcoming directions and experimental plans. Time permitting, I’ll give a live demo of my synthetic data pipeline, showing how we can go from video games to ML-ready datasets.

This is a work-in-progress talk, and I look forward to feedback and discussion.

Bio

Yihang She is a second-year PhD student in Computer Science at the University of Cambridge. His research focuses on advancing computer vision in the novel context of forest monitoring, spanning both close-range and satellite-based observations.

• Speaker: Yihang She, University of Cambridge
• Thursday 29 May 2025, 13:00-14:00
• Venue: Room GS15 at the William Gates Building and on Zoom: https://cl-cam-ac-uk.zoom.us/j/4361570789?pwd=Nkl2T3ZLaTZwRm05bzRTOUUxY3Q4QT09&from=addon .
• Series: Energy and Environment Group, Department of CST; organiser: lyr24.

Add to your calendar or Include in your list