diff options
Diffstat (limited to 'notes.norg')
| -rw-r--r-- | notes.norg | 111 |
1 files changed, 0 insertions, 111 deletions
diff --git a/notes.norg b/notes.norg deleted file mode 100644 index ed823b3..0000000 --- a/notes.norg +++ /dev/null @@ -1,111 +0,0 @@ -@document.meta -title: Neural Network Equivalence -description: WIP tool to prove NNEQ using Interaction Nets as pre-processor fo my Batchelor's Thesis -authors: ericmarin -categories: research -created: 2026-03-14T09:21:24 -updated: 2026-03-25T09:32:43 -version: 1.1.1 -@end - -* TODO - - (!) Scalability: - Added cache for already processed NN. - Removed limits from Inpla, but it runs slow on big NN because of parsing overhead. - *I should write a Reduction Engine in Rust with a Work Stealing Queue to be more flexible.* - - - (x) Soundness of translated NN: - Translation from NN to IN and the Interaction Rules are proved {:proof.norg:}[here]. - - - (x) Compatibility with other types of NN: - Added support for ONNX format. - Operations: Gemm, ReLU, Flatten, Reshape, Matmul. - - - (+) Comparison with other tool ({https://github.com/NeuralNetworkVerification/Marabou}[Marabou], {https://github.com/guykatzz/ReluplexCav2017}[Reluplex]): - My tool is just a pre-processor that takes an NN, optimizes it using IN and converts in a format for SMT solvers. - Marabou and Reluplex are solvers and this tool could be used WITH them. - DeePoly/Marabou-Preprocessor: numeric bound tightening, lossy and heuristic. - ONNX-Simplifier: just folds constants. - Neurify: symbolic bound tightening (similar to the Range agent). Doesn't use a solver - - - (!) Add Range agent to enable ReLU optimization: - - - ( ) Merging Linear packets of the same variable when Adding: - - ~ Completare passo induttivo dimostrazione - ~ 2 Reti uguali NOTE - ~ 1 Rete grande NOTE - -* Agents -** Built-in - - Eraser: delete other agents recursively - - Dup: duplicates other agents recursively - -** Implemented - - Linear(x, float q, float r): represent "q*x + r" - - Concrete(float k): represent a concrete value k - - Symbolic(id): represent the variable id - - Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete) - - Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete) - - ReLU(out): represent "IF x > 0 THEN x ELSE 0" - - Materialize(out): transforms a Linear packet into a final representation of TermAdd/TermMul - -* Rules -** Add - Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r); - - Concrete(float k) >< Add(out, b) - | k == 0 => out ~ b - | _ => b ~ AddCheckConcrete(out, k); - - Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r) - | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser - | (s == 0) && (t == 0) => out ~ Linear(x, q, r), y ~ Eraser - | (q == 0) && (r == 0) => out ~ (*L)Linear(y, s, t), x ~ Eraser - | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0); - - Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j); - - Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k); - - Concrete(float j) >< AddCheckConcrete(out, float k) - | j == 0 => out ~ Concrete(k) - | _ => out ~ Concrete(k + j); - -** Mul - Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r); - - Concrete(float k) >< Mul(out, b) - | k == 0 => b ~ Eraser, out ~ (*L)Concrete(0) - | k == 1 => out ~ b - | _ => b ~ MulCheckConcrete(out, k); - - Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r) - | ((q == 0) && (r == 0)) || ((s == 0) && (t == 0)) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser - | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0); - - Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j); - - Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k); - - Concrete(float j) >< MulCheckConcrete(out, float k) - | j == 0 => out ~ Concrete(0) - | j == 1 => out ~ Concrete(k) - | _ => out ~ Concrete(k * j); - -** ReLU - Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0); - - Concrete(float k) >< ReLU(out) - | k > 0 => out ~ (*L)Concrete(k) - | _ => out ~ Concrete(0); - -** Materialize - Linear(x, float q, float r) >< Materialize(out) - | (q == 0) => out ~ Concrete(r), x ~ Eraser - | (q == 1) && (r == 0) => out ~ x - | (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r)) - | (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x) - | _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r)); - - Concrete(float k) >< Materialize(out) => out ~ (*L)Concrete(k); |