A Formal Proof of PAC Learnability for Decision Stumps

TL;DR

This paper provides a formal proof in Lean of the PAC learnability of decision stumps, addressing measure-theoretic subtleties and separating deterministic reasoning from probabilistic analysis.

Contribution

It offers the first fully formalized proof of PAC learnability for decision stumps, clarifying measure-theoretic aspects in the process.

Findings

Formal proof of PAC learnability established

Addresses measure-theoretic subtleties in formalization

Separates deterministic and probabilistic reasoning

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.