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.
Author supplied keywords
Cite
CITATION STYLE
Tassarotti, J., Vajjha, K., Banerjee, A., & Tristan, J. B. (2021). A formal proof of PAC learnability for decision stumps. In CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021 (pp. 5–17). Association for Computing Machinery, Inc. https://doi.org/10.1145/3437992.3439917
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
