Learning from uniform random examples

A concept over the cube is a Boolean function f : (ι → Bool) → Bool, and a concept class is a PACLearning.ConceptClass (ι → Bool) Bool. A deterministic learner from m examples is a PACLearning.Learner (ι → Bool) Bool m: it maps a PACLearning.LabeledSample of m labelled points to a hypothesis. Here the examples of the unknown target f are labelled at independent uniformly random points (UniformLearning.examples, UniformLearning.uniformExamples), and the error of a hypothesis h is the fraction of the points where it differs from f (UniformLearning.uniformError): the probability that h misclassifies a fresh uniform point. A learner learns a class with error ε and confidence 1 - δ under the uniform distribution (UniformLearning.Learns) if, for every target in the class, the hypothesis has error above ε with probability at most δ over the examples. This is learning from random examples under the uniform distribution, the setting of the low-degree algorithm of Linial, Mansour and Nisan [LMN93] O'Donnell, Definition 3.27.

Valiant's model of probably approximately correct learning, PACLearning.IsPACLearnerFor [Val84], is distribution-free, and in its computational form asks for learners running in polynomial time. Learning under the uniform distribution is the special case of the realizable family of the uniform distribution labelled by a concept (UniformLearning.uniformRealizable): a learner that learns C under the uniform distribution is a PAC learner for C over that family (UniformLearning.Learns.isPACLearnerFor). The definitions here are information-theoretic: they bound the number of examples, not the running time of the learner.

Main definitions

• Cslib.MachineLearning.UniformLearning.examples, Cslib.MachineLearning.UniformLearning.uniformExamples: the examples of a concept at given points, and at independent uniform points.
• Cslib.MachineLearning.UniformLearning.uniformError: the error of a hypothesis under the uniform distribution.
• Cslib.MachineLearning.UniformLearning.Learns: learning a concept class from uniform random examples.
• Cslib.MachineLearning.UniformLearning.uniformRealizable: the uniform distribution labelled by the concepts of a class, as a family of distributions on labelled points.

Main results

• Cslib.MachineLearning.UniformLearning.uniformExamples_eq_pi: the examples are independent.
• Cslib.MachineLearning.UniformLearning.learns_iff: learning in terms of uniform samples of points.
• Cslib.MachineLearning.UniformLearning.mem_uniformRealizable_iff: the uniform realizable family as pushforwards along the graphs of concepts.
• Cslib.MachineLearning.UniformLearning.Learns.isPACLearnerFor: learning under the uniform distribution is PAC learning over the uniform realizable family.

References

• L. G. Valiant, A theory of the learnable
• N. Linial, Y. Mansour, N. Nisan, Constant depth circuits, Fourier transform, and learnability
• R. O'Donnell, Analysis of Boolean Functions

def Cslib.MachineLearning.UniformLearning.examples {ι : Type u_1} {m : ℕ} (f : (ι → Bool) → Bool) (x : Fin m → ι → Bool) : PACLearning.LabeledSample (ι → Bool) Bool m

The examples of f at the points x j: the labelled pairs (x j, f (x j)).

@[simp]

theorem Cslib.MachineLearning.UniformLearning.examples_apply {ι : Type u_1} {m : ℕ} (f : (ι → Bool) → Bool) (x : Fin m → ι → Bool) (j : Fin m) : examples f x j = (x j, f (x j))

noncomputable def Cslib.MachineLearning.UniformLearning.uniformExamples {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (m : ℕ) : PMF (PACLearning.LabeledSample (ι → Bool) Bool m)

m labelled examples of f at independent uniformly random points.

theorem Cslib.MachineLearning.UniformLearning.uniformExamples_eq_pi {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (m : ℕ) : uniformExamples f m = Probability.PMF.pi fun (x : Fin m) => PMF.map (fun (x : ι → Bool) => (x, f x)) (Probability.PMF.uniformOfFintype (ι → Bool))

The examples are independent, each a uniform point labelled by f.

noncomputable def Cslib.MachineLearning.UniformLearning.uniformError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f h : (ι → Bool) → Bool) : ℝ

The error of a hypothesis h for the target f under the uniform distribution: the fraction of the points where h and f differ.

theorem Cslib.MachineLearning.UniformLearning.uniformError_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f h : (ι → Bool) → Bool) : 0 ≤ uniformError f h

@[simp]

theorem Cslib.MachineLearning.UniformLearning.uniformError_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) : uniformError f f = 0

theorem Cslib.MachineLearning.UniformLearning.uniformError_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f h : (ι → Bool) → Bool) : uniformError f h ≤ 1

The error of a hypothesis is at most one.

def Cslib.MachineLearning.UniformLearning.Learns {ι : Type u_1} {m : ℕ} [Fintype ι] [DecidableEq ι] (A : PACLearning.Learner (ι → Bool) Bool m) (C : PACLearning.ConceptClass (ι → Bool) Bool) (ε δ : ℝ) : Prop

The learner A learns the concept class C from m uniform random examples with error ε and confidence 1 - δ: for every target f ∈ C, the hypothesis output by A on m examples of f at independent uniform points has error above ε with probability at most δ.

theorem Cslib.MachineLearning.UniformLearning.learns_iff {ι : Type u_1} {m : ℕ} [Fintype ι] [DecidableEq ι] {A : PACLearning.Learner (ι → Bool) Bool m} {C : PACLearning.ConceptClass (ι → Bool) Bool} {ε δ : ℝ} : Learns A C ε δ ↔ ∀ f ∈ C, (Probability.PMF.uniformOfFintype (Fin m → ι → Bool)).toOuterMeasure {x : Fin m → ι → Bool | ε < uniformError f (A (examples f x))} ≤ ENNReal.ofReal δ

A learner learns C exactly when, for every target f ∈ C, the uniform samples of m points whose examples lead to a hypothesis of error above ε have probability at most δ.

theorem Cslib.MachineLearning.UniformLearning.Learns.mono {ι : Type u_1} {m : ℕ} [Fintype ι] [DecidableEq ι] {A : PACLearning.Learner (ι → Bool) Bool m} {C C' : PACLearning.ConceptClass (ι → Bool) Bool} {ε ε' δ δ' : ℝ} (hA : Learns A C ε δ) (hC : C' ⊆ C) (hε : ε ≤ ε') (hδ : δ ≤ δ') : Learns A C' ε' δ'

Learning is monotone: a smaller class, a larger error and a smaller confidence.

The uniform realizable family

def Cslib.MachineLearning.UniformLearning.uniformRealizable {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : PACLearning.ConceptClass (ι → Bool) Bool) : Set (MeasureTheory.Measure ((ι → Bool) × Bool))

The uniform realizable family of a concept class C: the distributions of a uniform point labelled by a concept of C.

theorem Cslib.MachineLearning.UniformLearning.mem_uniformRealizable_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : PACLearning.ConceptClass (ι → Bool) Bool} {D : MeasureTheory.Measure ((ι → Bool) × Bool)} : D ∈ uniformRealizable C ↔ ∃ c ∈ C, D = MeasureTheory.Measure.map (fun (x : ι → Bool) => (x, c x)) (Probability.PMF.uniformOfFintype (ι → Bool)).toMeasure

The uniform realizable family consists of the pushforwards of the uniform distribution along the graphs x ↦ (x, c x) of the concepts c ∈ C: the realizable distributions of PACLearning with the uniform distribution on points.

theorem Cslib.MachineLearning.UniformLearning.error_map_eq_ofReal_uniformError {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f h : (ι → Bool) → Bool) : PACLearning.error (PMF.map (fun (x : ι → Bool) => (x, f x)) (Probability.PMF.uniformOfFintype (ι → Bool))).toMeasure h = ENNReal.ofReal (uniformError f h)

Under the uniform distribution labelled by f, the error of h is its uniform error.

theorem Cslib.MachineLearning.UniformLearning.Learns.isPACLearnerFor {ι : Type u_1} {m : ℕ} [Fintype ι] [DecidableEq ι] {A : PACLearning.Learner (ι → Bool) Bool m} {C : PACLearning.ConceptClass (ι → Bool) Bool} {ε δ : ↑(Set.Ioo 0 1)} (hA : Learns A C ↑↑ε ↑↑δ) : PACLearning.IsPACLearnerFor m ε δ C (uniformRealizable C)

Learning under the uniform distribution is PAC learning over the uniform realizable family: a learner that learns C from m uniform random examples with error ε and confidence 1 - δ witnesses PACLearning.IsPACLearnerFor m ε δ C (uniformRealizable C).