← All papers
A Formal Proof of PAC Learnability for Decision Stumps
cs.LG
Nov 1, 2019 · v1
TL;DR
Formalizes a PAC learnability proof for decision stumps in Lean with measure theory.
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.
Problem
PAC learnability of decision stumps is a classic result in machine learning theory, but its formal proof involves analytic and measure-theoretic subtleties that make full formalization non-trivial.
Approach
The authors present a formal proof in Lean of PAC learnability of the concept class of decision stumps. The proof is structured to separate reasoning about deterministic properties of a learning function from proofs of measurability and analysis of probabilities.
Results
The formalization provides a complete machine-checked proof of PAC learnability for decision stumps, addressing the measure-theoretic and analytic subtleties that arise in the formal setting.