Backpropagation
StructureFeedforward network#✓fully proved
Given layer widths \(d : \mathbb{N} \to \mathbb{N}\), a feedforward network with widths \(d\) is a sequence of arbitrary maps \(f_k : \mathbb{R}^{d(k)} \to \mathbb{R}^{d(k+1)}\), one for each \(k \in \mathbb{N}\), where \(f_k\) is the map computed by layer \(k\) and \(\mathbb{R}^n\) carries its Euclidean structure.
structure Net (d : ℕ → ℕ) where
/-- The map computed by layer `k`. -/
layer : (k : ℕ) → EuclideanSpace ℝ (Fin (d k)) → EuclideanSpace ℝ (Fin (d (k + 1)))Used by 11
DefinitionThe forward pass#✓fully proved
For a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, the forward pass through the first \(n\) layers is the map \(N_n : \mathbb{R}^{d_0} \to \mathbb{R}^{d_n}\) given by \(N_0(x) = x\) and \(N_{n+1}(x) = f_n(N_n(x))\), that is, \(N_n = f_{n-1} \circ \cdots \circ f_0\).
def Net.forward : (n : ℕ) → EuclideanSpace ℝ (Fin (d 0)) → EuclideanSpace ℝ (Fin (d n))
| 0, x => x
| n + 1, x => N.layer n (forward n x)Uses 1 · Used by 8
DefinitionThe backward pass#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, let \(x \in \mathbb{R}^{d_0}\) be an input, and write \(a_k \in \mathbb{R}^{d_k}\) for the forward pass of \(x\) through the first \(k\) layers. For each \(n \in \mathbb{N}\), the backward pass at \(x\) sends a vector \(\delta \in \mathbb{R}^{d_n}\) to \(B_n(\delta) \in \mathbb{R}^{d_0}\), defined by \(B_0(\delta) = \delta\) and \(B_{n+1}(\delta) = B_n(Df_n(a_n)^* \, \delta)\), where \(Df_n(a_n)\) is the Fréchet derivative of \(f_n\) at \(a_n\) (taken to be \(0\) if \(f_n\) is not differentiable there) and \(^*\) denotes the adjoint. Thus \(B_n(\delta) = Df_0(a_0)^* \cdots Df_{n-1}(a_{n-1})^* \, \delta\): the adjoints of the layer Jacobians are applied from the last layer to the first.
noncomputable def Net.backward (x : EuclideanSpace ℝ (Fin (d 0))) :
(n : ℕ) → EuclideanSpace ℝ (Fin (d n)) → EuclideanSpace ℝ (Fin (d 0))
| 0, δ => δ
| n + 1, δ => backward x n (adjoint (fderiv ℝ (N.layer n) (N.forward n x)) δ)Uses 2 · Used by 3
DefinitionDifferentiability along the forward pass#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, let \(x \in \mathbb{R}^{d_0}\) and \(n \in \mathbb{N}\), and write \(a_j \in \mathbb{R}^{d_j}\) for the forward pass of \(x\) through the first \(j\) layers. The network is differentiable along the forward pass of \(x\) through its first \(n\) layers when \(f_j\) is differentiable at \(a_j\) for every \(j < n\).
def Net.DiffAlong (x : EuclideanSpace ℝ (Fin (d 0))) (n : ℕ) : Prop :=
∀ j < n, DifferentiableAt ℝ (N.layer j) (N.forward j x)Uses 2 · Used by 5
TheoremDifferentiable layers are differentiable along every forward pass#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces. If every \(f_k\) is differentiable on all of \(\mathbb{R}^{d_k}\), then for every input \(x \in \mathbb{R}^{d_0}\) and every \(n \in \mathbb{N}\), the layer \(f_j\) is differentiable at the forward pass of \(x\) through the first \(j\) layers for every \(j < n\).
theorem Net.diffAlong_of_differentiable (hN : ∀ k, Differentiable ℝ (N.layer k))
(x : EuclideanSpace ℝ (Fin (d 0))) (n : ℕ) : N.DiffAlong x nUses 3
TheoremDifferentiability of the forward pass#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, let \(x \in \mathbb{R}^{d_0}\) and \(n \in \mathbb{N}\), and write \(N_j : \mathbb{R}^{d_0} \to \mathbb{R}^{d_j}\) for the forward pass through the first \(j\) layers. If \(f_j\) is differentiable at \(N_j(x)\) for every \(j < n\), then \(N_n\) is differentiable at \(x\).
theorem Net.differentiableAt_forward (x : EuclideanSpace ℝ (Fin (d 0))) :
∀ n, N.DiffAlong x n → DifferentiableAt ℝ (N.forward n) xTheoremThe backward pass is the vector-Jacobian product#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, let \(x \in \mathbb{R}^{d_0}\) and \(n \in \mathbb{N}\), and write \(N_j : \mathbb{R}^{d_0} \to \mathbb{R}^{d_j}\) for the forward pass through the first \(j\) layers. If \(f_j\) is differentiable at \(N_j(x)\) for every \(j < n\), then for every \(\delta \in \mathbb{R}^{d_n}\) the backward pass from \(\delta\) at input \(x\) through the first \(n\) layers equals \(DN_n(x)^* \, \delta\), where \(DN_n(x)\) is the Fréchet derivative of \(N_n\) at \(x\) and \(^*\) denotes the adjoint.
theorem Net.backward_eq (x : EuclideanSpace ℝ (Fin (d 0))) :
∀ (n : ℕ), N.DiffAlong x n → ∀ δ : EuclideanSpace ℝ (Fin (d n)),
N.backward x n δ = adjoint (fderiv ℝ (N.forward n) x) δUses 5 · Used by 1
TheoremBackpropagation computes the input gradient#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, let \(x \in \mathbb{R}^{d_0}\) and \(n \in \mathbb{N}\), and write \(N_j\) for the forward pass through the first \(j\) layers. Assume that \(f_j\) is differentiable at \(N_j(x)\) for every \(j < n\), and let \(\ell : \mathbb{R}^{d_n} \to \mathbb{R}\) be differentiable at \(N_n(x)\). Then \(\nabla(\ell \circ N_n)(x)\) is the backward pass of \(\nabla \ell(N_n(x))\) at input \(x\) through the first \(n\) layers, that is, \(\nabla(\ell \circ N_n)(x) = Df_0(N_0(x))^* \cdots Df_{n-1}(N_{n-1}(x))^* \, \nabla \ell(N_n(x))\), where \(Df_j(N_j(x))\) is the Fréchet derivative of \(f_j\) at \(N_j(x)\) and \(^*\) denotes the adjoint.
theorem gradient_comp_forward {n : ℕ} (ℓ : EuclideanSpace ℝ (Fin (d n)) → ℝ)
(x : EuclideanSpace ℝ (Fin (d 0))) (hN : N.DiffAlong x n)
(hℓ : DifferentiableAt ℝ ℓ (N.forward n x)) :
∇ (ℓ ∘ N.forward n) x = N.backward x n (∇ ℓ (N.forward n x))Uses 7 · Used by 1
DefinitionShifted network#✓fully proved
For a feedforward network \(N\) with layer widths \(d\) and a natural number \(j\), the shifted network has layer widths \(i \mapsto d(j + i)\), and its layer \(i\) is layer \(j + i\) of \(N\). It is made of the layers of \(N\) from layer \(j\) on.
def Net.shift (j : ℕ) : Net (fun i => d (j + i)) := ⟨fun i => N.layer (j + i)⟩structure Net (d : ℕ → ℕ) where
/-- The map computed by layer `k`. -/
layer : (k : ℕ) → EuclideanSpace ℝ (Fin (d k)) → EuclideanSpace ℝ (Fin (d (k + 1)))CSLibExt/MachineLearning/Backpropagation.lean:57
Uses 1 · Used by 2
TheoremSplitting the forward pass#✓fully proved
Let \(N\) be a feedforward network with layers \(f_k : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) between Euclidean spaces, write \(N_n\) for its forward pass through the first \(n\) layers, and for \(j \in \mathbb{N}\) write \(N^{(j)}_m\) for the forward pass through the first \(m\) layers of the shifted network with layers \(f_j, f_{j+1}, \dots\). Then for all \(j, m \in \mathbb{N}\) and \(x \in \mathbb{R}^{d_0}\), \(N_{j+m}(x) = N^{(j)}_m(N_j(x))\).
theorem Net.forward_add (j : ℕ) (x : EuclideanSpace ℝ (Fin (d 0))) :
∀ m, N.forward (j + m) x = (N.shift j).forward m (N.forward j x)Uses 3 · Used by 1
StructureParametrized feedforward network#✓fully proved
Given layer widths \(d : \mathbb{N} \to \mathbb{N}\) and parameter dimensions \(p : \mathbb{N} \to \mathbb{N}\), a parametrized network is a sequence of arbitrary maps \(f_k : \mathbb{R}^{p(k)} \times \mathbb{R}^{d(k)} \to \mathbb{R}^{d(k+1)}\), one for each \(k \in \mathbb{N}\): layer \(k\) sends parameters \(\theta \in \mathbb{R}^{p(k)}\) and an input \(x \in \mathbb{R}^{d(k)}\) to \(f_k(\theta, x)\).
structure PNet (d p : ℕ → ℕ) where
/-- The map computed by layer `k` with parameters `θ`. -/
layer : (k : ℕ) → EuclideanSpace ℝ (Fin (p k)) → EuclideanSpace ℝ (Fin (d k)) →
EuclideanSpace ℝ (Fin (d (k + 1)))Used by 2
DefinitionThe network at fixed parameters#✓fully proved
Let \(P\) be a network with parameters whose layer \(k\) is a map \(g_k : \mathbb{R}^{p_k} \times \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\) of the parameters and the input (all spaces Euclidean). For parameters \(\theta = (\theta_k)_{k \in \mathbb{N}}\) with \(\theta_k \in \mathbb{R}^{p_k}\), the network at \(\theta\) is the feedforward network whose layer \(k\) is \(g_k(\theta_k, \cdot) : \mathbb{R}^{d_k} \to \mathbb{R}^{d_{k+1}}\).
def PNet.net (P : PNet d p) (θ : (k : ℕ) → EuclideanSpace ℝ (Fin (p k))) : Net d :=
⟨fun k => P.layer k (θ k)⟩structure PNet (d p : ℕ → ℕ) where
/-- The map computed by layer `k` with parameters `θ`. -/
layer : (k : ℕ) → EuclideanSpace ℝ (Fin (p k)) → EuclideanSpace ℝ (Fin (d k)) →
EuclideanSpace ℝ (Fin (d (k + 1)))CSLibExt/MachineLearning/Backpropagation.lean:131
structure Net (d : ℕ → ℕ) where
/-- The map computed by layer `k`. -/
layer : (k : ℕ) → EuclideanSpace ℝ (Fin (d k)) → EuclideanSpace ℝ (Fin (d (k + 1)))CSLibExt/MachineLearning/Backpropagation.lean:57
Uses 2 · Used by 1
TheoremBackpropagation computes the parameter gradients#✓fully proved
Let \(P\) be a network with parameters whose layer \(i\) is a map \(g_i : \mathbb{R}^{p_i} \times \mathbb{R}^{d_i} \to \mathbb{R}^{d_{i+1}}\) of the parameters and the input (all spaces Euclidean). Fix parameters \(\theta = (\theta_i)_i\) with \(\theta_i \in \mathbb{R}^{p_i}\), let \(N\) be the network with layers \(f_i = g_i(\theta_i, \cdot)\), let \(x \in \mathbb{R}^{d_0}\) and \(k, m \in \mathbb{N}\), set \(L = k + 1 + m\), and write \(a_j\) for the forward pass of \(x\) through the first \(j\) layers of \(N\). Assume that \(f_{k+1+i}\) is differentiable at \(a_{k+1+i}\) for every \(i < m\), that \(h(t) = g_k(t, a_k)\) is differentiable at \(\theta_k\), and that \(\ell : \mathbb{R}^{d_L} \to \mathbb{R}\) is differentiable at \(a_L\). For \(t \in \mathbb{R}^{p_k}\) let \(\Phi(t)\) be the forward pass of \(x\) through the first \(L\) layers of the network obtained by replacing \(\theta_k\) with \(t\). Then
where \(\delta = Df_{k+1}(a_{k+1})^* \cdots Df_{L-1}(a_{L-1})^* \, \nabla \ell(a_L)\) (so \(\delta = \nabla \ell(a_L)\) when \(m = 0\)) is the backward pass of \(\nabla \ell(a_L)\) through layers \(k + 1, \dots, L - 1\) of \(N\), \(D\) denotes the Fréchet derivative and \(^*\) the adjoint.
theorem gradient_param (P : PNet d p) (θ : (k : ℕ) → EuclideanSpace ℝ (Fin (p k)))
(x : EuclideanSpace ℝ (Fin (d 0))) (k m : ℕ)
(hN : ∀ i < m, DifferentiableAt ℝ ((P.net θ).layer (k + 1 + i))
((P.net θ).forward (k + 1 + i) x))
(hk : DifferentiableAt ℝ (fun t => P.layer k t ((P.net θ).forward k x)) (θ k))
(ℓ : EuclideanSpace ℝ (Fin (d (k + 1 + m))) → ℝ)
(hℓ : DifferentiableAt ℝ ℓ ((P.net θ).forward (k + 1 + m) x)) :
∇ (fun t => ℓ ((P.net (Function.update θ k t)).forward (k + 1 + m) x)) (θ k) =
adjoint (fderiv ℝ (fun t => P.layer k t ((P.net θ).forward k x)) (θ k))
(((P.net θ).shift (k + 1)).backward ((P.net θ).forward (k + 1) x) m
(∇ ℓ ((P.net θ).forward (k + 1 + m) x)))structure PNet (d p : ℕ → ℕ) where
/-- The map computed by layer `k` with parameters `θ`. -/
layer : (k : ℕ) → EuclideanSpace ℝ (Fin (p k)) → EuclideanSpace ℝ (Fin (d k)) →
EuclideanSpace ℝ (Fin (d (k + 1)))CSLibExt/MachineLearning/Backpropagation.lean:131
Uses 11
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.