UNIVERSITÄT BERN

STRADA

Scientific Transformations through the Alliance of Domain Knowledge and AI

Computer-aided proofs in first-orderoptimization, with applications to error feedback

Prof. Dr. Aymeric Dieuleveut
Wednesday, May 27, 2026 at 16:15-17:00 in Room B78, ExWi

First-order methods are widely used in optimization and machine learning, and their behavior is often
analyzed through the spectrum of worst case convergence rates. Obtaining such guarantees is often
difficult and both time consuming and error-prone. Starting with the work of Drori and Teboulle (2014),
novel techniques have been used to gain numerical insights, leading to the release of various
performance estimation (PE) software.
In this talk, I will show how various computer-aided techniques can be used to study first-order
optimization methods in a systematic way. From performance estimation problems with automated
Lyapunov discovery, to symbolic regression and computer algebra systems, novel tools completely
reshape the way we approach theory of optimization.
As a main example, I will focus on error feedback methods used with compressed communication in
distributed optimization. While error feedback has been widely studied, existing theory often provides
untight (thus unreliable) bounds. I will present tight analyses with matching lower bounds that allow a fair
comparison between error feedback schemes and standard compressed gradient descent, and help
explain when error feedback is useful and when it is not.
Overall, the talk aims to show how various computer-aided proofs can lead to clearer and more reliable
insights into first-order optimization methods.