Prossimi seminari del Dipartimento di Matematica

Mathematical formalization has attracted increasing attention in recent years, with Lean 4 emerging as one of the central tools in this area. This series of four seminars will introduce mathematical formalization, discuss its significance, and showcase recent examples of successful formalization projects. Two of the seminars will provide hands-on tutorials using the interactive theorem prover Lean 4. In the final seminar, we will examine how artificial intelligence and formalization interact, highlighting recent developments in autoformalization and automatic theorem proving.

Mathematical formalization has attracted increasing attention in recent years, with Lean 4 emerging as one of the central tools in this area. This series of four seminars will introduce mathematical formalization, discuss its significance, and showcase recent examples of successful formalization projects. Two of the seminars will provide hands-on tutorials using the interactive theorem prover Lean 4. In the final seminar, we will examine how artificial intelligence and formalization interact, highlighting recent developments in autoformalization and automatic theorem proving.

Mathematical formalization has attracted increasing attention in recent years, with Lean 4 emerging as one of the central tools in this area. This series of four seminars will introduce mathematical formalization, discuss its significance, and showcase recent examples of successful formalization projects. Two of the seminars will provide hands-on tutorials using the interactive theorem prover Lean 4. In the final seminar, we will examine how artificial intelligence and formalization interact, highlighting recent developments in autoformalization and automatic theorem proving.

Mathematical formalization has attracted increasing attention in recent years, with Lean 4 emerging as one of the central tools in this area. This series of four seminars will introduce mathematical formalization, discuss its significance, and showcase recent examples of successful formalization projects. Two of the seminars will provide hands-on tutorials using the interactive theorem prover Lean 4. In the final seminar, we will examine how artificial intelligence and formalization interact, highlighting recent developments in autoformalization and automatic theorem proving.

This teaching unit will introduce students to the Bayesian statistical framework for performing inference in high-dimensional inverse problems related to imaging sciences. We will start from basic concepts on probabilistic modelling, Bayesian decision theory, and Monte Carlo integration for Bayesian computation, and progress quickly to modern Bayesian imaging approaches. We will pay special attention to strategies based on stochastic diffusion processes and to Bayesian imaging models that combine elements derived from machine learning with elements derived from the physics of the considered imaging problem. The key ideas and techniques will be illustrated on imaging problems where we will conduct challenges inferences such as uncertainty quantification, hypothesis testing, model self-calibration, and model selection without ground truth.

This teaching unit introduces a computational "toolbox" for learning priors in the context of solving Bayesian inverse problems in imaging. The tools covered include methods for learning optimal discretizations of total-variation related regularization terms, explicit diffusion models based on products of 1D Gaussian mixture models, and the application of the maximum entropy principle for learning generative priors.

This question has been much discussed in physics and one suggestion is that the long time persistence of classical/quantum correspondence is due to interaction of a small, observed system with a larger environment. Lindblad or GKSL evolution is one of the standard models for describing such interactions. In that context the question of the length of time of classical/quantum agreement was recently revisited in physics by Hernández-Ranard-Riedel. In my talk I will introduce the concept of Lindblad evolution and present results showing that the evolution of a quantum observable remains close to the classical Fokker-Planck evolution in the Hilbert-Schmidt norm for times vastly exceeding the Ehrenfest time (the limit of such an agreement when there is no interaction with a larger system). The time scale is the same as in two recent papers by Hernández-Ranard-Riedel but the statement and methods are different. The talk is based on joint work with J Galkowski and numerical results obtained jointly with Z Huang. I will also comment on recent progress on trace class estimates by Z Li and on the hypoelliptic case by H Smith.

We will introduce the basic concepts of (deterministic) regularisation theory and discuss model- and data-driven regularisations. We will discover how these concepts can be utilised to optimally sample data in magnetic resonance imaging and single-pixel camera applications, or to construct decoders for trained encoders in deep learning without additional training of the decoder.

Note: this is the first part of a two-part seminar. AI is progressing at a remarkable speed, but we still don’t have a clear understanding of basic concepts in cognition (e.g. learning, understanding, abstraction, awareness, intelligence, etc). I shall argue that research focused on understanding how learning machines such as LLMs or deep neural networks do what they do, sidesteps the key issue by defining these concepts from the outset. For example, statistical learning is based on a classification of problems (supervised/unsupervised, classification, regression etc.) and addresses the resulting optimisation problem (maximisation of the likelihood, minimisation of errors, etc). Learning entails first of all detecting what makes sense to be learned 1) from very few samples, and 2) without a priori knowing why that date makes sense. This requires a quantitative notion of relevance that can distinguish data that makes sense from meaningless noise. I will first introduce and discuss the notion of relevance. Next I will claim that learning differs from understanding, where the latter implies integrating data that make sense into a pre-existing representation. The properties of this representation should be abstract, i.e. independent of the data, precisely because they need to represent data of a widely different domain. This is what enables higher cognitive functions that we do all the time, like drawing analogies and relating data learned independently from widely different domains. Such a representation should be flexible and continuously adaptable if more data or more resources are made available. I will show that such an abstract representation can be defined as the fixed point of a renormalisation group transformation, and it coincides with a model that can be defined from the principle of maximal relevance. I will provide empirical evidence that the representations of simple neural networks approach this universal model as the network is trained on a broader and broader domain of data. Overall, the aim of the seminar is to support the idea that an approach to central issues in cognition is also possible studying very simple models and does not necessarily require understanding large machine learning models.

Note: this is the second part of a two-part seminar. AI is progressing at a remarkable speed, but we still don’t have a clear understanding of basic concepts in cognition (e.g. learning, understanding, abstraction, awareness, intelligence, etc). I shall argue that research focused on understanding how learning machines such as LLMs or deep neural networks do what they do, sidesteps the key issue by defining these concepts from the outset. For example, statistical learning is based on a classification of problems (supervised/unsupervised, classification, regression etc.) and addresses the resulting optimisation problem (maximisation of the likelihood, minimisation of errors, etc). Learning entails first of all detecting what makes sense to be learned 1) from very few samples, and 2) without a priori knowing why that date makes sense. This requires a quantitative notion of relevance that can distinguish data that makes sense from meaningless noise. I will first introduce and discuss the notion of relevance. Next I will claim that learning differs from understanding, where the latter implies integrating data that make sense into a pre-existing representation. The properties of this representation should be abstract, i.e. independent of the data, precisely because they need to represent data of a widely different domain. This is what enables higher cognitive functions that we do all the time, like drawing analogies and relating data learned independently from widely different domains. Such a representation should be flexible and continuously adaptable if more data or more resources are made available. I will show that such an abstract representation can be defined as the fixed point of a renormalisation group transformation, and it coincides with a model that can be defined from the principle of maximal relevance. I will provide empirical evidence that the representations of simple neural networks approach this universal model as the network is trained on a broader and broader domain of data. Overall, the aim of the seminar is to support the idea that an approach to central issues in cognition is also possible studying very simple models and does not necessarily require understanding large machine learning models.

This seminar will cover some concepts and recent advances in the emerging field of self-supervised learning methods for solving imaging inverse problems with deep neural networks. Self-supervised learning is a fundamental tool deploying deep learning solutions in scientific and medical imaging applications where obtaining a large dataset of ground-truth images is very expensive or impossible. The seminar will present different self-supervised methods, discuss their theoretical underpinnings and present practical self-supervised imaging applications. Finally, I will discuss my experience developing and collaborating on open-source software for science (https://deepinv.github.io/), and some of the lessons learned along the way.

TBA