Documentation

Complexity.MachineLearning.UniformLearning.MembershipQuery

Learning with membership queries #

A learner with membership queries may ask for the value f x of the unknown target f at any point x of its choice [Ang88]. With its random choices fixed, it is a decision tree whose variables are the points of the cube: run on the truth table of f, the query of the variable x returns f x, and the leaf it reaches is the hypothesis. So a randomized membership-query learner is a family of such decision trees indexed by random seeds drawn from a distribution (UniformLearning.QueryLearner), and the depth of the trees bounds the number of queries on every run (UniformLearning.QueryLearner.QueriesAtMost). It learns a concept class with error ε and confidence 1 - δ (UniformLearning.QueryLearner.Learns) if, for every target in the class, the hypothesis has error above ε under the uniform distribution (UniformLearning.uniformError) with probability at most δ over the seed. Membership queries subsume random examples: querying uniformly random points simulates a learner from uniform random examples, which learns exactly the same classes (UniformLearning.QueryLearner.learns_ofLearner_iff). This is learning under the uniform distribution with queries O'Donnell, Definition 3.27; the query model has no counterpart in PACLearning, whose learners see only labelled samples.

A non-adaptive learner chooses its query points from the seed alone, and then computes its hypothesis from the answers (UniformLearning.QueryLearner.ofNonadaptive); it makes as many queries as it lists points (UniformLearning.QueryLearner.depth_ofNonadaptive_le).

Main definitions #

Main results #

References #

source
@[reducible, inline]
abbrev Cslib.MachineLearning.UniformLearning.QueryLearner (ι : Type u_1) (Ω : Type u_2) :
Type (max u_1 u_2)

A learner with membership queries on the cube ι → Bool, with random seeds in Ω: for each seed, a decision tree whose variables are the points of the cube and whose leaves are hypotheses. Run on the truth table of the target f, the query of the point x returns f x.

Instances For
    source
    def Cslib.MachineLearning.UniformLearning.QueryLearner.QueriesAtMost {ι : Type u_1} {Ω : Type u_2} (A : QueryLearner ι Ω) (q : ℕ) :
    Prop

    The learner A makes at most q membership queries on every seed and every target.

    Instances For
      source
      def Cslib.MachineLearning.UniformLearning.QueryLearner.Learns {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] (A : QueryLearner ι Ω) (μ : PMF Ω) (C : PACLearning.ConceptClass (ι → Bool) Bool) (ε δ : ℝ) :
      Prop

      The learner A learns the concept class C with membership queries, with seeds drawn from μ, error ε and confidence 1 - δ: for every target f ∈ C, the hypothesis output by A on f has error above ε with probability at most δ.

      Instances For
        source
        theorem Cslib.MachineLearning.UniformLearning.QueryLearner.Learns.mono {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] {A : QueryLearner ι Ω} {μ : PMF Ω} {C C' : PACLearning.ConceptClass (ι → Bool) Bool} {ε ε' δ δ' : ℝ} (hA : A.Learns μ C ε δ) (hC : C' ⊆ C) (hε : ε ≤ ε') (hδ : δ ≤ δ') :
        A.Learns μ C' ε' δ'

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

        source
        theorem Cslib.MachineLearning.UniformLearning.QueryLearner.learns_iff {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι] {A : QueryLearner ι Ω} {μ : PMF Ω} {C : PACLearning.ConceptClass (ι → Bool) Bool} {ε δ : ℝ} :
        A.Learns μ C ε δ ↔ ∀ f ∈ C, μ.toOuterMeasure {ω : Ω | ε < uniformError f ((A ω).eval f)} ≤ ENNReal.ofReal δ

        A learner learns C when, for every target f ∈ C, the seeds on which it outputs a hypothesis of error above ε have probability at most δ.

        source
        def Cslib.MachineLearning.UniformLearning.QueryLearner.ofNonadaptive {ι : Type u_1} {Ω : Type u_2} [Fintype ι] (points : Ω → List (ι → Bool)) (hyp : ((ι → Bool) → Bool) → Ω → (ι → Bool) → Bool) :
        QueryLearner ι Ω

        The non-adaptive learner that queries the points points ω and outputs hyp g ω, computed from the answers g at those points.

        Instances For
          source
          theorem Cslib.MachineLearning.UniformLearning.QueryLearner.eval_ofNonadaptive {ι : Type u_1} {Ω : Type u_2} [Fintype ι] {points : Ω → List (ι → Bool)} {hyp : ((ι → Bool) → Bool) → Ω → (ι → Bool) → Bool} (hhyp : ∀ (ω : Ω) (g g' : (ι → Bool) → Bool), (∀ x ∈ points ω, g x = g' x) → hyp g ω = hyp g' ω) (f : (ι → Bool) → Bool) (ω : Ω) :
          (ofNonadaptive points hyp ω).eval f = hyp f ω

          If the hypothesis depends only on the answers at the queried points, the non-adaptive learner run on f outputs hyp f ω.

          source
          theorem Cslib.MachineLearning.UniformLearning.QueryLearner.depth_ofNonadaptive_le {ι : Type u_1} {Ω : Type u_2} [Fintype ι] (points : Ω → List (ι → Bool)) (hyp : ((ι → Bool) → Bool) → Ω → (ι → Bool) → Bool) (ω : Ω) :
          (ofNonadaptive points hyp ω).depth ≤ (points ω).length

          The non-adaptive learner makes at most as many queries as it lists points.

          source
          def Cslib.MachineLearning.UniformLearning.QueryLearner.ofLearner {ι : Type u_1} [Fintype ι] {m : ℕ} (A : PACLearning.Learner (ι → Bool) Bool m) :
          QueryLearner ι (Fin m → ι → Bool)

          The membership-query learner simulating the learner A from random examples: it queries the target at m uniformly random points and runs A on the resulting examples.

          Instances For
            source
            theorem Cslib.MachineLearning.UniformLearning.QueryLearner.eval_ofLearner {ι : Type u_1} [Fintype ι] {m : ℕ} (A : PACLearning.Learner (ι → Bool) Bool m) (f : (ι → Bool) → Bool) (x : Fin m → ι → Bool) :
            (ofLearner A x).eval f = A (examples f x)

            Run on the target f, the simulating learner outputs the hypothesis of A on the examples of f at its seed.

            source
            theorem Cslib.MachineLearning.UniformLearning.QueryLearner.queriesAtMost_ofLearner {ι : Type u_1} [Fintype ι] {m : ℕ} (A : PACLearning.Learner (ι → Bool) Bool m) :
            (ofLearner A).QueriesAtMost m

            The simulating learner makes m queries.

            source
            theorem Cslib.MachineLearning.UniformLearning.QueryLearner.learns_ofLearner_iff {ι : Type u_1} [Fintype ι] {m : ℕ} [DecidableEq ι] {A : PACLearning.Learner (ι → Bool) Bool m} {C : PACLearning.ConceptClass (ι → Bool) Bool} {ε δ : ℝ} :
            (ofLearner A).Learns (Probability.PMF.uniformOfFintype (Fin m → ι → Bool)) C ε δ ↔ UniformLearning.Learns A C ε δ

            Membership queries subsume random examples: with uniform seeds, the learner simulating A learns exactly the classes that A learns from uniform random examples.