1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
@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);
|
