A Formal Proof of PAC Learnability for Decision Stumps
Machine Learning
2021-01-11 v3 Logic in Computer Science
Machine Learning
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.
Cite
@article{arxiv.1911.00385,
title = {A Formal Proof of PAC Learnability for Decision Stumps},
author = {Joseph Tassarotti and Koundinya Vajjha and Anindya Banerjee and Jean-Baptiste Tristan},
journal= {arXiv preprint arXiv:1911.00385},
year = {2021}
}
Comments
13 pages, appeared in Certified Programs and Proofs (CPP) 2021