~/bend-docscommunity

main.bend checks

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

bend-ml-tensor: tensores com a shape no TIPO. Erro de shape é erro de tipo.

import bend-ml-tensor@0.1.0.0/main.bend as T

Vec<n> é um vetor de n números F32; Mat<r, c> é uma matriz r x c (lista de r linhas com c números). As dimensões são parâmetros de tipo apagados: não custam nada em tempo de execução, mas o checker as confere em toda operação.

2 imports
import Base
import bend-ml-nat-lemmas@0.1.0.0/main.bend as NL

Laws

law reshape_swap proved

Also proved in bend-mathlib as nat.mul_comm: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.mul_comm.

source · line 473 · raw

@+r:Nat -> @+c:Nat -> {Nat.mul(r, c) == Nat.mul(c, r) : Nat}

LEI (reshape_swap): r x c e c x r têm o mesmo número de elementos (a multiplicação é comutativa), então esse reshape sempre existe.

law reshape_flat provedsource · line 483 · raw

@+r:Nat -> @+c:Nat -> {Nat.mul(r, c) == Nat.mul(1n, Nat.mul(r, c)) : Nat}

LEI (reshape_flat): r x c tem o mesmo número de elementos que 1 x (r*c) (multiplicar por 1 não muda nada), então achatar uma matriz sempre existe.

Types

type Vec source · line 12 · raw

@-n:Nat -> Data

type Mat source · line 15 · raw

@-r:Nat -> @-c:Nat -> Data

Definitions

def zip_with.add source · line 22 · raw

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

def zip_with.sub source · line 29 · raw

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

def zip_with.mul source · line 36 · raw

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

def scale.l source · line 43 · raw

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

def dot.go source · line 50 · raw

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

def sum.go source · line 57 · raw

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

def relu.l source · line 64 · raw

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

def fill.l source · line 71 · raw

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

def Vec.zeros source · line 82 · raw

@n:Nat -> Vec<n>

def Vec.fill source · line 85 · raw

@n:Nat -> @+v:F32 -> Vec<n>

def Vec.add source · line 88 · raw

@-n:Nat -> @a:Vec<n> -> @b:Vec<n> -> Vec<n>

def Vec.sub source · line 93 · raw

@-n:Nat -> @a:Vec<n> -> @b:Vec<n> -> Vec<n>

def Vec.mul source · line 98 · raw

@-n:Nat -> @a:Vec<n> -> @b:Vec<n> -> Vec<n>

def Vec.scale source · line 103 · raw

@-n:Nat -> @+k:F32 -> @a:Vec<n> -> Vec<n>

def Vec.dot source · line 108 · raw

@-n:Nat -> @a:Vec<n> -> @b:Vec<n> -> F32

def Vec.sum source · line 113 · raw

@-n:Nat -> @a:Vec<n> -> F32

def Vec.relu source · line 118 · raw

@-n:Nat -> @a:Vec<n> -> Vec<n>

def heads source · line 127 · raw

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

def tails source · line 134 · raw

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

def transpose.go source · line 142 · raw

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

transposta de uma matriz com c colunas (c é quem encolhe, vem primeiro)

def rows.zip_add source · line 149 · raw

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

def rows.zip_sub source · line 156 · raw

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

def rows.zip_mul source · line 163 · raw

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

def rows.scale source · line 170 · raw

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

def rows.relu source · line 177 · raw

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

def rows.col_sums source · line 185 · raw

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

soma por colunas

def rows.add_row source · line 192 · raw

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

def matmul.row source · line 199 · raw

@+ra:List<&2, F32> -> @bt:List<&2, List<&2, F32>> -> List<&2, F32>

def matmul.rows source · line 206 · raw

@a:List<&2, List<&2, F32>> -> @+bt:List<&2, List<&2, F32>> -> List<&2, List<&2, F32>>

def flatten.l source · line 214 · raw

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

junta todas as linhas numa lista só

def chunk.l source · line 222 · raw

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

quebra uma lista em r linhas de c números

def Mat.zeros source · line 233 · raw

@+r:Nat -> @+c:Nat -> Mat<r, c>

def Mat.fill source · line 236 · raw

@+r:Nat -> @+c:Nat -> @+v:F32 -> Mat<r, c>

def Mat.add source · line 239 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> @b:Mat<r, c> -> Mat<r, c>

def Mat.sub source · line 244 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> @b:Mat<r, c> -> Mat<r, c>

def Mat.mul source · line 250 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> @b:Mat<r, c> -> Mat<r, c>

produto elemento a elemento (Hadamard)

def Mat.scale source · line 255 · raw

@-r:Nat -> @-c:Nat -> @+k:F32 -> @a:Mat<r, c> -> Mat<r, c>

def Mat.relu source · line 260 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> Mat<r, c>

def Mat.transpose source · line 265 · raw

@-r:Nat -> @+c:Nat -> @a:Mat<r, c> -> Mat<c, r>

def Mat.matmul source · line 271 · raw

@-n:Nat -> @+k:Nat -> @+m:Nat -> @a:Mat<n, k> -> @b:Mat<k, m> -> Mat<n, m>

(n x k) · (k x m) = (n x m): as dimensões internas têm que ser a mesma k

def Mat.add_row source · line 277 · raw

@-n:Nat -> @-m:Nat -> @a:Mat<n, m> -> @b:Vec<m> -> Mat<n, m>

soma bias (um vetor de m números) a cada linha de uma matriz n x m

def Mat.col_sums source · line 283 · raw

@-n:Nat -> @+m:Nat -> @a:Mat<n, m> -> Vec<m>

soma de cada coluna: Mat<n, m> -> Vec<m>

def Mat.matvec source · line 289 · raw

@-n:Nat -> @+k:Nat -> @a:Mat<n, k> -> @v:Vec<k> -> Vec<n>

matriz · vetor: (n x k) · k = n

def Mat.reshape source · line 295 · raw

@-r1:Nat -> @-c1:Nat -> @r2:Nat -> @+c2:Nat -> @-p:{Nat.mul(r1, c1) == Nat.mul(r2, c2) : Nat} -> @a:Mat<r1, c1> -> Mat<r2, c2>

Reshape: só compila com a PROVA de que o número de elementos não muda.

def max.go source · line 304 · raw

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

def max.l source · line 311 · raw

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

def exp_shift source · line 318 · raw

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

def div.l source · line 325 · raw

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

def softmax.fin source · line 333 · raw

@+es:List<&2, F32> -> List<&2, F32>

softmax estável: subtrai o máximo antes de exponenciar

def softmax.l source · line 336 · raw

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

def rows.softmax source · line 339 · raw

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

def gelu.f source · line 347 · raw

@+x:F32 -> F32

GELU com a aproximação por tanh (a mesma do GPT-2)

def gelu.l source · line 350 · raw

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

def rows.gelu source · line 357 · raw

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

def sub_const source · line 364 · raw

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

def sq_sum source · line 371 · raw

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

def layernorm.fin source · line 379 · raw

@+cs:List<&2, F32> -> @+d:F32 -> @+eps:F32 -> @+gamma:List<&2, F32> -> @+beta:List<&2, F32> -> List<&2, F32>

(x - média) / sqrt(variância + eps), depois * gamma + beta

def layernorm.l source · line 382 · raw

@+xs:List<&2, F32> -> @+d:F32 -> @+eps:F32 -> @+gamma:List<&2, F32> -> @+beta:List<&2, F32> -> List<&2, F32>

def rows.layernorm source · line 385 · raw

@xs:List<&2, List<&2, F32>> -> @+d:F32 -> @+eps:F32 -> @+gamma:List<&2, F32> -> @+beta:List<&2, F32> -> List<&2, List<&2, F32>>

def Mat.softmax source · line 392 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> Mat<r, c>

def Mat.gelu source · line 397 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> Mat<r, c>

def Mat.layernorm source · line 403 · raw

@-n:Nat -> @d:Nat -> @eps:F32 -> @g:Vec<d> -> @bt:Vec<d> -> @a:Mat<n, d> -> Mat<n, d>

normaliza cada linha (d colunas) e aplica gamma e beta, vetores de d números

def Vec.softmax source · line 408 · raw

@-n:Nat -> @a:Vec<n> -> Vec<n>

def len.eq source · line 417 · raw

@xs:List<&2, F32> -> @n:Nat -> Bool

def rows.ok source · line 426 · raw

@rs:List<&2, List<&2, F32>> -> @+c:Nat -> @r:Nat -> Bool

def Vec.of2 source · line 435 · raw

@-n:Nat -> @ok:Bool -> @xs:List<&2, F32> -> Maybe<&2, Vec<n>>

def Vec.of source · line 443 · raw

@n:Nat -> @+xs:List<&2, F32> -> Maybe<&2, Vec<n>>

Vec<n> a partir de uma lista, só se ela tem exatamente n números

def Mat.of2 source · line 446 · raw

@-r:Nat -> @-c:Nat -> @ok:Bool -> @rs:List<&2, List<&2, F32>> -> Maybe<&2, Mat<r, c>>

def Mat.of source · line 454 · raw

@+r:Nat -> @+c:Nat -> @+rs:List<&2, List<&2, F32>> -> Maybe<&2, Mat<r, c>>

Mat<r, c> a partir de linhas, só se são exatamente r linhas de c números

def Vec.to_list source · line 457 · raw

@-n:Nat -> @a:Vec<n> -> List<&2, F32>

def Mat.to_rows source · line 462 · raw

@-r:Nat -> @-c:Nat -> @a:Mat<r, c> -> List<&2, List<&2, F32>>

def Mat.flatten source · line 492 · raw

@+r:Nat -> @+c:Nat -> @a:Mat<r, c> -> Mat<1n, Nat.mul(r, c)>

Mat<r, c> -> Mat<1, r*c>: a prova vem da lei acima

def Mat.reshape_swap source · line 496 · raw

@+r:Nat -> @+c:Nat -> @a:Mat<r, c> -> Mat<c, r>

Mat<r, c> -> Mat<c, r> pelos mesmos dados (não é a transposta!): só reinterpreta