@inproceedings{65a34aaf6f5d43c98e43f295cf511081,
title = "A formal proof of PAC learnability for decision stumps",
abstract = "We present a formal proof in Lean of probably approximately correct (PAC) learnability of the concept class of decision stumps. This classic result in machine learning theory derives a bound on error probabilities for a simple type of classifier. Though such a proof appears simple on paper, analytic and measure-theoretic subtleties arise when carrying it out fully formally. Our proof is structured so as to separate reasoning about deterministic properties of a learning function from proofs of measurability and analysis of probabilities.",
keywords = "decision stumps, interactive theorem proving, probably approximately correct",
author = "Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Tristan, {Jean Baptiste}",
note = "Publisher Copyright: {\textcopyright} 2021 ACM.; 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 ; Conference date: 17-01-2021 Through 19-01-2021",
year = "2021",
month = jan,
day = "17",
doi = "10.1145/3437992.3439917",
language = "English (US)",
series = "CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021",
publisher = "Association for Computing Machinery, Inc",
pages = "5--17",
editor = "Catalin Hritcu and Andrei Popescu",
booktitle = "CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021",
}