maxhaslbeck / verml

Verification of Machine Learning Practical Course

verML - Verification of Machine Learning Practical Course

This repository collects efforts to formalize results on machine learning following the book "Understanding Machine Learning" by Shalev-Shwartz and Ben-David.

It features the following verifications:

• Basics:
  • LearningTheory formalizes basic notation from Chapter 2
  • FiniteHypClasses proves that finite Hypothesis classes are PAC
• VC dimension:
  • VCDim formalizes results from Chapter 6
• Boosting:
  • Boosting formalizes AdaBoost following Chapter 10
• Soft SVM:
  • SVM formalizes soft SVM following Chapter 15

verml's Issues

Add CONTRIBUTING.md

Add a description how contributing to the project works.

Make theories on Boosting conform guidelines

Refactor and add documentation to the theories of the Boosting theories.

The theories should adhere to the Isabelle Community Conventions.

Prove Theorem 6.11

In the formalization of Boosting a crucial theorem is not proven yet: Theorem 6.11.
It is very important, as it provides the bridge between combinatorics and probability theory.

verML/VCDim.thy

Lines 730 to 735 in 9c98ae3

	section \<open>Theorem 6.11\<close>
	lemma assumes "set_pmf D \<subseteq> (X\<times>Y)"
	and "\<delta>\<in>{x.0<x\<and>x<1}"
	shows theorem611: "measure_pmf.prob (Samples m D) {S. \<forall>h\<in>H. abs(PredErr D h - TrainErr S {0..<m} h)
	\<le> (4+sqrt(ln(real(growth (2*m)))))/(\<delta> * sqrt(2*m))} \<ge> 1 - \<delta>"
	sorry

There are attempts to prove it following the Understanding Machine Learning book, but they are not complete.

• [Theorem611.thy] contains a collection of mostly failed attempts
• [NewTry.thy] contains a second attempt, that was not finished yet