main.bend checks

raw source on the hub · import bend-ml-autograd@0.1.0.0/main.bend as Main

bend-ml-autograd: diferenciação automática com uma lei provada.

import bend-ml-autograd@0.1.0.0/main.bend as AG

1) MODELO PROVADO (sobre Nat): o modo reverso do autodiff dá o mesmo resultado que o modo direto (números duais). Prova pelo kernel, usando os lemas de soma e produto do bend-ml-nat-lemmas. 2) AUTOGRAD DE ESCALARES em F32 (estilo micrograd), com a mesma estrutura. 3) CAMADAS COM TENSORES (forward e backward) cujo formato é checado pelo tipo.

F32 não é um número real, então a correção NUMÉRICA do F32 é validada por testes contra o PyTorch (reference/test_autograd.py), não por prova.

3 imports

import Base
import bend-ml-nat-lemmas@0.1.0.0/main.bend as NL
import bend-ml-tensor@0.1.0.0/main.bend as T

Laws

law reverse_eq_forward provedsource · line 113 · raw

@+e:NE -> @+x:Nat -> {nbwd(e, x, 1n) == nfwd(e, x) : Nat}

LEI (reverse_eq_forward): para qualquer expressão feita de constantes, X, somas e produtos, o gradiente em modo reverso (começando com gradiente 1 na saída) é igual à derivada em modo direto. Vale para todo x.

Types

type NE source · line 23 · raw

Data

Expressões com uma variável NX, sobre Nat (um semianel comutativo).

NCst
```
@n:Nat -> NE
```
NX
```
NE
```
NAdd
```
@a:NE -> @b:NE -> NE
```
NMul
```
@a:NE -> @b:NE -> NE
```

type G source · line 126 · raw

Data

GCst
```
@c:F32 -> G
```
GVar
```
@i:Nat -> G
```
GAdd
```
@a:G -> @b:G -> G
```
GMul
```
@a:G -> @b:G -> G
```
GRelu
```
@a:G -> G
```
GTanh
```
@a:G -> G
```
GExp
```
@a:G -> G
```

Definitions

def nval source · line 30 · raw

@e:NE -> @+x:Nat -> Nat

valor da expressão em x

def nfwd source · line 42 · raw

@e:NE -> @+x:Nat -> Nat

derivada em modo DIRETO (números duais): derivada da soma e regra do produto

def nbwd source · line 56 · raw

@e:NE -> @+x:Nat -> @+g:Nat -> Nat

derivada em modo REVERSO: g é o gradiente que chega da saída; cada nó repassa g (soma) ou g * valor-do-outro-fator (produto) para os filhos e soma o que chega em NX.

def ndist_l source · line 68 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(a, Nat.add(b, c)) == Nat.add(Nat.mul(a, b), Nat.mul(a, c)) : Nat}

a * (b + c) == a*b + a*c (distributividade à esquerda; o nat-lemmas só tem à direita)

def nmul_case source · line 79 · raw

@+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}

Caso do produto, com tudo abstraído em números: (g*vb)*fa + (g*va)*fb == g * (fa*vb + va*fb)

def nbwd_ok source · line 95 · raw

@e:NE -> @+x:Nat -> @+g:Nat -> {nbwd(e, x, g) == Nat.mul(g, nfwd(e, x)) : Nat}

O modo reverso devolve g vezes a derivada do modo direto.

def lookup source · line 135 · raw

@env:List<&2, F32> -> @+i:Nat -> F32

def gval source · line 144 · raw

@e:G -> @+env:List<&2, F32> -> F32

def acc_add source · line 162 · raw

@acc:List<&2, F32> -> @+i:Nat -> @+v:F32 -> List<&2, F32>

soma v ao gradiente da variável i

def mask2 source · line 171 · raw

@pos:Bool -> F32

def relu_d source · line 179 · raw

@+x:F32 -> F32

derivada local da relu: 1 se a entrada > 0, senão 0

def tanh_d source · line 182 · raw

@+x:F32 -> F32

def gbwd source · line 186 · raw

@e:G -> @+env:List<&2, F32> -> @+g:F32 -> @acc:List<&2, F32> -> List<&2, F32>

g é o gradiente que chega ao nó; acc acumula o gradiente de cada variável

def ggrad source · line 204 · raw

@e:G -> @+env:List<&2, F32> -> List<&2, F32>

gradiente da expressão em relação a cada variável de env

def linear source · line 212 · raw

@-n:Nat -> @+i:Nat -> @+o:Nat -> @x:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, i> -> @w:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<i, o> -> @b:0xf9837737d2c3f58ae1d0c5df42255584/main.Vec<o> -> 0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, o>

y = x·W + b x: n x i, W: i x o, b: o -> y: n x o

def linear_bwd source · line 220 · raw

@+n:Nat -> @+i:Nat -> @+o:Nat -> @x:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, i> -> @w:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<i, o> -> @+dy:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, o> -> Pair(0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, i>, Pair(0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<i, o>, 0xf9837737d2c3f58ae1d0c5df42255584/main.Vec<o>))

Dado o gradiente dy que chega em y, devolve (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 = soma das linhas de dy Se alguma conta tivesse as dimensões erradas, o programa não compilaria.

def mask.l source · line 223 · raw

@xs:List<&2, F32> -> List<&2, F32>

def mask.rows source · line 230 · raw

@xs:List<&2, List<&2, F32>> -> List<&2, List<&2, F32>>

def relu_bwd source · line 238 · raw

@-r:Nat -> @-c:Nat -> @x:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<r, c> -> @dy:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<r, c> -> 0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<r, c>

y = relu(x); o gradiente passa onde x > 0

def onehot.cell source · line 244 · raw

@hit:Bool -> F32

one-hot: n linhas de c números, com 1 na posição do rótulo

def onehot.row source · line 247 · raw

@c:Nat -> @+k:Nat -> @+j:Nat -> List<&2, F32>

def onehot.rows source · line 254 · raw

@labels:List<&2, Nat> -> @+c:Nat -> List<&2, List<&2, F32>>

def log.l source · line 261 · raw

@xs:List<&2, F32> -> List<&2, F32>

def log.rows source · line 268 · raw

@xs:List<&2, List<&2, F32>> -> List<&2, List<&2, F32>>

def rows.total source · line 275 · raw

@xs:List<&2, List<&2, F32>> -> @acc:F32 -> F32

def ce_loss2 source · line 282 · raw

@-n:Nat -> @-c:Nat -> @+cc:Nat -> @+nf:F32 -> @p:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, c> -> @labels:List<&2, Nat> -> F32

def ce_loss source · line 288 · raw

@+n:Nat -> @+c:Nat -> @logits:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, c> -> @labels:List<&2, Nat> -> F32

perda de entropia cruzada média: -(1/n) Σ log p[i][rótulo_i]

def ce_grad source · line 292 · raw

@+n:Nat -> @+c:Nat -> @logits:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, c> -> @labels:List<&2, Nat> -> 0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<n, c>

gradiente da perda em relação aos logits: (softmax - one-hot) / n

def sgd source · line 295 · raw

@-r:Nat -> @-c:Nat -> @+lr:F32 -> @w:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<r, c> -> @dw:0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<r, c> -> 0xf9837737d2c3f58ae1d0c5df42255584/main.Mat<r, c>

def sgd_vec source · line 298 · raw

@-n:Nat -> @+lr:F32 -> @b:0xf9837737d2c3f58ae1d0c5df42255584/main.Vec<n> -> @db:0xf9837737d2c3f58ae1d0c5df42255584/main.Vec<n> -> 0xf9837737d2c3f58ae1d0c5df42255584/main.Vec<n>