bend-ml-autograd Releases (2): 0.1.1.0 0x0ed882696c6c048c64c66242a999a426 indexed https://jend.leeeet.dev/files.txt?path=bend-ml-autograd@0.1.1.0 0.1.0.0 0x174ef0d27bc1c621ddb9961c7f224de1 unindexed https://jend.leeeet.dev/files.txt?path=bend-ml-autograd@0.1.0.0 Definitions (33): BendMlAutograd.NE (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=NE) # Expressions with one variable NX, over Nat (a commutative semiring). type NE is Data: NCst{n: Nat} NX{} NAdd{a: NE, b: NE} NMul{a: NE, b: NE} BendMlAutograd.nval (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nval) # value of the expression at x def nval(e: NE, +x: Nat) -> Nat: BendMlAutograd.nfwd (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nfwd) # FORWARD-mode derivative (dual numbers): derivative of the sum and the product rule def nfwd(e: NE, +x: Nat) -> Nat: BendMlAutograd.nbwd (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nbwd) # REVERSE-mode derivative: g is the gradient arriving from the output; each node passes on # g (sum) or g * value-of-the-other-factor (product) to its children and adds up what # arrives at NX. def nbwd(e: NE, +x: Nat, +g: Nat) -> Nat: BendMlAutograd.ndist_l (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=ndist_l) # a * (b + c) == a*b + a*c (left distributivity; nat-lemmas only has the right one) def ndist_l(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}: BendMlAutograd.nmul_case (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nmul_case) # The product case, with everything abstracted into numbers: # (g*vb)*fa + (g*va)*fb == g * (fa*vb + va*fb) def nmul_case(+g: Nat, +fa: Nat, +fb: Nat, +va: Nat, +vb: Nat, +ba: Nat, +bb: Nat, iha: {ba == Nat.mul(Nat.mul(g, vb), fa) : Nat}, ihb: {bb == Nat.mul(Nat.mul(g, va), fb) : Nat}) -> {Nat.add(ba, bb) == Nat.mul(g, Nat.add(Nat.mul(fa, vb), Nat.mul(va, fb))) : Nat}: BendMlAutograd.nbwd_ok (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=nbwd_ok) # The reverse mode returns g times the forward-mode derivative. def nbwd_ok(e: NE, +x: Nat, +g: Nat) -> {nbwd(e, x, g) == Nat.mul(g, nfwd(e, x)) : Nat}: BendMlAutograd.reverse_eq_forward (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=reverse_eq_forward) # LAW (reverse_eq_forward): for any expression made of constants, X, sums # and products, the reverse-mode gradient (starting with gradient 1 at the output) # equals the forward-mode derivative. It holds for every x. law reverse_eq_forward: for +e: NE for +x: Nat {nbwd(e, x, 1n) == nfwd(e, x) : Nat} BendMlAutograd.G (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=G) type G is Data: GCst{c: F32} GVar{i: Nat} GAdd{a: G, b: G} GMul{a: G, b: G} GRelu{a: G} GTanh{a: G} GExp{a: G} BendMlAutograd.lookup (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=lookup) def lookup(env: List<&2, F32>, +i: Nat) -> F32: BendMlAutograd.gval (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=gval) def gval(e: G, +env: List<&2, F32>) -> F32: BendMlAutograd.acc_add (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=acc_add) # adds v to the gradient of variable i def acc_add(acc: List<&2, F32>, +i: Nat, +v: F32) -> List<&2, F32>: BendMlAutograd.mask2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=mask2) def mask2(pos: Bool) -> F32: BendMlAutograd.relu_d (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=relu_d) # local derivative of relu: 1 if the input > 0, else 0 def relu_d(+x: F32) -> F32: BendMlAutograd.tanh_d (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=tanh_d) def tanh_d(+x: F32) -> F32: BendMlAutograd.gbwd (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=gbwd) # g is the gradient arriving at the node; acc accumulates the gradient of each variable def gbwd(e: G, +env: List<&2, F32>, +g: F32, acc: List<&2, F32>) -> List<&2, F32>: BendMlAutograd.ggrad (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=ggrad) # gradient of the expression with respect to each variable of env def ggrad(e: G, +env: List<&2, F32>) -> List<&2, F32>: BendMlAutograd.linear (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=linear) # y = x·W + b x: n x i, W: i x o, b: o -> y: n x o def linear(-n: Nat, +i: Nat, +o: Nat, x: T.Mat, w: T.Mat, b: T.Vec) -> T.Mat: BendMlAutograd.linear_bwd (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=linear_bwd) # Given the gradient dy arriving at y, returns (dx, (dW, db)): # dx = dy · Wᵀ (n x o)·(o x i) = n x i # dW = xᵀ · dy (i x n)·(n x o) = i x o # db = sum of the rows of dy # If any of these products had the wrong dimensions, the program would not compile. def linear_bwd(+n: Nat, +i: Nat, +o: Nat, x: T.Mat, w: T.Mat, +dy: T.Mat) -> T.Mat & (T.Mat & T.Vec): BendMlAutograd.mask.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=mask.l) def mask.l(xs: List<&2, F32>) -> List<&2, F32>: BendMlAutograd.mask.rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=mask.rows) def mask.rows(xs: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>: BendMlAutograd.relu_bwd (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=relu_bwd) # y = relu(x); the gradient passes where x > 0 def relu_bwd(-r: Nat, -c: Nat, x: T.Mat, dy: T.Mat) -> T.Mat: BendMlAutograd.onehot.cell (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=onehot.cell) # one-hot: n rows of c numbers, with 1 at the label's position def onehot.cell(hit: Bool) -> F32: BendMlAutograd.onehot.row (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=onehot.row) def onehot.row(c: Nat, +k: Nat, +j: Nat) -> List<&2, F32>: BendMlAutograd.onehot.rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=onehot.rows) def onehot.rows(labels: List<&2, Nat>, +c: Nat) -> List<&2, List<&2, F32>>: BendMlAutograd.log.l (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=log.l) def log.l(xs: List<&2, F32>) -> List<&2, F32>: BendMlAutograd.log.rows (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=log.rows) def log.rows(xs: List<&2, List<&2, F32>>) -> List<&2, List<&2, F32>>: BendMlAutograd.rows.total (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=rows.total) def rows.total(xs: List<&2, List<&2, F32>>, acc: F32) -> F32: BendMlAutograd.ce_loss2 (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=ce_loss2) def ce_loss2(-n: Nat, -c: Nat, +cc: Nat, +nf: F32, p: T.Mat, labels: List<&2, Nat>) -> F32: BendMlAutograd.ce_loss (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=ce_loss) # mean cross-entropy loss: -(1/n) Σ log p[i][label_i] def ce_loss(+n: Nat, +c: Nat, logits: T.Mat, labels: List<&2, Nat>) -> F32: BendMlAutograd.ce_grad (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=ce_grad) # gradient of the loss with respect to the logits: (softmax - one-hot) / n def ce_grad(+n: Nat, +c: Nat, logits: T.Mat, labels: List<&2, Nat>) -> T.Mat: BendMlAutograd.sgd (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=sgd) def sgd(-r: Nat, -c: Nat, +lr: F32, w: T.Mat, dw: T.Mat) -> T.Mat: BendMlAutograd.sgd_vec (https://jend.leeeet.dev/definition.txt?path=bend-ml-autograd@0.1.1.0/main.bend&name=sgd_vec) def sgd_vec(-n: Nat, +lr: F32, b: T.Vec, db: T.Vec) -> T.Vec: