Additive-Bias Scaled-Dot-Product Attention

This file proves the differentiable fixed-score-bias form:

softmax(c · QKᵀ + bias) V.

The bias tensor is fixed data. This is useful for relative-position biases or other intentional finite score shifts. It is not the boolean causal-mask semantics: boolean attention masks in the spec/runtime path use hard masking, where blocked entries contribute zero softmax numerator.

@[reducible, inline]

abbrev Proofs.Autograd.Attention.ssMaskedScaledDotProduct (m d : ℕ) : List Spec.Shape

Saved tensors for fixed-bias scaled-dot-product attention.

noncomputable def Proofs.Autograd.Attention.maskedScaledDotProductDGraph {m d : ℕ} (c : ℝ) (bias : Vec (Spec.Shape.dim m (Spec.Shape.dim m Spec.Shape.scalar)).size := 0) : DGraph (ΓQKV m d) (ssMaskedScaledDotProduct m d)

Scaled dot-product attention with a fixed additive score bias.

The proof follows the unmasked graph with one extra affine identity node between scaling and softmax. Because the bias is fixed, its derivative is the identity on the scaled logits.

theorem Proofs.Autograd.Attention.backprop_eq_adjoint_fderiv_maskedScaledDotProduct {m d : ℕ} (c : ℝ) (bias : Vec (Spec.Shape.dim m (Spec.Shape.dim m Spec.Shape.scalar)).size := 0) (xV : CtxVec (ΓQKV m d)) (seedV : CtxVec (ΓQKV m d ++ ssMaskedScaledDotProduct m d)) : (maskedScaledDotProductDGraph c bias).g.backpropVec xV seedV = (ContinuousLinearMap.adjoint (fderiv ℝ (maskedScaledDotProductDGraph c bias).g.evalVec xV)) seedV

Reverse-mode theorem for finite additive-mask scaled-dot-product attention.