DROPS

Document

Short Paper

DOI: 10.4230/LIPIcs.ITP.2024.39

Robust Mean Estimation by All Means (Short Paper)

Authors: Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

We report the results of a verification experiment on an algorithm for robust mean estimation, i.e., an algorithm that computes a mean in the presence of outliers. We formalize the algorithm in the Coq proof assistant and devise a pragmatic approach for identifying and solving issues related to the choice of bounds. To keep our formalization succinct and generic, we recast the original argument using an existing library for finite probabilities that we extend with reusable lemmas. To formalize the original algorithm, which relies on a subtle convergence argument, we observe that by adding suitable termination checks, we can turn it into a well-founded recursion without losing its original properties. We also exploit a tactic for solving real-valued inequalities by approximation to heuristically fix inaccurate constant values in the original proof.

Cite as

Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, and Carsten Schürmann. Robust Mean Estimation by All Means (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 39:1-39:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.39,
  author =	{Affeldt, Reynald and Barrett, Clark and Bruni, Alessandro and Daukantas, Ieva and Khan, Harun and Saikawa, Takafumi and Sch\"{u}rmann, Carsten},
  title =	{{Robust Mean Estimation by All Means}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{39:1--39:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.39},
  URN =		{urn:nbn:de:0030-drops-207679},
  doi =		{10.4230/LIPIcs.ITP.2024.39},
  annote =	{Keywords: robust statistics, probability theory, formal verification}
}

Search Results

Documents authored by Khan, Harun

Robust Mean Estimation by All Means (Short Paper)

Abstract

Cite as

Thanks for your feedback!

Could not send message