Lipschitz constants for the MLP softmax-CE loss — descent through the ReLU kinks #
SgdDescentLinear discharged sgd_descends' smoothness hypothesis for the
Chapter-1 linear net. This file extends the discharge through the Chapter-2
MLP (dense → relu → dense → relu → dense), layer by layer:
Output layer
W₂— free. The top dense layer sees the loss with no ReLU in between, so its descent statement IS the linear one at the hidden activationa₁(mlp_output_sgd_descends=linear_sgd_descendsatx := a₁).Hidden layer
W₁— the genuinely new piece. The chain to the loss crosses one ReLU kink, so the loss-of-W₁map is only piecewise smooth. The key is the margin hypothesisa·D < |z₁ⱼ|(stepℓ1-radiusD, activations bounded bya): the parameter step then cannot flip any ReLU sign, the masks FREEZE along the whole segment (sign_stable_of_close), and on the frozen-mask region the same elementary route as the linear case (logit drift → softmax ratio sandwich → γ-form) yields the explicit segment-Lipschitz constant2·d₃·w₂²·a²/(1 − 2·w₂·a·D)(mlp_hidden_loss_grad_lipschitz). This is the descent-side twin ofFloatBridge's quantitative ReLU marginez < |zᵢ|: there the rounding must not flip a mask, here the step.Input layer
W₀— two frozen masks. Same shape, one more dense+ReLU crossing; the constant picks up theℓ1→ℓ1operator factord₂·w₁of the middle layer:2·d₃·d₂²·w₁²·w₂²·a²/(1 − 2·d₂·w₁·w₂·a·D)(mlp_input_loss_grad_lipschitz).
The capstones mlp_hidden_sgd_descends / mlp_input_sgd_descends mirror
linear_sgd_descends: an η-accurate gradient oracle (the float budgets),
the margin(s) at the step radius, the small-step condition, and the two
dominance conditions ⇒ one inexact SGD step on that layer's weights
provably decreases the cross-entropy loss by ≥ lr·‖∇L‖₂²/2. Every
hypothesis is checkable arithmetic at a concrete point; smoothness is
proven, not assumed. Bias columns are the same argument with the layer
input replaced by the constant 1 and are omitted. The joint all-layers
step (every parameter moving at once, logits no longer affine in the moving
parameters) is the remaining open rung.
ReLU is entrywise 1-Lipschitz. FloatBridge.lean proves the same fact for
the rounded net (relu exact-in-float); this is the ℝ-side workhorse
that lets forward drift pass through a kinked layer unamplified.
The ℓ1 mass of a flattened weight perturbation, summed column by
column, is the total ℓ1 mass — finProdFinEquiv partitions the
flat index set into the columns.
The dense pre-activation difference under a weight perturbation, exactly:
column j only sees the column-j slice of the perturbation.
Column-refined drift: the column-j pre-activation moves by at most
a times the column-j ℓ1 mass (not the total mass — this is what
keeps the hidden-layer Lipschitz constant width-free).
The margin keeps the pre-activation off the kink along the whole
segment. With the step's ℓ1 mass at most D and inputs bounded by
a, the pre-activation drifts by at most a·D — strictly inside the
margin — so every point of [v, v + e] is off the kink with the
original sign.
Loss input-gradient through one ReLU — at an off-kink point the
chain picks up the mask: ∂(CE ∘ dense W₂ ∘ relu)/∂zⱼ = relu'(zⱼ)·∑ₖ W₂ⱼₖ·(softmax − onehot)ₖ. The pdiv-level form of the
cotangent mlpCotOut1 delivers (cf. mlpCotOut1_denote).
One inexact SGD step on the MLP's output weights provably decreases
the cross-entropy loss — for free. The top dense layer sits directly
below the softmax-CE loss with no ReLU in between, so the loss-of-W₂
map IS the linear net's loss at the hidden activation
a₁ = relu(dense W₁ b₁ (relu(dense W₀ b₀ x))): this is
linear_sgd_descends instantiated there. No margin needed — the output
layer never crosses a kink.
Loss input-gradient through the relu→dense→relu chain — the
two-mask closed form relu'(z₀ⱼ)·∑ₗ W₁ⱼₗ·relu'(z₁ₗ)·∑ₖ W₂ₗₖ·(softmax − onehot)ₖ at a point with both pre-activations off the kinks. The
pdiv-level form of the deepest cotangent mlpCotOut0 delivers
(cf. mlpCotOut0_denote).
The loss-of-W₀ map is differentiable wherever both pre-activations
are off the kinks.
Closed form of the input-layer loss gradient at any two-margin
point: ∂L/∂W₀_{ij} = xᵢ·relu'(z₀ⱼ)·∑ₗ W₁ⱼₗ·relu'(z₁ₗ)·∑ₖ W₂ₗₖ· (softmax − onehot)ₖ — the deepest fold (mlp_input_total_loss_grad)
with both pdiv factors collapsed. The input-layer peer of
linear_loss_gradAt.
The input-layer logit drift: through two dense layers and two
1-Lipschitz ReLUs, a weight perturbation of ℓ1 mass ‖e‖₁ moves every
logit by at most w₂·d₂·w₁·a·‖e‖₁. The middle layer contributes its
ℓ1→ℓ1 operator factor d₂·w₁ — unlike the first hop, the perturbation
arriving at layer 1 is no longer column-structured.
The layer-1 margin keeps the middle pre-activation off the kink along
the segment: the perturbation arrives through one dense + ReLU, so the
drift is at most w₁·a·D — the layer-1 analogue of
margin_keeps_offkink.
Segment-Lipschitz gradient for the input-layer loss, explicit
constant. Under both margins (neither ReLU layer's sign pattern can
change along the step) and the small-step condition, the gradient
entries drift by at most
(2·d₃·d₂²·w₁²·w₂²·a²/(1−2·w₂·d₂·w₁·a·D))·(t·D). The input-layer peer
of mlp_hidden_loss_grad_lipschitz; the extra d₂·w₁ is the middle
layer's ℓ1→ℓ1 operator factor.
One inexact SGD step on the MLP's input weights provably decreases
the cross-entropy loss. The deepest descent capstone: both ReLU
layers' margins at the step radius D = lr·(‖∇L‖₁ + d₀d₁·η) freeze the
masks, the segment-Lipschitz constant
C = 2·d₃·d₂²·w₁²·w₂²·a²/(1−2·w₂·d₂·w₁·a·D) is proven, and the loss
drops by ≥ lr·‖∇L‖₂²/2. Remaining hypotheses are checkable
arithmetic. The input-layer peer of linear_sgd_descends; with this,
every MLP weight layer's descent statement is discharged.
One binary32 SGD step on the MLP's output weights provably decreases the
cross-entropy loss — with NO abstract gradient-accuracy parameter. The
output-layer rung of the η-composition (Item D / G1 for the MLP). Since the
top dense layer sits directly below the softmax-CE loss with no ReLU between,
the loss-of-W₂ map is the linear net's loss at the hidden activation
a₁ = relu(dense W₁ b₁ (relu(dense W₀ b₀ x))) — so this is
linear_float_sgd_descends instantiated there. The gradient is the actual
binary32 output-layer gradient M.linearFloatGrad W₂ b₂ a₁ and its accuracy
η = mulErr u a 1 0 (cotErr …) is proven (by linear_grad_close, inside
the linear theorem), not assumed. No margin needed — the output layer never
crosses a kink.
The hidden/input rungs (mlp_{hidden,input}_sgd_descends) still take an
abstract η: their float gradients run back through the ReLU masks and the
W₂-cotangent fan-in, so the η-composition there needs a per-layer
float-backward grad-close (a mlp_w{1,0}_grad_close) under the descent
margins — the joint-step refinement flagged at the top of this file, left
open.
The binary32 hidden-layer (W₁) gradient is within an explicit budget of
the certified one, per entry — the float-backward grad-close that the
hidden η-composition needs. With the layer-1 input activation a₀ frozen
exact (the descent moves only W₁), the rendered trainer computes the
W₁ gradient as fl(a₀ᵢ · c̃₁ⱼ) where the float layer-1 cotangent
c̃₁ = mask(z̃₁, W₂ᵀ·c̃₂) reads the float pre-activation z̃₁ = M.dense W₁ b₁ a₀
and the float softmax−onehot head c̃₂ at the float logits. This is within
mulErr M.u a … 0 (layerBudget … (cotErr …)) of the certified
a₀ᵢ · mask(z₁, W₂ᵀ·(softmax−onehot))ⱼ (= mlp_hidden_loss_gradAt), built
from three reusable closes: the head (softmax_ce_cot_close, accuracy
cotErr), the masked W₂ᵀ contraction (cot_step_close, under the
quantitative margin E₁ < |z₁ⱼ| — forward rounding must not flip the
layer-1 ReLU), and the final input multiply (mul_close, with the exact
a₀ operand, ea = 0, exactly as the linear grad-close).
The binary32 hidden-layer (W₁) gradient of the MLP loss, exactly
as the rendered trainer computes it (with the layer-1 input activation
a₀ frozen exact): fl(a₀ᵢ · c̃₁ⱼ) where the float layer-1 cotangent
c̃₁ = mask(z̃₁, W₂ᵀ·c̃₂) reads the float pre-activation
z̃₁ = M.dense W₁ b₁ a₀ and the float softmax−onehot head c̃₂ at the
float logits. Flattened to the Vec (d₁*d₂) parameter layout that
gradAt/mlp_hidden_sgd_descends use. The hidden-layer peer of
linearFloatGrad.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A masked Wᵀ contraction in if-then-else form equals the reluMask
form. (relu'(zₗ))·∑ₖ Wₗₖ·cₖ = reluMask z (Wᵀ·c) l — the per-step
identity behind the gradAt↔reluMask bridges (mlp_hidden_/
mlp_input_loss_gradAt_reluMask): one ReLU-sign case split + mul_comm
(the transpose dense (fun j i' => W i' j) 0 c reads ∑ₖ cₖ·Wₗₖ).
The binary32 input-layer (W₀) gradient of the MLP loss, exactly as
the rendered trainer computes it (x the exact input): fl(xᵢ · c̃₀ⱼ)
where the float layer-0 cotangent c̃₀ = mask(z̃₀, W₁ᵀ·c̃₁) reads the float
layer-1 cotangent c̃₁ = mask(z̃₁, W₂ᵀ·c̃₂) and the float softmax−onehot head
c̃₂, all at the float pre-activations. Flattened to the Vec (d₀*d₁)
parameter layout. The two-mask peer of mlpHiddenFloatGrad.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The certified input-layer loss gradient, in the nested reluMask form
that mlp_w0_grad_close bounds against. At an off-kink point (both
hz0, hz1), mlp_input_loss_gradAt's two-mask if-then-else closed form
equals xᵢ · reluMask(z₀, W₁ᵀ·reluMask(z₁, W₂ᵀ·(softmax−onehot)))ⱼ. Two
applications of reluMask_dense_transpose_eq (inner W₂ᵀ then outer W₁ᵀ),
fired by simp_rw.
The binary32 input-layer (W₀) gradient is within an explicit budget of
the certified one, per entry — the float-backward grad-close for the
deepest rung. With x exact, the rendered trainer computes the W₀
gradient fl(xᵢ·c̃₀ⱼ), c̃₀ = mask(z̃₀, W₁ᵀ·mask(z̃₁, W₂ᵀ·c̃₂)) from the float
softmax−onehot head c̃₂ back through two ReLU masks. This is within
mulErr … 0 (layerBudget … (layerBudget … (cotErr …))) of the certified
xᵢ·mask(z₀, W₁ᵀ·mask(z₁, W₂ᵀ·(softmax−onehot)))ⱼ (= mlp_input_loss_gradAt,
via mlp_input_loss_gradAt_reluMask). Built like mlp_w1_grad_close with
one more cot_step_close: head (softmax_ce_cot_close), masked W₂ᵀ
contraction (cot_step_close, under the layer-1 margin E₁ < |z₁|),
masked W₁ᵀ contraction (cot_step_close, under the layer-0 margin
E₀ < |z₀|), final exact-x multiply (mul_close, ea = 0).
One binary32 SGD step on the MLP's input weights provably decreases the
cross-entropy loss — with NO abstract gradient-accuracy parameter. The
input-layer rung of the η-composition (Item D / G1 for the MLP), one mask
deeper than the hidden rung. The gradient is the actual binary32 W₀
gradient M.mlpInputFloatGrad …, and its accuracy is proven by
mlp_w0_grad_close (via the nested reluMask↔gradAt bridge
mlp_input_loss_gradAt_reluMask), not assumed.
Four margins are carried as hypotheses (the honest first cut): the two
rounding margins hmargin0_round/hmargin1_round (forward rounding
must not flip either ReLU — the grad-close preconditions) and the two
step margins hmargin0_step/hmargin1_step (the parameter step must
not flip either along the segment — the smoothness preconditions). With
this, "one binary32 SGD step on any single MLP weight layer provably
decreases the loss" is closed for all three layers.