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.

Conference Day
Tue 19 Jan

Displayed 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
15m
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
15m
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