Provedunbiased-attentionrandomized-algorithmssoftmaxgradient
The true derivative of attention: shifting scores by t·c_k, d/dt of the softmax output at 0 is E_π[c v] − E_π[v]·E_π[c]
For all and , if , then
What the notation means · or point at any symbol
- NNatural numbers
- The natural numbers 0, 1, 2, …. In Lean they start at 0. (
ℕ) - Fin
- Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Fin) - f(x)Function application
- Fin applied to n. Lean writes f x; papers write f(x). (
Fin n) - ⟹Implies
- If Fin(n), then ℝ. (Between types, A → B is the type of functions from A to B.) (
Fin n → ℝ) - x : TVariables
- s, c, v range over Fin n → ℝ: the statement must hold for every choice. (
(s c v : Fin n → ℝ)) - <Less than
- 0 is strictly smaller than ∑ k, exp(s(k)). (
0 < ∑ k, Real.exp (s k)) - HasDerivAt
- HasDerivAt: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
HasDerivAt) - ∑Summation
- Add up exp(s(k)) for every k. (
∑ k, Real.exp (s k)) - RReal numbers
- The real numbers: every point on the number line. (
ℝ) - eˣExponential function
- e raised to the power s(k), where e ≈ 2.718. (
Real.exp (s k)) - x ↦ f(x)Function (λ-abstraction)
- The function sending t to (∑ k, exp(s(k) + t · c(k)) · v(k))/(∑ k, exp(s(k) + t · c(…. Lean writes fun x => …; papers write x ↦ …. (
fun t => (∑ k, Real.exp (s k + t * c k)…) - a/bDivision
- ∑ k, exp(s(k) + t · c(k)) · v(k) divided by ∑ k, exp(s(k) + t · c(k)). In Lean, dividing by 0 gives 0. (
(∑ k, Real.exp (s k + t * c k) * v k) /…) - +Addition
- s(k) plus t · c(k). (
s k + t * c k) - ·Multiplication
- t times c(k). (
t * c k) - -Subtraction
- (∑ k, exp(s(k)) · c(k) · v(k))/(∑ k, exp(s(k))) minus (∑ k, exp(s(k)) · v(k))/(∑ k, exp(s(k))) · ((∑ k, exp(s(k)…. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
(∑ k, Real.exp (s k) * c k * v k) / (∑ …)
theorem ua-attention-derivative {n : ℕ} (s c v : Fin n → ℝ) (hZ : 0 < ∑ k, Real.exp (s k)) :
HasDerivAt (fun t => (∑ k, Real.exp (s k + t * c k) * v k) / (∑ k, Real.exp (s k + t * c k))) ((∑ k, Real.exp (s k) * c k * v k) / (∑ k, Real.exp (s k)) - ((∑ k, Real.exp (s k) * v k) / (∑ k, Real.exp (s k))) * ((∑ k, Real.exp (s k) * c k) / (∑ k, Real.exp (s k)))) 0A HasDerivAt statement, not an asserted formula: for s_k = ⟨q, k_k⟩ and a query perturbation along coordinate a (c_k = k_{k,a}), the derivative of Σ e^{s_k} v_k / Σ e^{s_k} is the covariance of c and v under the softmax row. This grounds the gradient lemmas (covariance form, product estimates, gradient gadget) in calculus. Part of 'Unbiased randomized attention: cost x variance thresholds', round 9 (true derivative, whole-instance reduction, compositions).
How it was proved
- Proved
- 4 October 2026
- By
- Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
- Checked by
- Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
- Axioms
- Classical.choice, Quot.sound, propext
- Proof
- 30 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.