diff options
| author | ericmarin <maarin.eric@gmail.com> | 2026-03-23 17:53:21 +0100 |
|---|---|---|
| committer | ericmarin <maarin.eric@gmail.com> | 2026-03-25 10:23:07 +0100 |
| commit | 689c34076d08e59b1382864f9efcd983c8665ae5 (patch) | |
| tree | b76f3eb0ece697cb042d578a0a11800bd13a8dc8 /proof.norg | |
| parent | 4a9b66faae8bf362849b961ac2bf5dedc079c6ce (diff) | |
| download | vein-689c34076d08e59b1382864f9efcd983c8665ae5.tar.gz vein-689c34076d08e59b1382864f9efcd983c8665ae5.zip | |
added FashionMNIST
xd
Diffstat (limited to '')
| -rw-r--r-- | proof.norg | 23 |
1 files changed, 13 insertions, 10 deletions
@@ -2,21 +2,21 @@ title: proof description: authors: ericmarin -categories: +categories: research created: 2026-03-16T11:34:52 -updated: 2026-03-17T18:59:09 +updated: 2026-03-25T08:18:04 version: 1.1.1 @end * Mathematical Definitions - - Linear(x, q, r) ~ out => out = q*x + r %with q,r Real% - - Concrete(k) ~ out => out = k %with k Real% + - Linear(x, q, r) ~ out => out = q*x + r + - Concrete(k) ~ out => out = k - Add(out, b) ~ a => out = a + b - - AddCheckLinear(out, x, q, r) ~ b => out = q*x + (r + b) %with q,r Real% - - AddCheckConcrete(out, k) ~ b => out = k + b %with k Real% + - AddCheckLinear(out, x, q, r) ~ b => out = q*x + (r + b) + - AddCheckConcrete(out, k) ~ b => out = k + b - Mul(out, b) ~ a => out = a * b - - MulCheckLinear(out, x, q, r) ~ b => out = q*b*x + r*b %with q,r Real% - - MulCheckConcrete(out, k) ~ b => out = k*b %with k Real% + - MulCheckLinear(out, x, q, r) ~ b => out = q*b*x + r*b + - MulCheckConcrete(out, k) ~ b => out = k*b - ReLU(out) ~ x => out = IF (x > 0) THEN x ELSE 0 - Materialize(out) ~ x => out = x @@ -47,10 +47,13 @@ version: 1.1.1 /Y = alpha * A * B + beta * C/ ** Flatten - Just identity mapping + Just identity mapping. ** MatMul - Equal to Gemm with alpha=1 and beta=0 + Equal to Gemm with alpha=1 and beta=0. + +** Reshape + Just identity mapping. * Proof for the Interaction Rules ** Materialize |
