A Formal Proof of PAC Learnability for Decision Stumps
This work offers a formal proof for a classic ML theory result, which is incremental as it verifies an existing concept rather than introducing new methods or applications.
The authors tackled the formal verification of PAC learnability for decision stumps by providing a proof in Lean, addressing analytic and measure-theoretic subtleties to derive error probability bounds.
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.