Documentation

Complexity.MachineLearning.UniformLearning.LowDegree

The low-degree algorithm #

The low-degree algorithm of Linial, Mansour and Nisan [LMN93] O'Donnell, Section 3.4 learns from uniform random examples every Boolean function whose Fourier spectrum is concentrated on the sets of at most t coordinates. From m examples (x_j, y_j) it estimates each Fourier coefficient f̂(S) with #S ≤ t by the empirical average c̃(S) = (1 / m) ∑_j y_j χ_S(x_j), reading the labels as signs (UniformLearning.empiricalCoeff), and outputs the sign of the truncated expansion ∑_{#S ≤ t} c̃(S) χ_S (UniformLearning.lowDegreeHypothesis, UniformLearning.lowDegreeLearner).

Each c̃(S) is an average of m independent values in [-1, 1] with mean f̂(S), so by Hoeffding's inequality (Probability.PMF.uniform_abs_sum_div_sub_expect_ge_le) it is off by at least γ with probability at most 2 exp (-m γ² / 2) (UniformLearning.uniform_abs_empiricalCoeff_sub_ge_le). Let N be the number of sets of at most t coordinates, at most (n + 1) ^ t for n coordinates (BitString.card_filter_card_le_le_pow). By the union bound, all N estimates are within γ = √(ε / (2 N)) of their coefficients except with probability at most 2 N exp (-m ε / (4 N)), and then rounding the truncated expansion misclassifies at most a fraction N γ² + W = ε / 2 + W of the points, where W is the Fourier weight of f above degree t (BitString.hammingDist_signRound_sum_mul_chi_div_le, by rounding to the sign as in O'Donnell, Proposition 3.31). So if W ≤ ε / 2, the hypothesis has error above ε with probability at most 2 N exp (-m ε / (4 N)) (UniformLearning.uniform_lt_uniformError_lowDegreeHypothesis_le), which is at most δ once m ≥ (4 N / ε) log (2 N / δ) (UniformLearning.lowDegreeLearner_learns). The whole argument is O'Donnell, Theorem 3.29 for the family of sets of at most t coordinates.

Cost. The algorithm uses m examples, computes N empirical coefficients, each an average of m characters χ_S(x_j) of sets of at most t coordinates, so O (N m t) arithmetic operations on the examples, and evaluates its hypothesis at a point with O (N t) operations. This count is informal: the running time is not certified by a machine model here, and the theorems below bound only the number of examples.

Main definitions #

Main results #

References #

The algorithm #

source
noncomputable def Cslib.MachineLearning.UniformLearning.empiricalCoeff {ι : Type u_1} {m : ℕ} (e : PACLearning.LabeledSample (ι → Bool) Bool m) (S : Finset ι) :
ℝ

The empirical Fourier coefficient on S of a sample of labelled examples (x_j, y_j): the average of y_j χ_S(x_j) over the examples, reading the labels as signs.

Instances For
    source
    noncomputable def Cslib.MachineLearning.UniformLearning.lowDegreeHypothesis {ι : Type u_1} {m : ℕ} [Fintype ι] (t : ℕ) (e : PACLearning.LabeledSample (ι → Bool) Bool m) :
    (ι → Bool) → Bool

    The hypothesis of the low-degree algorithm of degree t: the sign of the empirical Fourier expansion ∑_{#S ≤ t} c̃(S) χ_S truncated at degree t.

    Instances For
      source
      noncomputable def Cslib.MachineLearning.UniformLearning.lowDegreeLearner (ι : Type u_1) [Fintype ι] (t m : ℕ) :
      PACLearning.Learner (ι → Bool) Bool m

      The low-degree algorithm of degree t from m examples: estimate the Fourier coefficients on the sets of at most t coordinates empirically, and output the sign of the truncated expansion. It is a deterministic learner.

      Instances For
        source
        theorem Cslib.MachineLearning.UniformLearning.uniform_abs_empiricalCoeff_sub_ge_le {ι : Type u_1} {m : ℕ} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (S : Finset ι) (hm : 0 < m) {γ : ℝ} (hγ : 0 ≤ γ) :
        (Probability.PMF.uniformOfFintype (Fin m → ι → Bool)).toOuterMeasure {x : Fin m → ι → Bool | γ ≤ |empiricalCoeff (examples f x) S - BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (f x)) S|} ≤ ENNReal.ofReal (2 * Real.exp (-(↑m * γ ^ 2) / 2))

        Estimating a Fourier coefficient O'Donnell, Proposition 3.30: from m > 0 uniform random examples of f, the empirical coefficient on S is off from f̂(S) by at least γ with probability at most 2 exp (-m γ² / 2), by Hoeffding's inequality.

        The low-degree algorithm #

        source
        theorem Cslib.MachineLearning.UniformLearning.uniform_lt_uniformError_lowDegreeHypothesis_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (t m : ℕ) {ε : ℝ} (hε : 0 ≤ ε) (hf : ∑ S : Finset ι with t < S.card, BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (f x)) S ^ 2 ≤ ε / 2) :
        (Probability.PMF.uniformOfFintype (Fin m → ι → Bool)).toOuterMeasure {x : Fin m → ι → Bool | ε < uniformError f (lowDegreeHypothesis t (examples f x))} ≤ ENNReal.ofReal (2 * ↑{S : Finset ι | S.card ≤ t}.card * Real.exp (-(↑m * ε) / (4 * ↑{S : Finset ι | S.card ≤ t}.card)))

        The failure probability of the low-degree algorithm. If the Fourier weight of f, read as signs, on the sets of more than t coordinates is at most ε / 2, then from m uniform random examples the low-degree hypothesis of degree t has error above ε with probability at most 2 N exp (-m ε / (4 N)), where N is the number of sets of at most t coordinates.

        source
        theorem Cslib.MachineLearning.UniformLearning.lowDegreeLearner_learns {ι : Type u_1} [Fintype ι] [DecidableEq ι] {t m : ℕ} {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (hm : 4 * ↑{S : Finset ι | S.card ≤ t}.card / ε * Real.log (2 * ↑{S : Finset ι | S.card ≤ t}.card / δ) ≤ ↑m) {C : PACLearning.ConceptClass (ι → Bool) Bool} (hC : ∀ f ∈ C, ∑ S : Finset ι with t < S.card, BitString.fourierCoeff (fun (x : ι → Bool) => BitString.signVal (f x)) S ^ 2 ≤ ε / 2) :
        Learns (lowDegreeLearner ι t m) C ε δ

        The low-degree algorithm [LMN93], O'Donnell, Section 3.4: let N be the number of sets of at most t coordinates (at most (n + 1) ^ t, BitString.card_filter_card_le_le_pow). The low-degree algorithm of degree t from m ≥ (4 N / ε) log (2 N / δ) uniform random examples learns, with error ε and confidence 1 - δ, every class of Boolean functions whose Fourier weight, read as signs, on the sets of more than t coordinates is at most ε / 2.