Perceptron

DefinitionSign of a Boolean label#✓fully proved

For a commutative ring \(K\), the sign of a Boolean label \(y\) is the element \(\operatorname{sign}(y) \in K\) equal to \(1\) if \(y\) is true and to \(-1\) if \(y\) is false.

def sign (y : Bool) : K := if y then 1 else -1

Used by 17

Used byUnrolling the weights · Normalizer of a boosting round · The normalizer of a round is \(2\sqrt{\varepsilon(1 - \varepsilon)}\) · AdaBoost reweighting · AdaBoost's combined score · Training error of AdaBoost · AdaBoost drives the training error down exponentially · The training error is at most the product of the normalizers · The Freund–Schapire bound on AdaBoost's training error · A mistake-free pass classifies every example · Novikoff's mistake bound over an ordered field · Novikoff's perceptron mistake bound · The starting mistake count only shifts the final count · Invariant of the perceptron run · Perceptron step · Trained weights classify every example · The perceptron converges

DefinitionPerceptron step#✓fully proved

Let \(K\) be a commutative ring with a linear order, \(\iota\) a finite type, and \(v \cdot w = \sum_{i \in \iota} v_i w_i\) the dot product on \(K^\iota\). One perceptron step takes a state \((w, m)\), made of weights \(w \in K^\iota\) and a mistake count \(m \in \mathbb{N}\), and a labelled example \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean. If \(\operatorname{sign}(y)\,(w \cdot x) \le 0\), that is, \(w\) does not classify the example strictly correctly, the step returns \((w + \operatorname{sign}(y)\,x,\ m + 1)\) and counts a mistake; otherwise it returns \((w, m)\) unchanged.

def step (s : (ι → K) × ℕ) (e : (ι → K) × Bool) : (ι → K) × ℕ :=
  if (sign e.2 : K) * (s.1 ⬝ᵥ e.1) ≤ 0 then (s.1 + (sign e.2 : K) • e.1, s.2 + 1) else s

Uses 1 · Used by 5

Statement usesSign of a Boolean label

Used byA mistake-free pass classifies every example · Every failed training pass adds a mistake · Perceptron run · The starting mistake count only shifts the final count · Invariant of the perceptron run

DefinitionPerceptron run#✓fully proved

Let \(K\) be a commutative ring with a linear order and \(\iota\) a finite type. The run of the perceptron over a finite list \(L\) of labelled examples \((x, y)\), with \(x \in K^\iota\) and \(y\) a Boolean, from weights \(w \in K^\iota\) with \(m \in \mathbb{N}\) mistakes so far is the pair of final weights and final mistake count obtained by applying the perceptron step to each example of \(L\) in order, starting from the state \((w, m)\).

def run (w : ι → K) (m : ℕ) (xs : List ((ι → K) × Bool)) : (ι → K) × ℕ :=
  xs.foldl step (w, m)

Uses 1 · Used by 9

Statement usesPerceptron step

Used byA mistake-free pass classifies every example · Every failed training pass adds a mistake · Novikoff's mistake bound over an ordered field · Novikoff's perceptron mistake bound · The starting mistake count only shifts the final count · Invariant of the perceptron run · Perceptron training · Trained weights classify every example · The perceptron converges

DefinitionPerceptron training#✓fully proved

Given a finite list \(D\) of labelled examples, a number \(n\) of passes and weights \(w\), training returns nothing when \(n = 0\). When \(n = m + 1\), it runs one perceptron pass over \(D\) from \(w\) with mistake count \(0\); if that pass makes no mistake it returns \(w\), and otherwise it trains on \(D\) for \(m\) passes from the weights the pass produced. So training repeats passes until one makes no mistake, for at most \(n\) passes, and returns the weights of that pass, or nothing if every pass made a mistake.

def train (xs : List ((ι → K) × Bool)) : ℕ → (ι → K) → Option (ι → K)
  | 0, _ => none
  | n + 1, w =>
      let r := run w 0 xs
      if r.2 = 0 then some w else train xs n r.1

Uses 1 · Used by 3

Statement usesPerceptron run

Used byEvery failed training pass adds a mistake · Trained weights classify every example · The perceptron converges

12 fully proved

Bookkeeping

TheoremThe starting mistake count only shifts the final count#✓fully proved

Let \(K\) be a commutative ring with a linear order and \(\iota\) a finite type, and let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean. For all weights \(w \in K^\iota\) and every natural number \(m\), the perceptron run over \(L\) from \(w\) with \(m\) mistakes so far ends with the same weights as the run from \(w\) with \(0\) mistakes so far, and with mistake count \(m + c\), where \(c\) is the final mistake count of the run from \(w\) with \(0\) mistakes so far.

theorem run_eq (xs : List ((ι → K) × Bool)) :
    ∀ (w : ι → K) (m : ℕ), run w m xs = ((run w 0 xs).1, m + (run w 0 xs).2)

Uses 3 · Used by 2

Statement usesPerceptron run

Proof usesSign of a Boolean label · Perceptron step

Used byA mistake-free pass classifies every example · Every failed training pass adds a mistake

TheoremA mistake-free pass classifies every example#✓fully proved

Let \(K\) be a commutative ring with a linear order, \(\iota\) a finite type, and \(v \cdot w = \sum_{i \in \iota} v_i w_i\) the dot product on \(K^\iota\). Let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean, and let \(w \in K^\iota\). If the perceptron run over \(L\) from weights \(w\) with \(0\) mistakes so far ends with mistake count \(0\), then every example \((x, y)\) in \(L\) satisfies \(0 < \operatorname{sign}(y)\,(w \cdot x)\).

theorem classifies_of_run_eq_zero (xs : List ((ι → K) × Bool)) :
    ∀ w : ι → K, (run w 0 xs).2 = 0 → ∀ e ∈ xs, 0 < sign e.2 * (w ⬝ᵥ e.1)

Uses 4 · Used by 1

Statement usesPerceptron run · Sign of a Boolean label

Proof usesThe starting mistake count only shifts the final count · Perceptron step

Used byTrained weights classify every example

Novikoff's mistake bound

TheoremInvariant of the perceptron run#✓fully proved

Let \(K\) be a linearly ordered commutative ring, \(\iota\) a finite type, \(v \cdot w = \sum_{i \in \iota} v_i w_i\) the dot product on \(K^\iota\), \(u \in K^\iota\) and \(\gamma, R \in K\). Let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean, such that every example in \(L\) satisfies \(\gamma \le \operatorname{sign}(y)\,(u \cdot x)\) and \(x \cdot x \le R^2\). Let \(w \in K^\iota\) and \(m \in \mathbb{N}\) satisfy \(m \gamma \le u \cdot w\) and \(w \cdot w \le m R^2\), and let the perceptron run over \(L\) from \(w\) with \(m\) mistakes so far end with weights \(w'\) and mistake count \(m'\). Then \(m' \gamma \le u \cdot w'\) and \(w' \cdot w' \le m' R^2\).

theorem run_invariant (xs : List ((ι → K) × Bool))
    (hsep : ∀ e ∈ xs, γ ≤ sign e.2 * (u ⬝ᵥ e.1)) (hR : ∀ e ∈ xs, e.1 ⬝ᵥ e.1 ≤ R ^ 2) :
    ∀ (w : ι → K) (m : ℕ), (m : K) * γ ≤ u ⬝ᵥ w → w ⬝ᵥ w ≤ m * R ^ 2 →
      ((run w m xs).2 : K) * γ ≤ u ⬝ᵥ (run w m xs).1 ∧
        (run w m xs).1 ⬝ᵥ (run w m xs).1 ≤ (run w m xs).2 * R ^ 2

Uses 3 · Used by 1

Statement usesPerceptron run · Sign of a Boolean label

Proof usesPerceptron step

Used byNovikoff's perceptron mistake bound

TheoremNovikoff's perceptron mistake bound#✓fully proved

Let \(K\) be a linearly ordered commutative ring, \(\iota\) a finite type, \(v \cdot w = \sum_{i \in \iota} v_i w_i\) the dot product on \(K^\iota\), \(u \in K^\iota\), and \(\gamma, R \in K\) with \(\gamma > 0\). Let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean, such that every example in \(L\) satisfies \(\gamma \le \operatorname{sign}(y)\,(u \cdot x)\) and \(x \cdot x \le R^2\). If the perceptron run over \(L\) from the zero weights with \(0\) mistakes so far ends with mistake count \(k\), then \(k \gamma^2 \le (u \cdot u) R^2\).

theorem mistakes_mul_sq_le (xs : List ((ι → K) × Bool))
    (hsep : ∀ e ∈ xs, γ ≤ sign e.2 * (u ⬝ᵥ e.1)) (hR : ∀ e ∈ xs, e.1 ⬝ᵥ e.1 ≤ R ^ 2)
    (hγ : 0 < γ) : ((run 0 0 xs).2 : K) * γ ^ 2 ≤ (u ⬝ᵥ u) * R ^ 2

Uses 3 · Used by 2

Statement usesPerceptron run · Sign of a Boolean label

Proof usesInvariant of the perceptron run

Used byNovikoff's mistake bound over an ordered field · The perceptron converges

TheoremNovikoff's mistake bound over an ordered field#✓fully proved

Let \(F\) be a linearly ordered field, \(\iota\) a finite type, \(v \cdot w = \sum_{i \in \iota} v_i w_i\) the dot product on \(F^\iota\), \(u \in F^\iota\), and \(\gamma, R \in F\) with \(\gamma > 0\). Let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in F^\iota\) and \(y\) a Boolean, such that every example in \(L\) satisfies \(\gamma \le \operatorname{sign}(y)\,(u \cdot x)\) and \(x \cdot x \le R^2\). If the perceptron run over \(L\) from the zero weights with \(0\) mistakes so far ends with mistake count \(k\), then \(k \le (u \cdot u) R^2 / \gamma^2\); for a unit vector \(u\) this is the textbook bound \(R^2 / \gamma^2\).

theorem mistakes_le_div {F : Type*} [Field F] [LinearOrder F] [IsStrictOrderedRing F]
    {u : ι → F} {γ R : F} (xs : List ((ι → F) × Bool))
    (hsep : ∀ e ∈ xs, γ ≤ sign e.2 * (u ⬝ᵥ e.1)) (hR : ∀ e ∈ xs, e.1 ⬝ᵥ e.1 ≤ R ^ 2)
    (hγ : 0 < γ) : ((run 0 0 xs).2 : F) ≤ (u ⬝ᵥ u) * R ^ 2 / γ ^ 2

Uses 3

Statement usesPerceptron run · Sign of a Boolean label

Proof usesNovikoff's perceptron mistake bound

Training until a pass makes no mistake

TheoremTrained weights classify every example#✓fully proved

Let \(K\) be a commutative ring with a linear order, \(\iota\) a finite type, and \(v \cdot w = \sum_{i \in \iota} v_i w_i\) the dot product on \(K^\iota\). Let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean. For every natural number \(n\) and all weights \(w, v \in K^\iota\), if training on \(L\) from \(w\) with at most \(n\) passes returns \(v\), then every example \((x, y)\) in \(L\) satisfies \(0 < \operatorname{sign}(y)\,(v \cdot x)\).

theorem train_classifies (xs : List ((ι → K) × Bool)) :
    ∀ (n : ℕ) (w v : ι → K), train xs n w = some v → ∀ e ∈ xs, 0 < sign e.2 * (v ⬝ᵥ e.1)

Uses 4 · Used by 1

Statement usesSign of a Boolean label · Perceptron training

Proof usesA mistake-free pass classifies every example · Perceptron run

Used byThe perceptron converges

TheoremEvery failed training pass adds a mistake#✓fully proved

Let \(K\) be a commutative ring with a linear order and \(\iota\) a finite type, and let \(L\) be a finite list of labelled examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean. For every natural number \(n\) and all weights \(w \in K^\iota\), if training on \(L\) from \(w\) with at most \(n\) passes returns no weights, then the perceptron run from \(w\) with \(0\) mistakes so far over the concatenation of \(n\) copies of \(L\) ends with a mistake count of at least \(n\).

theorem le_run_of_train_eq_none (xs : List ((ι → K) × Bool)) :
    ∀ (n : ℕ) (w : ι → K), train xs n w = none →
      n ≤ (run w 0 (List.replicate n xs).flatten).2

Uses 4 · Used by 1

Statement usesPerceptron run · Perceptron training

Proof usesThe starting mistake count only shifts the final count · Perceptron step

Used byThe perceptron converges

TheoremThe perceptron converges#✓fully proved

Let \(K\) be a linearly ordered commutative ring, let \(\iota\) be a finite index type, write \(a \cdot b = \sum_{j \in \iota} a_j b_j\) for \(a, b \in K^\iota\), and let the label sign \(s(y)\) be \(1\) if the Boolean \(y\) is true and \(-1\) otherwise. Let \(D\) be a finite list of examples \((x, y)\) with \(x \in K^\iota\) and \(y\) a Boolean, and let \(u \in K^\iota\) and \(\gamma, R \in K\) with \(\gamma > 0\) be such that every example \((x, y)\) of \(D\) satisfies \(\gamma \le s(y)\,(u \cdot x)\) and \(x \cdot x \le R^2\). Then for every natural number \(n\) with \((u \cdot u) R^2 < n \gamma^2\), perceptron training on \(D\) from the zero weights with at most \(n\) passes returns some weights \(v\), and \(0 < s(y)\,(v \cdot x)\) for every example \((x, y)\) of \(D\).

theorem train_converges (xs : List ((ι → K) × Bool))
    (hsep : ∀ e ∈ xs, γ ≤ sign e.2 * (u ⬝ᵥ e.1)) (hR : ∀ e ∈ xs, e.1 ⬝ᵥ e.1 ≤ R ^ 2)
    (hγ : 0 < γ) {n : ℕ} (hn : (u ⬝ᵥ u) * R ^ 2 < n * γ ^ 2) :
    ∃ v, train xs n 0 = some v ∧ ∀ e ∈ xs, 0 < sign e.2 * (v ⬝ᵥ e.1)

Uses 6

Statement usesSign of a Boolean label · Perceptron training

Proof usesEvery failed training pass adds a mistake · Novikoff's perceptron mistake bound · Perceptron run · Trained weights classify every example

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.