Provedunbiased-gradientscounterexamplereview-response
Counterexample: reusing the forward samples in the backward pass biases the gradient: E[ô·d̂] = p(1−p)/2, but the dense gradient is p²(1−p) (3/32 vs 3/64 at p = 1/4)
For all :
What the notation means · or point at any symbol
- RReal numbers
- The real numbers: every point on the number line. (
ℝ) - ∑Summation
- Add up p if x.1, else 1 − p · p if x.2, else 1 − p · ((1 if x.1, … for every x in Bool × Bool. (
∑ x : Bool × Bool, (if x.1 then p else …) - =Equality
- ∑ x, p if x.1, else 1 − p · p if x.2, else 1 − p · ((1 if … and p are the same. (
∑ x : Bool × Bool, (if x.1 then p else …) - Bool
- Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (
Bool) - ×Product
- Pairs of an element of Bool and an element of Bool. (
Bool × Bool) - ·Multiplication
- p if x.1, else 1 − p times p if x.2, else 1 − p. (
(if x.1 then p else 1 - p) * (if x.2 th…) - { a if c; b otherwiseCases (if … then … else)
- p when x.1, and 1 − p otherwise. (
if x.1 then p else 1 - p) - p₁Component
- The first component of the pair x. (
x.1) - -Subtraction
- 1 minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (
1 - p) - a/bDivision
- 1 if x.1, else 0 + 1 if x.2, else 0 divided by 2. In Lean, dividing by 0 gives 0. (
((if x.1 then (1 : ℝ) else 0) + (if x.2…) - +Addition
- 1 if x.1, else 0 plus 1 if x.2, else 0. (
(if x.1 then (1 : ℝ) else 0) + (if x.2 …) - (x : T)As real numbers
- 1 read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. (
(1 : ℝ)) - aᵇPower
- 1 if x.1, else 0 − 1 if x.2, else 0 raised to the power 2. (
((if x.1 then (1 : ℝ) else 0) - (if x.2…) - ⟹Implies
- If p = 1/4, then p · (1 − p)/2 = 3/32 ∧ p^2 · (1 − p) = 3/64. (Between types, A → B is the type of functions from A to B.) (
p = 1 / 4 → p * (1 - p) / 2 = 3 / 32 ∧ …) - ∧And
- Both hold: p · (1 − p)/2 = 3/32, and p^2 · (1 − p) = 3/64. (
p * (1 - p) / 2 = 3 / 32 ∧ p ^ 2 * (1 -…)
theorem ug-sample-reuse-gradient-bias (p : ℝ) :
(∑ x : Bool × Bool, (if x.1 then p else 1 - p) * (if x.2 then p else 1 - p) * (((if x.1 then (1 : ℝ) else 0) + (if x.2 then 1 else 0)) / 2) = p) ∧ (∑ x : Bool × Bool, (if x.1 then p else 1 - p) * (if x.2 then p else 1 - p) * (((if x.1 then (1 : ℝ) else 0) - (if x.2 then 1 else 0)) ^ 2 / 2) = p * (1 - p)) ∧ (∑ x : Bool × Bool, (if x.1 then p else 1 - p) * (if x.2 then p else 1 - p) * ((((if x.1 then (1 : ℝ) else 0) + (if x.2 then 1 else 0)) / 2) * (((if x.1 then (1 : ℝ) else 0) - (if x.2 then 1 else 0)) ^ 2 / 2)) = p * (1 - p) / 2) ∧ (p = 1 / 4 → p * (1 - p) / 2 = 3 / 32 ∧ p ^ 2 * (1 - p) = 3 / 64)Two keys with scores (0, θ), values (0, 1), loss ℓ(o) = o²/2, so o = p = σ(θ) and the dense gradient is p²(1−p). Two exact samples X₁, X₂ ~ Bernoulli(p): the forward estimate ô = (X₁+X₂)/2 is unbiased, the local derivative estimate d̂ = (X₁−X₂)²/2 is unbiased for p(1−p), but their product has mean p(1−p)/2, twice the dense gradient at p = 1/4. Unbiased forward and local-derivative estimates do not give an unbiased gradient of the dense loss when the upstream derivative depends on the same samples. Counterexample supplied by an external review (2026-10-05); it bounds the scope of op-one-pass-gradient-unbiased (fixed upstream vector).
How it was proved
- Proved
- 5 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
- 16 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.