diff options
| author | ericmarin <maarin.eric@gmail.com> | 2026-04-08 14:58:51 +0200 |
|---|---|---|
| committer | ericmarin <maarin.eric@gmail.com> | 2026-04-09 15:36:02 +0200 |
| commit | 9fb816496d392638fa6981e71800466d71434680 (patch) | |
| tree | dd4848bdff4f091716ad5c5ae0ad6a5d2cec8751 /proof.md | |
| parent | d48822e9aa91903e77a1496ef559cd42d09ad6d0 (diff) | |
| download | vein-9fb816496d392638fa6981e71800466d71434680.tar.gz vein-9fb816496d392638fa6981e71800466d71434680.zip | |
changed name
Diffstat (limited to 'proof.md')
| -rw-r--r-- | proof.md | 562 |
1 files changed, 0 insertions, 562 deletions
diff --git a/proof.md b/proof.md deleted file mode 100644 index 9a1d2c9..0000000 --- a/proof.md +++ /dev/null @@ -1,562 +0,0 @@ -# Soundness Proof -## Mathematical Definitions -\sim&space;out\Rightarrow&space;out=q*x+r&space;) -\sim&space;out\Rightarrow&space;out=k&space;) -\sim&space;a\Rightarrow&space;out=a+b&space;) -\sim&space;b\Rightarrow&space;out=q*x+(r+b)) -\sim&space;b\Rightarrow&space;out=k+b&space;) -\sim&space;a\Rightarrow&space;out=a*b&space;) -\sim&space;b\Rightarrow&space;out=q*b*x+r*b&space;) -\sim&space;b\Rightarrow&space;out=k*b&space;) -\sim&space;x\Rightarrow&space;out=\text{IF}\;(x>0)\;\text{THEN}\;x\;\text{ELSE}\;0) -\sim&space;x\Rightarrow&space;out=x&space;) - -## Soundness of Translation -### ReLU -ONNX ReLU node is defined as: - - -The translation defines the interactions: -) - -By definition this interaction is equal to: -\;\text{THEN}\;x_i\;\text{ELSE}\;0) - -### Gemm -ONNX Gemm node is defined as: - - -The translation defines the interactions: -)) -,...),v_n)\sim&space;Concrete(\beta*c_i)) - -By definition this interaction is equal to: - - - -By grouping the operations we get: - - -### Flatten -Just identity mapping because the wires are always Flatten. - - -### MatMul -Equal to Gemm with ,  and . - -### Reshape -Just identity mapping because the wires always Flatten. - - -### Add -ONNX Add node is defined as: - - -The translation defines the interactions: -\sim&space;a_i) - -By definition this interaction is equal to: - - -By grouping the operations we get: - - -### Sub -ONNX Sub node is defined as: - - -The translation defines the interactions: -\sim&space;a_i) -)\sim&space;b_i) - -By definition this interaction is equal to: - - - -By grouping the operations we get: - - -## 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: -```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) -``` - -#### Linear >< Materialize -><Materialize(out)\Rightarrow&space;(1),(2),(3),(4),(5)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -##### Case 1: -,x\sim&space;Eraser) - -RHS: - - -EQUIVALENCE: - - -##### Case 2: - - -RHS: - - - -EQUIVALENCE: - - -##### Case 3: -)) - -RHS: - - -EQUIVALENCE: - - -##### Case 4: -,x)) - -RHS: - - -EQUIVALENCE: - - -##### Case 5: -,x),Concrete(r))) - -RHS: - - -EQUIVALENCE: - - -#### Concrete >< Materialize -><Materialize(out)\Rightarrow&space;out\sim&space;Concrete(k)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -RHS: - - -EQUIVALENCE: - - -### Add -#### Linear >< Add -><Add(out,b)\Rightarrow&space;b\sim&space;AddCheckLinear(out,x,q,r)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -RHS: -) - -EQUIVALENCE: -\Rightarrow&space;q*x+(r+b)=q*x+(r+b)) - -#### Concrete >< Add -><Add(out,b)\Rightarrow&space;(1),(2)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -##### Case 1: - - -RHS: - - -EQUIVALENCE: - - -##### Case 2: -) - -RHS: - - -EQUIVALENCE: - - -#### Linear >< AddCheckLinear -><AddCheckLinear(out,x,q,r)\Rightarrow&space;(1),(2),(3),(4)) - -LHS: -\sim&space;wire) -\sim&space;wire) - -) -) - -##### Case 1: -,x\sim&space;Eraser,y\sim&space;Eraser) - -RHS: - - -EQUIVALENCE: -=0\Rightarrow&space;0=0) - -##### Case 2: -,y\sim&space;Eraser) - -RHS: - - -EQUIVALENCE: -=q*x+r\Rightarrow&space;q*x+r=q*x+r) - -##### Case 3: -,x\sim&space;Eraser) - -RHS: - - -EQUIVALENCE: -=s*y+t\Rightarrow&space;s*y+t=s*y+t) - -##### Case 4: -\sim&space;Materialize(out_x),Linear(y,s,t)\sim&space;Materialize(out_y),out\sim&space;Linear(TermAdd(out_x,out_y),1,0)) - -RHS: -\sim&space;wire_1) -\sim&space;wire_1) - - -\sim&space;wire_2) -\sim&space;wire_2) - - -+0) -Because `TermAdd(a, b)` is defined as `a+b`: -+0) - -EQUIVALENCE: -=1*(q*x+r+s*y+t)+0\Rightarrow&space;q*x+r+s*y+t=q*x+r+s*y+t) - -#### Concrete >< AddCheckLinear -><AddCheckLinear(out,x,q,r)\Rightarrow&space;out\sim&space;Linear(x,q,r+j)) - -LHS: -\sim&space;wire) -\sim&space;wire) - -) -) - -RHS: -) - -EQUIVALENCE: -=q*x+(r+j)) - -#### Linear >< AddCheckConcrete -><AddCheckConcrete(out,k)\Rightarrow&space;out\sim&space;Linear(y,s,t+k)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -RHS: -) - -EQUIVALENCE: -\Rightarrow&space;s*y+(t+k)=s*y+(t+k)) - -#### Concrete >< AddCheckConcrete -><AddCheckConcrete(out,k)\Rightarrow&space;(1),(2)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -##### Case 1: -) - -RHS: - - -EQUIVALENCE: - - -##### Case 2: -) - -RHS: - - -EQUIVALENCE: - - -### Mul -#### Linear >< Mul -><Mul(out,b)\Rightarrow&space;b\sim&space;MulCheckLinear(out,x,q,r)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - -*b) - -RHS: - - -EQUIVALENCE: -*b=q*b*x+r*b\Rightarrow&space;q*b*x+r*b=q*b*x+r*b) - -#### Concrete >< Mul -><Mul(out,b)\Rightarrow&space;(1),(2),(3)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -##### Case 1: -,b\sim&space;Eraser) - -RHS: - - -EQUIVALENCE: - - -##### Case 2: - - -RHS: - - -EQUIVALENCE: - - -##### Case 3: -) - -RHS: - - -EQUIVALENCE: - - -#### Linear >< MulCheckLinear -><MulCheckLinear(out,x,q,r)\Rightarrow&space;(1),(2)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - -*x+r*(s*y+t)) - -##### Case 1: -\lor(s,t=0)\Rightarrow&space;x\sim&space;Eraser,y\sim&space;Eraser,out\sim&space;Concrete(0)) - -RHS: - - -EQUIVALENCE: -*x+0*(s*y+t)=0\Rightarrow&space;0=0) - -*x+r*(0*y+0)=0\Rightarrow&space;0=0) - -##### Case 2: -\sim&space;Materialize(out_x),Linear(y,s,t)\sim&space;Materialize(out_y),out\sim&space;Linear(TermMul(out_x,out_y),1,0)) - -RHS: -\sim&space;wire_1) -\sim&space;wire_1) - - -\sim&space;wire_2) -\sim&space;wire_2) - - -+0) -Because `TermMul(a, b)` is defined as `a*b`: -*(s*y+t)+0) - -EQUIVALENCE: -*x+r*(s*y+t)=1*(q*x+r)*(s*y+t)\Rightarrow&space;q*(s*y+t)*x+r*(s*y+t)=(q*x+r)*(s*y+t)\Rightarrow&space;q*(s*y+t)*x+r*(s*y+t)=q*(s*y+t)*x+r*(s*y+t)) - - -#### Concrete >< MulCheckLinear -><MulCheckLinear(out,x,q,r)\Rightarrow&space;out\sim&space;Linear(x,q*j,r*j)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -RHS: - - -EQUIVALENCE: - - -#### Linear >< MulCheckConcrete -><MulCheckConcrete(out,k)\Rightarrow&space;out\sim&space;Linear(y,s*k,t*k)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - -) - -RHS: - - -EQUIVALENCE: -=s*k*y+t*k\Rightarrow&space;s*k*y+t*k=s*k*y+t*k) - - -#### Concrete >< MulCheckConcrete -><MulCheckConcrete(out,k)\Rightarrow&space;(1),(2),(3)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -##### Case 1: -) - -RHS: - - -EQUIVALENCE: - - -##### Case 2: -) - -RHS: - - -EQUIVALENCE: - - -##### Case 3: -) - -RHS: - - -EQUIVALENCE: - - -### ReLU -#### Linear >< ReLU -><ReLU(out)\Rightarrow&space;Linear(x,q,r)\sim&space;Materialize(out_x),out\sim&space;Linear(TermReLU(out_x),1,0)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - ->0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0) - -RHS: -\sim&space;wire) -\sim&space;wire) - - -+0) -Because `TermReLU(x)` is defined as `z3.If(x > 0, x, 0)`: ->0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0)+0) - -EQUIVALENCE: ->0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0=1*(\text{IF}\;(q*x+r)>0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0)+0\Rightarrow\text{IF}\;(q*x+r)>0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0=\text{IF}\;(q*x+r)>0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0) - - -#### Concrete >< ReLU -><ReLU(out)\Rightarrow&space;(1),(2)) - -LHS: -\sim&space;wire) -\sim&space;wire) - - - - -##### Case 1: -) - -RHS: - - -EQUIVALENCE: - - -##### Case 2: -) - -RHS: - - -EQUIVALENCE: - - -## Soundness of Reduction -Let  be the Interaction Net translated from a Neural Network . Let  be the state of the net -after  reduction steps. Then ![forall n in N, [IN_n] = [NN]](https://latex.codecogs.com/svg.image?\inline&space;\forall&space;n\in\mathbb{N},[\mathrm{IN_n}]=[\mathrm{NN}]). - -### Proof by Induction -- Base Case (): By the [Soundness of Translation](#soundness-of-translation), the initial net  is constructed such that -its semantics ![[IN_0]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_0}]) exactly match the mathematical definition of the ONNX nodes in . -- Induction Step (): Assume ![[IN_n] = [NN]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_n}]=[\mathrm{NN}]). If  is in normal form, the proof is complete. -Otherwise, there exists an active pair  that reduces . -By the [Soundness of Interaction Rules](#soundness-of-interaction-rules), the mathematical definition is preserved after any reduction step, -it follows that ![[IN_{n+1}] = [IN_n]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_{n+1}}]=[\mathrm{IN_n}]). By the inductive hypothesis, ![[IN_{n+1}] = [NN]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_{n+1}}]=[\mathrm{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. |