Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 18:00 - 18:15 at CPP - AI and Machine Learning Chair(s): Ekaterina Komendantskaya

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: AI and Machine LearningCPP at CPP
Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK

Streamed session: https://youtu.be/6NJdWdiZEiA

18:00 - 18:15
A Formal Proof of PAC Learnability for Decision Stumps
Joseph TassarottiBoston College, Koundinya VajjhaUniversity of Pittsburgh, Anindya BanerjeeIMDEA Software Institute, Jean-Baptiste TristanBoston College
Pre-print Media Attached
18:15 - 18:30
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 Research
Pre-print Media Attached