law causal_grad

bendtorch@1.3.0.0 · LAWS.bend:169

import Base
import bendtorch@1.3.0.0/main.bend as T

169# LAW (causal_grad): in T.Attention's backward pass, row i of a head's G (the gradient of its scores) is computed over
170# exactly i + 1 positions. T.grow reads dP's row against values 0..i only (as qrow reads keys 0..i), writes it from the
171# start of its row and runs the softmax's backward pass over as many positions as it wrote; this law says that count is
172# i + 1. G starts as zeros and nothing else writes the row, so its other t - (i + 1) positions stay 0: no gradient
173# reaches a key or a value after the query's position.
174law causal_grad:
175  for +i: Nat
176  for +t: Nat
177  for +hd: Nat
178  for +sc: F32
179  for +ds: U32
180  for +dc: U32
181  for +vs: U32
182  for +vc: U32
183  for d: Array<F32>
184  for v: Array<F32>
185  for p: Array<F32>
186  for g: Array<F32>
187  {T.gr_n(T.grow(i, t, hd, sc, ds, dc, vs, vc, d, v, p, g)) == 1n+i : Nat}