Lipschitz constants for the linear softmax-CE loss #
The missing hypothesis of sgd_descends, discharged for the Chapter-1 net:
the gradient of v ↦ crossEntropy(dense(unflatten v, b, x), label) is
segment-Lipschitz with the explicit constant 2a²/(1 − 2aD) (pixels
bounded by a, step ℓ1-radius D, small-step condition 2aD < 1).
No Hessian appears. The route is the same elementary ratio argument as
FloatBridge.lean's: the loss gradient is xᵢ·(softmax(z)ⱼ − onehotⱼ)
(linear_loss_gradAt, assembled from the suite's certified
lossWeightGrad_eq_sum + pdiv_dense_W), the logits move linearly in the
parameters (dense_unflatten_drift), and FloatModel.softmax_perturb +
the γ-form FloatModel.exp_sub_one_le turn the logit drift into a gradient
drift that is linear in t along the segment — exactly the shape
descent_segment consumes.
linear_sgd_descends is the capstone: an η-accurate gradient oracle
(e.g. the float budgets), the small-step condition, and the two dominance
conditions ⇒ one inexact SGD step on the weights W of the MNIST-linear
classifier, at one example (x, label) with the bias held fixed, decreases
that example's cross-entropy loss by ≥ lr·‖∇L‖₂²/2. The smoothness
hypothesis of sgd_descends is proven here, not assumed; the oracle accuracy,
the small-step condition and the two dominance conditions remain hypotheses.
linear_float_sgd_descends then discharges the oracle accuracy for the
FloatModel binary32 gradient.
Closed form of the linear softmax-CE loss gradient at any parameter
point: ∂L/∂W_{ij} = xᵢ·(softmax(z)ⱼ − onehotⱼ) — the suite's
certified contraction (lossWeightGrad_eq_sum + pdiv_dense_W),
re-expressed through gradAt.
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).
Softmax drift along a segment. Logits that move by at most t·δ (t ∈ [0, 1],
2δ < 1) move every softmax output by at most 2tδ/(1−2δ): softmax_perturb's
e^(2tδ) − 1, the γ-form exp_sub_one_le, then t ≤ 1 in the denominator. The
linear, MLP and CNN segment-Lipschitz lemmas all end in this step.
Segment-Lipschitz gradient for the linear softmax-CE loss, explicit
constant. Under the small-step condition 2aD < 1, the gradient
entries drift by at most (2a²/(1−2aD))·(t·D) along [v, v+d] — the
exact shape descent_segment consumes. The exponential softmax
perturbation is linearized by the γ-form, not the mean value theorem.
The linear classifier's loss as a function of its flattened weights.
Equations
- Proofs.linearLoss b x label w = Proofs.crossEntropy n (Proofs.dense (Proofs.Mat.unflatten w) b x) label
Instances For
One inexact SGD step on the MNIST-linear weights decreases one example's
cross-entropy loss. Stated at one example (x, label), weights only (the
bias b is fixed), with an update W − lr·gh for any η-accurate gh.
sgd_descends' smoothness and differentiability hypotheses are discharged
for the Chapter-1 net: differentiability is
lossWeightMap_differentiable, the segment-Lipschitz constant is the
explicit C = 2a²/(1−2aD) at step radius D = lr·(‖∇L‖₁ + mn·η).
Remaining hypotheses are checkable arithmetic: the oracle accuracy η
(supplied by the float budgets), the small-step condition, and the two
dominance conditions. Conclusion: the loss drops by ≥ lr·‖∇L‖₂²/2.
The binary32 gradient of the MNIST-linear loss — the FloatModel
transcription of the per-example weight gradient: float forward logits z̃ = M.dense W b x,
the rounded softmax−onehot cotangent head, and one final rounded
multiply by the (exact) input xᵢ to form the outer-product weight
gradient ∂L/∂Wᵢⱼ = xᵢ·(softmax(z)ⱼ − onehotⱼ). Flattened to the
Vec (m*n) parameter layout that gradAt/linear_sgd_descends use.
Equations
- M.linearFloatGrad W b x fexp label = Proofs.Mat.flatten fun (i : Fin m) (j : Fin n) => M.mul (x i) (M.softmaxCECotF fexp (M.dense W b x) label j)
Instances For
The binary32 gradient is within mulErr u a 1 0 (cotErr …) of the
certified real gradient, per entry. The head accuracy is the existing
softmax_ce_cot_close (cotErr); the final input-multiply is one
mul_close with an exact left operand (ea = 0) bounded by a, and a
right operand softmax−onehot ∈ [−1,1] (C = 1). This is the bridge
that discharges linear_sgd_descends' abstract η.
One SGD step with the FloatModel binary32 gradient decreases one example's
cross-entropy loss; the gradient's accuracy is proven, not assumed. The
descent side (linear_sgd_descends) and the rounding side (FloatBridge's
cotErr/mulErr head budget) are fused into one statement: the gradient is
M.linearFloatGrad (the FloatModel transcription of the per-example weight
gradient), and its accuracy η = mulErr u a 1 0 (cotErr …) is proven by
linear_grad_close.
Scope: one example (x, label), weights only (bias fixed), and the update
Mat.flatten W − lr • g̃ taken in ℝ — only the gradient is float-modelled.
What remains as hypotheses: the input bound a, 0 ≤ lr, the exp
accuracy eexp (hfexp), the logit drift δ (hδ, the FloatModel →
kernel trust boundary of softmax_ce_cot_close), and the small-step and two
dominance conditions. Depth-1 means there is no per-layer η-threading.