POPL 2021 (series) / CPP 2021 (series) / Certified Programs and Proofs /
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
Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30: AI and Machine LearningCPP at CPP Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK Streamed session: https://youtu.be/6NJdWdiZEiA | |||
18:00 - 18:15 Talk | A Formal Proof of PAC Learnability for Decision Stumps CPP Joseph TassarottiBoston College, Koundinya VajjhaUniversity of Pittsburgh, Anindya BanerjeeIMDEA Software Institute, Jean-Baptiste TristanBoston College Pre-print Media Attached | ||
18:15 - 18:30 Talk | CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq CPP Koundinya VajjhaUniversity of Pittsburgh, Avraham ShinnarIBM Research, Barry TragerIBM Research, Vasily PestunIBM Research; IHES, Nathan FultonIBM Research Pre-print Media Attached |