diff options
| -rw-r--r-- | .gitignore | 8 | ||||
| -rw-r--r-- | LICENSE | 2 | ||||
| -rw-r--r-- | README.md | 6 | ||||
| -rw-r--r-- | docs/proof.md (renamed from proof.md) | 2 | ||||
| -rw-r--r-- | examples/verify.py | 4 | ||||
| -rw-r--r-- | proof.norg | 513 | ||||
| -rw-r--r-- | vein.py (renamed from nneq.py) | 1 |
7 files changed, 8 insertions, 528 deletions
@@ -5,18 +5,10 @@ /examples/fashion_mnist/fashion_mnist_a.onnx.data /examples/fashion_mnist/fashion_mnist_b.onnx /examples/fashion_mnist/fashion_mnist_b.onnx.data -/examples/fashion_mnist/script_argmax.fish -/examples/fashion_mnist/script_epsilon.fish -/examples/fashion_mnist/script_strict.fish /examples/xor/xor_a.onnx /examples/xor/xor_a.onnx.data /examples/xor/xor_b.onnx /examples/xor/xor_b.onnx.data -/examples/fashion_mnist/FashionMNIST/raw -/notes.norg -/examples/ACASXU/script_argmax.fish -/examples/ACASXU/script_epsilon.fish -/examples/ACASXU/script_strict.fish /examples/iris/iris_b.onnx /examples/iris/iris_b.onnx.data /examples/iris/iris_a.onnx.data @@ -629,7 +629,7 @@ to attach them to the start of each source file to most effectively state the exclusion of warranty; and each file should have at least the "copyright" line and a pointer to where the full notice is found. - Neural Network Equivalence (NNEQ) + VErification via Interaction Nets (VEIN) Copyright (C) 2026 Eric Marin This program is free software: you can redistribute it and/or modify @@ -1,12 +1,12 @@ -# Neural Network Equivalence (NNEQ) +# VEIN: VErification via Interaction Nets Requires my [fork of Inpla](https://github.com/eric-marin/inpla). - Clone the fork - **make** the executable -- Copy the **inpla** executable in NNEQ/ +- Copy the **inpla** executable in **vein/** -[Soundness proof](./proof.md) +[Soundness proof](./docs/proof.md) ## License @@ -46,7 +46,7 @@ Equal to Gemm with  + ### Add ONNX Add node is defined as: diff --git a/examples/verify.py b/examples/verify.py index 046ec0b..65fb989 100644 --- a/examples/verify.py +++ b/examples/verify.py @@ -2,10 +2,10 @@ import sys, os sys.path.append(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) import z3 -import nneq +import vein def check_property(onnx_a, onnx_b, vnnlib): - solver = nneq.Solver() + solver = vein.Solver() print(f"--- Checking {vnnlib} ---") diff --git a/proof.norg b/proof.norg deleted file mode 100644 index 7bd9e25..0000000 --- a/proof.norg +++ /dev/null @@ -1,513 +0,0 @@ -@document.meta -title: proof -description: -authors: ericmarin -categories: research -created: 2026-03-16T11:34:52 -updated: 2026-03-28T17:37:48 -version: 1.1.1 -@end - -* Soundness Proof -** Mathematical Definitions - - $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)$ - - $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$ - - $MulCheckConcrete(out, k) ~ b => out = k*b$ - - $ReLU(out) ~ x => out = IF (x > 0) THEN x ELSE 0$ - - $Materialize(out) ~ x => out = x$ - -** Soundness of Translation -*** ReLU - ONNX ReLU node is defined as: - $Y = X if X > 0 else 0$ - - The translation defines the interactions: - $x_i ~ ReLU(y_i)$ - - By definition this interaction is equal to: - $y_i = IF (x_i > 0) THEN x_i ELSE 0$ - -*** Gemm - ONNX Gemm node is defined as: - $Y = alpha * A * B + beta * C$ - - The translation defines the interactions: - $a_i ~ Mul(v_i, Concrete(alpha * b_i))$ - $Add(...(Add(y_i, v_1), ...), v_n) ~ Concrete(beta * c_i)$ - - By definition this interaction is equal to: - $v_i = alpha * a_i * b_i$ - $y_i = v_1 + v_2 + ... + v_n + beta * c_i$ - - By grouping the operations we get: - $Y = alpha * A * B + beta * C$ - -*** Flatten - Just identity mapping because the wires are always Flatten. - $o_i ~ i_i$ - -*** MatMul - Equal to Gemm with $alpha=1$, $beta=0$ and $C=0$. - -*** Reshape - Just identity mapping because the wires always Flatten. - $o_i ~ i_i$ - -*** Add - ONNX Add node is defined as: - $C = A + B$ - - The translation defines the interactions: - $Add(c_i, b_i) ~ a_i$ - - By definition this interaction is equal to: - $c_i = a_i + b_i$ - - By grouping the operations we get: - $C = A + B$ - -*** Sub - ONNX Sub node is defined as: - $C = A - B$ - - The translation defines the interactions: - $Add(c_i, neg_b_i) ~ a_i$ - $Mul(neg_b_i, Concrete(-1)) ~ b_i$ - - By definition this interaction is equal to: - $c_i = a_i + neg_b_i$ - $neg_b_i = -1 * b_i$ - - By grouping the operations we get: - $C = A - B$ - -** Soundness of Interaction Rules -*** Materialize - The Materialize agent transforms a Linear agent into a tree of explicit mathematical operations - that are used as final representation for the solver. - In the Python module the terms are defined as: - @code python - def TermAdd(a, b): - return a + b - def TermMul(a, b): - return a * b - def TermReLU(x): - return z3.If(x > 0, x, 0) - @end -**** $Linear(x, q, r) >< Materialize(out) => (1), (2), (3), (4), (5)$ - LHS: - $Linear(x, q, r) ~ wire$ - $Materialize(out) ~ wire$ - $q*x + r = wire$ - $out = wire$ - $out = q*x + r$ - - $$ Case 1: $q = 0 => out ~ Concrete(r), x ~ Eraser$ - RHS: - $out = r$ - - EQUIVALENCE: - $0*x + r = r => r = r$ - $$ - - $$ Case 2: $q = 1, r = 0 => out ~ x$ - RHS: - $x = out$ - $out = x$ - - EQUIVALENCE: - $1*x + 0 = x => x = x$ - $$ - - $$ Case 3: $q = 1 => out ~ TermAdd(x, Concrete(r))$ - RHS: - $out = x + r$ - - EQUIVALENCE: - $1*x + r = x + r => x + r = x + r$ - $$ - - $$ Case 4: $r = 0 => out ~ TermMul(Concrete(q), x)$ - RHS: - $out = q*x$ - - EQUIVALENCE: - $q*x + 0 = q*x => q*x = q*x$ - $$ - - $$ Case 5: $otherwise => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r))$ - RHS: - $out = q*x + r$ - - EQUIVALENCE: - $q*x + r = q*x + r$ - $$ - -**** $Concrete(k) >< Materialize(out) => out ~ Concrete(k)$ - LHS: - $Concrete(k) ~ wire$ - $Materialize(out) ~ wire$ - $k = wire$ - $out = wire$ - $out = k$ - - RHS: - $out = k$ - - EQUIVALENCE: - $k = k$ - -*** Add -**** $Linear(x, q, r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r)$ - LHS: - $Linear(x, q, r) ~ wire$ - $Add(out, b) ~ wire$ - $q*x + r = wire$ - $out = wire + b$ - $out = q*x + r + b$ - - RHS: - $out = q*x + (r + b)$ - - EQUIVALENCE: - $q*x + r + b = q*x + (r + b) => q*x + (r + b) = q*x + (r + b)$ - -**** $Concrete(k) >< Add(out, b) => (1), (2)$ - LHS: - $Concrete(k) ~ wire$ - $Add(out, b) ~ wire$ - $k = wire$ - $out = wire + b$ - $out = k + b$ - - $$ Case 1: $k = 0 => out ~ b$ - RHS: - $out = b$ - - EQUIVALENCE: - $0 + b = b => b = b$ - $$ - - $$ Case 2: $otherwise => b ~ AddCheckConcrete(out, k)$ - RHS: - $out = k + b$ - - EQUIVALENCE: - $k + b = k + b$ - $$ - -**** $Linear(y, s, t) >< AddCheckLinear(out, x, q, r) => (1), (2), (3), (4)$ - LHS: - $Linear(y, s, t) ~ wire$ - $AddCheckLinear(out, x, q, r) ~ wire$ - $s*y + t = wire$ - $out = q*x + (r + wire)$ - $out = q*x + (r + s*y + t)$ - - $$ Case 1: $q,r,s,t = 0 => out ~ Concrete(0), x ~ Eraser, y ~ Eraser$ - RHS: - $out = 0$ - - EQUIVALENCE: - $0*x + (0 + 0*y + 0) = 0 => 0 = 0$ - $$ - - $$ Case 2: $s,t = 0 => out ~ Linear(x, q, r), y ~ Eraser$ - RHS: - $out = q*x + r$ - - EQUIVALENCE: - $q*x + (r + 0*y + 0) = q*x + r => q*x + r = q*x + r$ - $$ - - $$ Case 3: $q, r = 0 => out ~ Linear(y, s, t), x ~ Eraser$ - RHS: - $out = s*y + t$ - - EQUIVALENCE: - $0*x + (0 + s*y + t) = s*y + t => s*y + t = s*y + t$ - $$ - - $$ Case 4: $otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0)$ - RHS: - $Linear(x, q, r) ~ wire1$ - $Materialize(out_x) ~ wire1$ - $q*x + r = wire1$ - $out_x = wire1$ - $Linear(y, s, t) ~ wire2$ - $Materialize(out_y) ~ wire2$ - $s*y + t = wire2$ - $out_y = wire2$ - $out = 1*TermAdd(out_x, out_y) + 0$ - Because $TermAdd(a, b)$ is defined as "a+b$: - $out = 1*(q*x + r + s*y + t) + 0$ - - EQUIVALENCE: - $q*x + (r + s*y + t) = 1*(q*x + r + s*y + t) + 0 => q*x + r + s*y + t = q*x + r + s*y + t - $$ - -**** $Concrete(j) >< AddCheckLinear(out, x, q, r) => out ~ Linear(x, q, r + j)$ - LHS: - $Concrete(j) ~ wire$ - $AddCheckLinear(out, x, q, r) ~ wire$ - $j = wire$ - $out = q*x + (r + wire)$ - $out = q*x + (r + j)$ - - RHS: - $out = q*x + (r + j)$ - - EQUIVALENCE: - $q*x + (r + j) = q*x + (r + j)$ - -**** $Linear(y, s, t) >< AddCheckConcrete(out, k) => out ~ Linear(y, s, t + k)$ - LHS: - $Linear(y, s, t) ~ wire$ - $AddCheckConcrete(out, k) ~ wire$ - $s*y + t = wire$ - $out = k + wire$ - $out = k + s*y + t$ - - RHS: - $out = s*y + (t + k)$ - - EQUIVALENCE: - $k + s*y + t = s*y + (t + k) => s*y + (t + k) = s*y + (t + k)$ - -**** $Concrete(j) >< AddCheckConcrete(out, k) => (1), (2)$ - LHS: - $Concrete(j) ~ wire$ - $AddCheckConcrete(out, k) ~ wire$ - $j = wire$ - $out = k + wire$ - $out = k + j$ - - $$ Case 1: $j = 0 => out ~ Concrete(k)$ - RHS: - $out = k$ - - EQUIVALENCE: - $k + 0 = k => k = k$ - $$ - - $$ Case 2: $otherwise => out ~ Concrete(k + j)$ - RHS: - $out = k + j$ - - EQUIVALENCE: - $k + j = k + j$ - $$ - -*** Mul -**** $Linear(x, q, r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r)$ - LHS: - $Linear(x, q, r) ~ wire$ - $Mul(out, b) ~ wire$ - $q*x + r = wire$ - $out = wire * b$ - $out = (q*x + r) * b$ - - RHS: - $out = q*b*x + r*b$ - - EQUIVALENCE: - $(q*x + r) * b = q*b*x + r*b => q*b*x + r*b = q*b*x + r*b$ - -**** $Concrete(k) >< Mul(out, b) => (1), (2), (3)$ - LHS: - $Concrete(k) ~ wire$ - $Mul(out, b) ~ wire$ - $k = wire$ - $out = wire * b$ - $out = k * b$ - - $$ Case 1: $k = 0 => out ~ Concrete(0), b ~ Eraser$ - RHS: - $out = 0$ - - EQUIVALENCE: - $0 * b = 0 => 0 = 0$ - $$ - - $$ Case 2: $k = 1 => out ~ b$ - RHS: - $out = b$ - - EQUIVALENCE: - $1 * b = b => b = b$ - $$ - - $$ Case 3: $otherwise => b ~ MulCheckConcrete(out, k)$ - RHS: - $out = k * b$ - - EQUIVALENCE: - $k * b = k * b$ - $$ - -**** $Linear(y, s, t) >< MulCheckLinear(out, x, q, r) => (1), (2)$ - LHS: - $Linear(y, s, t) ~ wire$ - $MulCheckLinear(out, x, q, r) ~ wire$ - $s*y + t = wire$ - $out = q*wire*x + r*wire$ - $out = q*(s*y + t)*x + r*(s*y + t)$ - - $$ Case 1: $(q,r = 0) or (s,t = 0) => x ~ Eraser, y ~ Eraser, out ~ Concrete(0)$ - RHS: - $out = 0$ - - EQUIVALENCE: - $0*(s*y + t)*x + 0*(s*y + t) = 0 => 0 = 0$ - or - $q*(0*y + 0)*x + r*(0*y + 0) = 0 => 0 = 0$ - $$ - - $$ Case 2: $otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0)$ - RHS: - $Linear(x, q, r) ~ wire1$ - $Materialize(out_x) ~ wire1$ - $q*x + r = wire1$ - $out_x = wire1$ - $Linear(y, s, t) ~ wire2$ - $Materialize(out_y) ~ wire2$ - $s*y + t = wire2$ - $out_y = wire2$ - $out = 1*TermMul(out_x, out_y) + 0$ - Because $TermMul(a, b)$ is defined as $a*b$: - $out = 1*(q*x + r)*(s*y + t) + 0$ - - EQUIVALENCE: - $q*(s*y + t)*x + r*(s*y + t) = 1*(q*x + r)*(s*y + t) => - q*(s*y + t)*x + r*(s*y + t) = (q*x + r)*(s*y + t) => - q*(s*y + t)*x + r*(s*y + t) = q*(s*y + t)*x + r*(s*y + t)$ - $$ - -**** $Concrete(j) >< MulCheckLinear(out, x, q, r) => out ~ Linear(x, q * j, r * j)$ - LHS: - $Concrete(j) ~ wire$ - $MulCheckLinear(out, x, q, r) ~ wire$ - $j = wire$ - $out = q*wire*x + r*wire$ - $out = q*j*x + r*j$ - - RHS: - $out = q*j*x + r*j$ - - EQUIVALENCE: - $q*j*x + r*j = q*j*x + r*j$ - -**** $Linear(y, s, t) >< MulCheckConcrete(out, k) => out ~ Linear(y, s * k, t * k)$ - LHS: - $Linear(y, s, t) ~ wire$ - $MulCheckConcrete(out, k) ~ wire$ - $s*y + t = wire$ - $out = k * wire$ - $out = k * (s*y + t)$ - - RHS: - $out = s*k*y + t*k$ - - EQUIVALENCE: - $k * (s*y + t) = s*k*y + t*k => s*k*y + t*k = s*k*y + t*k$ - -**** $Concrete(j) >< MulCheckConcrete(out, k) => (1), (2), (3)$ - LHS: - $Concrete(j) ~ wire$ - $MulCheckConcrete(out, k) ~ wire$ - $j = wire$ - $out = k * wire$ - $out = k * j$ - - $$ Case 1: $j = 0 => out ~ Concrete(0)$ - RHS: - $out = 0$ - - EQUIVALENCE: - $k * 0 = 0 => 0 = 0$ - $$ - - $$ Case 2: $j = 1 => out ~ Concrete(k)$ - RHS: - $out = k$ - - EQUIVALENCE: - $k * 1 = k => k = k$ - $$ - - $$ Case 3: $otherwise => out ~ Concrete(k * j)$ - RHS: - $out = k * j$ - - EQUIVALENCE: - $k * j = k * j$ - -*** ReLU -**** $Linear(x, q, r) >< ReLU(out) => Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0)$ - LHS: - $Linear(x, q, r) ~ wire$ - $ReLU(out) ~ wire$ - $q*x + r = wire$ - $out = IF wire > 0 THEN wire ELSE 0$ - $out = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0$ - - RHS: - $Linear(x, q, r) ~ wire$ - $Materialize(out_x) ~ wire$ - $q*x + r = wire$ - $out_x = wire$ - $out = 1*TermReLU(out_x) + 0$ - Because $TermReLU(x)$ is defined as $z3.If(x > 0, x, 0)$: - $out = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0$ - - EQUIVALENCE: - $IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0 => - IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0$ - -**** $Concrete(k) >< ReLU(out) => (1), (2)$ - LHS: - $Concrete(k) ~ wire$ - $ReLU(out) ~ wire$ - $k = wire$ - $out = IF wire > 0 THEN wire ELSE 0$ - $out = IF k > 0 THEN k ELSE 0$ - - $$ Case 1: $k > 0 => out ~ Concrete(k)$ - RHS: - $out = k$ - - EQUIVALENCE: - $IF true THEN k ELSE 0 = k => k = k$ - $$ - - $$ Case 2: $k <= 0 => out ~ Concrete(0)$ - RHS: - $out = 0$ - - EQUIVALENCE: - $IF false THEN k ELSE 0 = 0 => 0 = 0$ - $$ - -** Soundness of Reduction - Let $IN_0$ be the Interaction Net translated from a Neural Network $NN$. Let $IN_n$ be the state of the net - after $n$ reduction steps. Then $\forall n \in N$, $[IN_n] = [NN]$. - -*** Proof by Induction - - Base Case ($n = 0$): By the {* Soundness of Translation}, the initial net $IN_0$ is constructed such that - its semantics $[IN_0]$ exactly match the mathematical definition of the ONNX nodes in $NN$. - - Induction Step ($n -> n + 1$): Assume $[IN_n] = [NN]$. If $IN_n$ is in normal form, the proof is complete. - Otherwise, there exists an active pair $A$ that reduces $IN_n$ to $IN_{n+1}$. - By the {* Soundness of Interaction Rules}, the mathematical definition is preserved after any reduction step, - it follows that $[IN_{n+1}] = [IN_n]$. By the inductive hypothesis, $[IN_{n+1}] = [NN]$. - --- - - By the principle of mathematical induction, the Interaction Net remains semantically equivalent to the original - Neural Network at every step of the reduction process. - - Since Interaction Nets are confluent, the reduced mathematical expression is unique regardless - of order in which rules are applied. @@ -1,3 +1,4 @@ +# VErification via interaction Nets (VEIN) # Copyright (C) 2026 Eric Marin # # This program is free software: you can redistribute it and/or modify it under the terms of the |