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.
Tue 19 Jan Times are displayed in 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