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

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.

Based on :
A Tight Theory of Error Feedback Algorithms in Distributed Optimization, DB Thomsen, A Taylor, A Dieuleveut
International Conference on Machine Learning (ICML 2026)
Tight analyses of first-order methods with error feedback, DB Thomsen, A Taylor, A Dieuleveut
Advances in Neural Information Processing Systems (NeurIPS) (2025).
PEPit: computer-assisted worst-case analyses of first-order optimization methods in Python
B Goujaud, C Moucer, F Glineur, JM Hendrickx, AB Taylor, A Dieuleveut
Mathematical Programming Computation 16 (3), 337-367  (2024)
(eventually - as a detour) Provable non-accelerations of the heavy-ball method B Goujaud, A Taylor, A Dieuleveut, Mathematical Programming, 1-59  (2025)