🐙Lean & Math-AI Seminar
Title: Training-Free Approaches for Image Inversion and Editing Using Latent Generative Models
Speaker: Sanjay Shakkottai, University of Texas, Austin
Date: Wed, 13 Aug 2025
Time: 5:30 pm
Venue: LH-1, Mathematics Department
Diffusion-based generative models transform random noise into images; their inversion aims to transform images back to structured noise that is suitable for recovery and editing. In this talk, we present Reference-Based Modulation (RB-Modulation), a plug-and-play solution for training-free editing and stylization of diffusion models. Existing training-free approaches exhibit difficulties in (a) style extraction from reference images in the absence of additional style or content text descriptions, (b) unwanted content leakage from reference style images, and (c) effective composition of style and content. RB-Modulation is built on a novel stochastic optimal controller where a style descriptor encodes the desired attributes through a terminal cost. The resulting drift not only overcomes the difficulties above, but it also ensures high fidelity to the reference style and adheres to the given text prompt. We also introduce a cross-attention-based feature aggregation scheme that allows RB-Modulation to decouple content and style from the reference image. Next, we study inversion and image editing using Rectified Flow (RF) models (such as Flux, the current state-of-art model for image generation). We present RF-Inversion using dynamic optimal control derived via a linear quadratic regulator. We show that the resulting vector field is equivalent to a rectified stochastic differential equation. Additionally, we extend our framework to design a stochastic sampler for Flux. Our inversion method allows for state-of-art performance in zero-shot inversion and editing, outperforming prior works in stroke-to-image synthesis and semantic image editing, with large-scale human evaluations confirming user preference. Our work is being productionized within Google across several platforms including Pixel and YouTube.
Projects: (ICLR 2025 — https://rb-modulation.github.io/ ), (ICLR 2025 — https://rf-inversion.github.io/ ), (CVPR 2024 — https://stsl-inverse-edit.github.io/ ), (Tutorial on diffusion models: https://www.youtube.com/watch?v=NJ72iEPRXFk )
Biography
Sanjay Shakkottai received his Ph.D. from the ECE Department at the University of Illinois at Urbana-Champaign in 2002. He is with The University of Texas at Austin, where he is a Professor in the Chandra Family Department of Electrical and Computer Engineering, and holds the Cockrell Family Chair in Engineering #15. He is also the Director of the Center for Generative AI, which hosts a campus-wide GPU cluster at UT Austin. He received the NSF CAREER award in 2004 and was elected as an IEEE Fellow in 2014. He was a co-recipient of the IEEE Communications Society William R. Bennett Prize in 2021. He has served as the Editor in Chief of IEEE/ACM Transactions on Networking. His current research interests are in Generative AI, with applications to language models, image editing, and network decision-making.
Title: Opportunities in Math-AI and Lean-Math-AI
Speaker: Ashvni Narayanan, SMRI, Sydney, Australia
Date: Wed, 23 Apr 2025
Time: 4 pm
Venue: LH-3, Mathematics Department
Title: Lean for Teaching
Speaker: Patrick Massot, Université Paris-Saclay, Saint-Aubin, France
Date: Tue, 22 Apr 2025
Time: 4 pm
Venue: LH-3, Mathematics Department
I will describe how the Lean proof assistant software can be used to teach mathematical reasoning to young students at university. This is different from teaching how to use Lean. Here Lean is only a tool, not the end goal.
I will explain what we can hope to teach using this tool, what are the available resources for teachers, and what choices should be made. I will then show my teaching library, Verbose Lean, which uses controlled natural language and customizable automation to optimize transfer of skills to paper proofs.
Title: Certifying Algebraic Number Theory Computation
Speaker: Anne Baanen, Lean FRO
Date: Tue, 22 Apr 2025
Time: 11 am
Venue: LH-3, Mathematics Department (Joint with the Number Theory Seminar)
Number fields and their rings of integers are fundamental objects in algebraic number theory. Computational information on these objects is available in computer algebra systems and databases. To make these values available to formalization in Lean 4, without tediously redoing existing work, we developed a variety of certificates that allow Lean to efficiently verify the outcome of computations. In particular I will focus on computing and certifying the ring of integers. The work of this talk is joint with Alain Chavarri Villarello and Sander Dahmen at Vrije Universiteit Amsterdam.
Title: Formalization of $p$-adic $L$-functions in Lean 3
Speaker: Ashvni Narayanan (London school of Geometry and Number Theory; Sydney University)
Date: Wed, 13 Sep 2023
Time: 4:00 pm
Venue: LH-1, Mathematics Department
The Kubota-Leopoldt $p$-adic $L$-function is an important concept in number theory. It takes special values in terms of generalized Bernoulli numbers, and helps solve Kummer congruences. It is also used in Iwasawa theory. Formalization of $p$-adic $L$-functions has been done for the first time in a theorem prover called Lean 3. In this talk, we shall briefly introduce the concept of formalization of mathematics, the theory behind $p$-adic $L$-functions, and its formalization.