2026-07-22T19:10:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20767 2024-09-02T10:03:25Z ddc:004 open_access

Robust Mean Estimation by All Means (Short Paper) Affeldt, Reynald Barrett, Clark Bruni, Alessandro Daukantas, Ieva Khan, Harun Saikawa, Takafumi Schürmann, Carsten robust statistics probability theory formal verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Reynald Affeldt and Clark Barrett and Alessandro Bruni and Ieva Daukantas and Harun Khan and Takafumi Saikawa and Carsten Schürmann 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.39 urn:nbn:de:0030-drops-207679 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.39 eng https://creativecommons.org/licenses/by/4.0/legalcode