A Formal Proof of PAC Learnability for Decision Stumps
We present a machine-checked, formal proof of 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. We construct and check our proof using the Lean theorem prover. Though such a proof appears simple on paper, analytic and measure-theoretic subtleties arise when carrying it out fully formally. We explain how we can cleanly separate out parts that deal with these subtleties.
Conference DayTue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30
|A Formal Proof of PAC Learnability for Decision Stumps|
Joseph TassarottiBoston College, Koundinya VajjhaUniversity of Pittsburgh, Anindya BanerjeeIMDEA Software Institute, Jean-Baptiste TristanBoston CollegePre-print Media Attached
|CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq|
Koundinya VajjhaUniversity of Pittsburgh, Avraham ShinnarIBM Research, Barry TragerIBM Research, Vasily PestunIBM Research; IHES, Nathan FultonIBM ResearchPre-print Media Attached