“Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation”
Mercoledì 22 Dicembre 2021, ore 11:00 - Aula 2BC30 e Zoom - Alessandro Bruni (IT University of Copenhagen)
Abstract
The operation of trimming data sets is heavily used in AI systems. Trimming is useful to make these AI systems more robust against adversarial or common perturbations. At the core of robust AI systems lies concept that outliers in a data set occur with low probability, and therefore can be discarded without loss of precision in the result. The statistical argument that formalizes this concept of robustness is based on an extension of the Chebyshev’s inequality first proposed by Tukey in 1960, which we call robustness.
In this paper we present a mechanized proof of robustness of the trimmed mean algorithm, which is a statistical method underlying many complex applications of deep learning. For this purpose we use the Coq proof assistant to formalize Tukey’s extension to Chebyshev’s inequality, which allows us to verify the robustness of the trimmed mean algorithm. Our contribution shows the viability of mechanized robustness arguments for algorithms that are at the foundation of complex AI systems. The key result of this paper has wide applicability in machine learning theory.
