From 9fb816496d392638fa6981e71800466d71434680 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Wed, 8 Apr 2026 14:58:51 +0200 Subject: changed name --- docs/proof.md | 562 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 562 insertions(+) create mode 100644 docs/proof.md (limited to 'docs') diff --git a/docs/proof.md b/docs/proof.md new file mode 100644 index 0000000..07717f9 --- /dev/null +++ b/docs/proof.md @@ -0,0 +1,562 @@ +# Soundness Proof +## Mathematical Definitions +![Linear(x, q, r) ~ out => out = q*x + r](https://latex.codecogs.com/svg.image?Linear(x,q,r)\sim&space;out\Rightarrow&space;out=q*x+r&space;) +![Concrete(k) ~ out => out = ](https://latex.codecogs.com/svg.image?Concrete(k)\sim&space;out\Rightarrow&space;out=k&space;) +![Add(out, b) ~ a => out = a + b](https://latex.codecogs.com/svg.image?Add(out,b)\sim&space;a\Rightarrow&space;out=a+b&space;) +![AddCheckLinear(out, x, q, r) ~ b => out = q*x + (r + b)](https://latex.codecogs.com/svg.image?AddCheckLinear(out,x,q,r)\sim&space;b\Rightarrow&space;out=q*x+(r+b)) +![AddCheckConcrete(out, k) ~ b => out = k + b](https://latex.codecogs.com/svg.image?AddCheckConcrete(out,k)\sim&space;b\Rightarrow&space;out=k+b&space;) +![Mul(out, b) ~ a => out = a * b](https://latex.codecogs.com/svg.image?Mul(out,b)\sim&space;a\Rightarrow&space;out=a*b&space;) +![MulCheckLinear(out, x, q, r) ~ b => out = q*b*x + r*b](https://latex.codecogs.com/svg.image?MulCheckLinear(out,x,q,r)\sim&space;b\Rightarrow&space;out=q*b*x+r*b&space;) +![MulCheckConcrete(out, k) ~ b => out = k*b](https://latex.codecogs.com/svg.image?MulCheckConcrete(out,k)\sim&space;b\Rightarrow&space;out=k*b&space;) +![ReLU(out) ~ x => out = IF (x > 0) THEN x ELSE 0](https://latex.codecogs.com/svg.image?ReLU(out)\sim&space;x\Rightarrow&space;out=\text{IF}\;(x>0)\;\text{THEN}\;x\;\text{ELSE}\;0) +![Materialize(out) ~ x => out = x](https://latex.codecogs.com/svg.image?Materialize(out)\sim&space;x\Rightarrow&space;out=x&space;) + +## Soundness of Translation +### ReLU +ONNX ReLU node is defined as: +![Y = X if X > 0 else 0](https://latex.codecogs.com/svg.image?Y=X\;if\;X>0\;else\;0&space;) + +The translation defines the interactions: +![x_i ~ ReLU(y_i)](https://latex.codecogs.com/svg.image?x_i\sim&space;ReLU(y_i)) + +By definition this interaction is equal to: +![y_i = IF (x_i > 0) THEN x_i ELSE 0](https://latex.codecogs.com/svg.image?y_i=\text{IF}\;(x_i>0)\;\text{THEN}\;x_i\;\text{ELSE}\;0) + +### Gemm +ONNX Gemm node is defined as: +![Y = alpha * A * B + beta * C](https://latex.codecogs.com/svg.image?Y=\alpha\cdot&space;A\cdot&space;B+\beta\cdot&space;C&space;) + +The translation defines the interactions: +![a_i ~ Mul(v_i, Concrete(alpha * b_i))](https://latex.codecogs.com/svg.image?a_i\sim&space;Mul(v_i,Concrete(\alpha*b_i))) +![Add(...(Add(y_i, v_1), ...), v_n) ~ Concrete(beta * c_i)](https://latex.codecogs.com/svg.image?Add(...(Add(y_i,v_1),...),v_n)\sim&space;Concrete(\beta*c_i)) + +By definition this interaction is equal to: +![v_i = alpha * a_i * b_i](https://latex.codecogs.com/svg.image?v_i=\alpha*a_i*b_i&space;) +![y_i = v_1 + v_2 + ... + v_n + beta * c_i](https://latex.codecogs.com/svg.image?y_i=v_1+v_2+...+v_n+\beta*c_i&space;) + +By grouping the operations we get: +![Y = alpha * A * B + beta * C](https://latex.codecogs.com/svg.image?Y=\alpha\cdot&space;A\cdot&space;B+\beta\cdot&space;C&space;) + +### Flatten +Just identity mapping because the wires are always Flatten. +![out_i ~ in_i](https://latex.codecogs.com/svg.image?out_i\sim&space;in_i) + +### MatMul +Equal to Gemm with ![alpha=1](https://latex.codecogs.com/svg.image?\inline&space;\alpha=1), ![beta=0](https://latex.codecogs.com/svg.image?\inline&space;\beta=0) and ![C=0](https://latex.codecogs.com/svg.image?\inline&space;&space;C=0). + +### Reshape +Just identity mapping because the wires always Flatten. +![out_i ~ in_i](https://latex.codecogs.com/svg.image?out_i\sim&space;in_i) + +### Add +ONNX Add node is defined as: +![C = A + B](https://latex.codecogs.com/svg.image?&space;C=A+B) + +The translation defines the interactions: +![Add(c_i, b_i) ~ a_i](https://latex.codecogs.com/svg.image?Add(c_i,b_i)\sim&space;a_i) + +By definition this interaction is equal to: +![c_i = a_i + b_i](https://latex.codecogs.com/svg.image?c_i=a_i+b_i) + +By grouping the operations we get: +![C = A + B](https://latex.codecogs.com/svg.image?C=A+B) + +### Sub +ONNX Sub node is defined as: +![C = A - B](https://latex.codecogs.com/svg.image?C=A-B) + +The translation defines the interactions: +![Add(c_i, neg_b_i) ~ a_i](https://latex.codecogs.com/svg.image?Add(c_i,neg_i)\sim&space;a_i) +![Mul(neg_b_i, Concrete(-1)) ~ b_i](https://latex.codecogs.com/svg.image?Mul(neg_i,Concrete(-1))\sim&space;b_i) + +By definition this interaction is equal to: +![c_i = a_i + neg_b_i](https://latex.codecogs.com/svg.image?c_i=a_i+neg_i) +![neg_b_i = -1 * b_i](https://latex.codecogs.com/svg.image?neg_i=-1*b_i) + +By grouping the operations we get: +![C = A - B](https://latex.codecogs.com/svg.image?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: +```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 +![Linear(x, q, r) >< Materialize(out) => (1), (2), (3), (4), (5)](https://latex.codecogs.com/svg.image?\inline&space;&space;Linear(x,q,r)> out ~ Concrete(r), x ~ Eraser](https://latex.codecogs.com/svg.image?q=0\Rightarrow&space;out\sim&space;Concrete(r),x\sim&space;Eraser) + +RHS: +![out = r](https://latex.codecogs.com/svg.image?out=r) + +EQUIVALENCE: +![0*x + r = r => r = r](https://latex.codecogs.com/svg.image?0*x+r=r\Rightarrow&space;r=r) + +##### Case 2: +![q = 1, r = 0 => out ~ x](https://latex.codecogs.com/svg.image?q=1,r=0\Rightarrow&space;out~x) + +RHS: +![x = out](https://latex.codecogs.com/svg.image?x=out) +![out = x](https://latex.codecogs.com/svg.image?out=x) + +EQUIVALENCE: +![1*x + 0 = x => x = x](https://latex.codecogs.com/svg.image?1*x+0=x\Rightarrow&space;x=x) + +##### Case 3: +![q = 1 => out ~ TermAdd(x, Concrete(r))](https://latex.codecogs.com/svg.image?q=1\Rightarrow&space;out\sim&space;TermAdd(x,Concrete(r))) + +RHS: +![out = x + r](https://latex.codecogs.com/svg.image?out=x+r) + +EQUIVALENCE: +![1*x + r = x + r => x + r = x + r](https://latex.codecogs.com/svg.image?1*x+r=x+r\Rightarrow&space;x+r=x+r) + +##### Case 4: +![r = 0 => out ~ TermMul(Concrete(q), x)](https://latex.codecogs.com/svg.image?r=0\Rightarrow&space;out\sim&space;TermMul(Concrete(q),x)) + +RHS: +![out = q*x](https://latex.codecogs.com/svg.image?out=q*x) + +EQUIVALENCE: +![q*x + 0 = q*x => q*x = q*x](https://latex.codecogs.com/svg.image?q*x+0=q*x\Rightarrow&space;q*x=q*x) + +##### Case 5: +![otherwise => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r))](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;out\sim&space;TermAdd(TermMul(Concrete(q),x),Concrete(r))) + +RHS: +![out = q*x + r](https://latex.codecogs.com/svg.image?out=q*x+r) + +EQUIVALENCE: +![q*x + r = q*x + r](https://latex.codecogs.com/svg.image?q*x+r=q*x+r) + +#### Concrete >< Materialize +![Concrete(k) >< Materialize(out) => out ~ Concrete(k)](https://latex.codecogs.com/svg.image?Concrete(k)>< Add +![Linear(x, q, r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r)](https://latex.codecogs.com/svg.image?Linear(x,q,r)> q*x + (r + b) = q*x + (r + b)](https://latex.codecogs.com/svg.image?q*x+r+b=q*x+(r+b)\Rightarrow&space;q*x+(r+b)=q*x+(r+b)) + +#### Concrete >< Add +![Concrete(k) >< Add(out, b) => (1), (2)](https://latex.codecogs.com/svg.image?Concrete(k)> out ~ b](https://latex.codecogs.com/svg.image?k=0\Rightarrow&space;out\sim&space;b) + +RHS: +![out = b](https://latex.codecogs.com/svg.image?out=b) + +EQUIVALENCE: +![0 + b = b => b = b](https://latex.codecogs.com/svg.image?0+b=b\Rightarrow&space;b=b) + +##### Case 2: +![otherwise => b ~ AddCheckConcrete(out, k)](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;b\sim&space;AddCheckConcrete(out,k)) + +RHS: +![out = k + b](https://latex.codecogs.com/svg.image?out=k+b) + +EQUIVALENCE: +![k + b = k + b](https://latex.codecogs.com/svg.image?k+b=k+b) + +#### Linear >< AddCheckLinear +![Linear(y, s, t) >< AddCheckLinear(out, x, q, r) => (1), (2), (3), (4)](https://latex.codecogs.com/svg.image?Linear(y,s,t)> out ~ Concrete(0), x ~ Eraser, y ~ Eraser](https://latex.codecogs.com/svg.image?q,r,s,t=0\Rightarrow&space;out\sim&space;Concrete(0),x\sim&space;Eraser,y\sim&space;Eraser) + +RHS: +![out = 0](https://latex.codecogs.com/svg.image?out=0) + +EQUIVALENCE: +![0*x + (0 + 0*y + 0) = 0 => 0 = 0](https://latex.codecogs.com/svg.image?0*x+(0+0*y+0)=0\Rightarrow&space;0=0) + +##### Case 2: +![s,t = 0 => out ~ Linear(x, q, r), y ~ Eraser](https://latex.codecogs.com/svg.image?s,t=0\Rightarrow&space;out\sim&space;Linear(x,q,r),y\sim&space;Eraser) + +RHS: +![out = q*x + r](https://latex.codecogs.com/svg.image?out=q*x+r) + +EQUIVALENCE: +![q*x + (r + 0*y + 0) = q*x + r => q*x + r = q*x + r](https://latex.codecogs.com/svg.image?q*x+(r+0*y+0)=q*x+r\Rightarrow&space;q*x+r=q*x+r) + +##### Case 3: +![q, r = 0 => out ~ Linear(y, s, t), x ~ Eraser](https://latex.codecogs.com/svg.image?q,r=0\Rightarrow&space;out\sim&space;Linear(y,s,t),x\sim&space;Eraser) + +RHS: +![out = s*y + t](https://latex.codecogs.com/svg.image?out=s*y+t) + +EQUIVALENCE: +![0*x + (0 + s*y + t) = s*y + t => s*y + t = s*y + t](https://latex.codecogs.com/svg.image?0*x+(0+s*y+t)=s*y+t\Rightarrow&space;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)](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;Linear(x,q,r)\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: +![Linear(x, q, r) ~ wire_1](https://latex.codecogs.com/svg.image?Linear(x,q,r)\sim&space;wire_1) +![Materialize(out_x) ~ wire_1](https://latex.codecogs.com/svg.image?Materialize(out_x)\sim&space;wire_1) +![q*x + r = wire_1](https://latex.codecogs.com/svg.image?q*x+r=wire_1) +![out_x = wire_1](https://latex.codecogs.com/svg.image?out_x=wire_1) +![Linear(y, s, t) ~ wire_2](https://latex.codecogs.com/svg.image?Linear(y,s,t)\sim&space;wire_2) +![Materialize(out_y) ~ wire_2](https://latex.codecogs.com/svg.image?Materialize(out_y)\sim&space;wire_2) +![s*y + t = wire_2](https://latex.codecogs.com/svg.image?s*y+t=wire_2) +![out_y = wire_2](https://latex.codecogs.com/svg.image?out_y=wire_2) +![out = 1*TermAdd(out_x, out_y) + 0](https://latex.codecogs.com/svg.image?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](https://latex.codecogs.com/svg.image?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](https://latex.codecogs.com/svg.image?q*x+(r+s*y+t)=1*(q*x+r+s*y+t)+0\Rightarrow&space;q*x+r+s*y+t=q*x+r+s*y+t) + +#### Concrete >< AddCheckLinear +![Concrete(j) >< AddCheckLinear(out, x, q, r) => out ~ Linear(x, q, r + j)](https://latex.codecogs.com/svg.image?Concrete(j)>< AddCheckConcrete +![Linear(y, s, t) >< AddCheckConcrete(out, k) => out ~ Linear(y, s, t + k)](https://latex.codecogs.com/svg.image?Linear(y,s,t)> s*y + (t + k) = s*y + (t + k)](https://latex.codecogs.com/svg.image?k+s*y+t=s*y+(t+k)\Rightarrow&space;s*y+(t+k)=s*y+(t+k)) + +#### Concrete >< AddCheckConcrete +![Concrete(j) >< AddCheckConcrete(out, k) => (1), (2)](https://latex.codecogs.com/svg.image?Concrete(j)> out ~ Concrete(k)](https://latex.codecogs.com/svg.image?j=0\Rightarrow&space;out\sim&space;Concrete(k)) + +RHS: +![out = k](https://latex.codecogs.com/svg.image?out=k) + +EQUIVALENCE: +![k + 0 = k => k = k](https://latex.codecogs.com/svg.image?k+0=k\Rightarrow&space;k=k) + +##### Case 2: +![otherwise => out ~ Concrete(k + j)](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;out\sim&space;Concrete(k+j)) + +RHS: +![out = k + j](https://latex.codecogs.com/svg.image?out=k+j) + +EQUIVALENCE: +![k + j = k + j](https://latex.codecogs.com/svg.image?k+j=k+j) + +### Mul +#### Linear >< Mul +![Linear(x, q, r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r)](https://latex.codecogs.com/svg.image?Linear(x,q,r)> q*b*x + r*b = q*b*x + r*b](https://latex.codecogs.com/svg.image?(q*x+r)*b=q*b*x+r*b\Rightarrow&space;q*b*x+r*b=q*b*x+r*b) + +#### Concrete >< Mul +![Concrete(k) >< Mul(out, b) => (1), (2), (3)](https://latex.codecogs.com/svg.image?Concrete(k)> out ~ Concrete(0), b ~ Eraser](https://latex.codecogs.com/svg.image?k=0\Rightarrow&space;out\sim&space;Concrete(0),b\sim&space;Eraser) + +RHS: +![out = 0](https://latex.codecogs.com/svg.image?out=0) + +EQUIVALENCE: +![0 * b = 0 => 0 = 0](https://latex.codecogs.com/svg.image?0*b=0\Rightarrow&space;0=0) + +##### Case 2: +![k = 1 => out ~ b](https://latex.codecogs.com/svg.image?k=1\Rightarrow&space;out\sim&space;b) + +RHS: +![out = b](https://latex.codecogs.com/svg.image?out=b) + +EQUIVALENCE: +![1 * b = b => b = b](https://latex.codecogs.com/svg.image?1*b=b\Rightarrow&space;b=b) + +##### Case 3: +![otherwise => b ~ MulCheckConcrete(out, k)](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;b\sim&space;MulCheckConcrete(out,k)) + +RHS: +![out = k * b](https://latex.codecogs.com/svg.image?out=k*b) + +EQUIVALENCE: +![k * b = k * b](https://latex.codecogs.com/svg.image?k*b=k*b) + +#### Linear >< MulCheckLinear +![Linear(y, s, t) >< MulCheckLinear(out, x, q, r) => (1), (2)](https://latex.codecogs.com/svg.image?Linear(y,s,t)> x ~ Eraser, y ~ Eraser, out ~ Concrete(0)](https://latex.codecogs.com/svg.image?(q,r=0)\lor(s,t=0)\Rightarrow&space;x\sim&space;Eraser,y\sim&space;Eraser,out\sim&space;Concrete(0)) + +RHS: +![out = 0](https://latex.codecogs.com/svg.image?out=0) + +EQUIVALENCE: +![0*(s*y + t)*x + 0*(s*y + t) = 0 => 0 = 0](https://latex.codecogs.com/svg.image?0*(s*y+t)*x+0*(s*y+t)=0\Rightarrow&space;0=0) +![or](https://latex.codecogs.com/svg.image?\lor) +![q*(0*y + 0)*x + r*(0*y + 0) = 0 => 0 = 0](https://latex.codecogs.com/svg.image?q*(0*y+0)*x+r*(0*y+0)=0\Rightarrow&space;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)](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;Linear(x,q,r)\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: +![Linear(x, q, r) ~ wire_1](https://latex.codecogs.com/svg.image?Linear(x,q,r)\sim&space;wire_1) +![Materialize(out_x) ~ wire_1](https://latex.codecogs.com/svg.image?Materialize(out_x)\sim&space;wire_1) +![q*x + r = wire_1](https://latex.codecogs.com/svg.image?q*x+r=wire_1) +![out_x = wire_1](https://latex.codecogs.com/svg.image?out_x=wire_1) +![Linear(y, s, t) ~ wire_2](https://latex.codecogs.com/svg.image?Linear(y,s,t)\sim&space;wire_2) +![Materialize(out_y) ~ wire_2](https://latex.codecogs.com/svg.image?Materialize(out_y)\sim&space;wire_2) +![s*y + t = wire_2](https://latex.codecogs.com/svg.image?s*y+t=wire_2) +![out_y = wire_2](https://latex.codecogs.com/svg.image?out_y=wire_2) +![out = 1*TermMul(out_x, out_y) + 0](https://latex.codecogs.com/svg.image?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](https://latex.codecogs.com/svg.image?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)](https://latex.codecogs.com/svg.image?q*(s*y+t)*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 +![Concrete(j) >< MulCheckLinear(out, x, q, r) => out ~ Linear(x, q * j, r * j)](https://latex.codecogs.com/svg.image?Concrete(j)>< MulCheckConcrete +![Linear(y, s, t) >< MulCheckConcrete(out, k) => out ~ Linear(y, s * k, t * k)](https://latex.codecogs.com/svg.image?Linear(y,s,t)> s*k*y + t*k = s*k*y + t*k](https://latex.codecogs.com/svg.image?k*(s*y+t)=s*k*y+t*k\Rightarrow&space;s*k*y+t*k=s*k*y+t*k) + + +#### Concrete >< MulCheckConcrete +![Concrete(j) >< MulCheckConcrete(out, k) => (1), (2), (3)](https://latex.codecogs.com/svg.image?Concrete(j)> out ~ Concrete(0)](https://latex.codecogs.com/svg.image?j=0\Rightarrow&space;out\sim&space;Concrete(0)) + +RHS: +![out = 0](https://latex.codecogs.com/svg.image?out=0) + +EQUIVALENCE: +![k * 0 = 0 => 0 = 0](https://latex.codecogs.com/svg.image?k*0=0\Rightarrow&space;0=0) + +##### Case 2: +![j = 1 => out ~ Concrete(k)](https://latex.codecogs.com/svg.image?j=1\Rightarrow&space;out\sim&space;Concrete(k)) + +RHS: +![out = k](https://latex.codecogs.com/svg.image?out=k) + +EQUIVALENCE: +![k * 1 = k => k = k](https://latex.codecogs.com/svg.image?k*1=k\Rightarrow&space;k=k) + +##### Case 3: +![otherwise => out ~ Concrete(k * j)](https://latex.codecogs.com/svg.image?otherwise\Rightarrow&space;out\sim&space;Concrete(k*j)) + +RHS: +![out = k * j](https://latex.codecogs.com/svg.image?out=k*j) + +EQUIVALENCE: +![k * j = k * j](https://latex.codecogs.com/svg.image?k*j=k*j) + +### ReLU +#### Linear >< ReLU +![Linear(x, q, r) >< ReLU(out) => Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0)](https://latex.codecogs.com/svg.image?Linear(x,q,r)> 0 THEN wire ELSE 0](https://latex.codecogs.com/svg.image?out=\text{IF}\;wire>0\;\text{THEN}\;wire\;\text{ELSE}\;0) +![out = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0](https://latex.codecogs.com/svg.image?out=\text{IF}\;(q*x+r)>0\;\text{THEN}\;(q*x+r)\;\text{ELSE}\;0) + +RHS: +![Linear(x, q, r) ~ wire](https://latex.codecogs.com/svg.image?Linear(x,q,r)\sim&space;wire) +![Materialize(out_x) ~ wire](https://latex.codecogs.com/svg.image?Materialize(out_x)\sim&space;wire) +![q*x + r = wire](https://latex.codecogs.com/svg.image?q*x+r=wire) +![out_x = wire](https://latex.codecogs.com/svg.image?out_x=wire) +![out = 1*TermReLU(out_x) + 0](https://latex.codecogs.com/svg.image?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](https://latex.codecogs.com/svg.image?out=1*(\text{IF}\;(q*x+r)>0\;\text{THEN}\;(q*x+r)\;\text{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](https://latex.codecogs.com/svg.image?\text{IF}\;(q*x+r)>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 +![Concrete(k) >< ReLU(out) => (1), (2)](https://latex.codecogs.com/svg.image?Concrete(k)> 0 THEN wire ELSE 0](https://latex.codecogs.com/svg.image?out=\text{IF}\;wire>0\;\text{THEN}\;wire\;\text{ELSE}\;0) +![out = IF k > 0 THEN k ELSE 0](https://latex.codecogs.com/svg.image?out=\text{IF}\;k>0\;\text{THEN}\;k\;\text{ELSE}\;0) + +##### Case 1: +![k > 0 => out ~ Concrete(k)](https://latex.codecogs.com/svg.image?k>0\Rightarrow&space;out\sim&space;Concrete(k)) + +RHS: +![out = k](https://latex.codecogs.com/svg.image?out=k) + +EQUIVALENCE: +![IF true THEN k ELSE 0 = k => k = k](https://latex.codecogs.com/svg.image?\text{IF}\;true\;\text{THEN}\;k\;\text{ELSE}\;0=k\Rightarrow&space;k=k) + +##### Case 2: +![k <= 0 => out ~ Concrete(0)](https://latex.codecogs.com/svg.image?k\leq&space;0\Rightarrow&space;out\sim&space;Concrete(0)) + +RHS: +![out = 0](https://latex.codecogs.com/svg.image?out=0) + +EQUIVALENCE: +![IF false THEN k ELSE 0 = 0 => 0 = 0](https://latex.codecogs.com/svg.image?\text{IF}\;false\;\text{THEN}\;k\;\text{ELSE}\;0=0\Rightarrow&space;0=0) + +## Soundness of Reduction +Let ![IN_0](https://latex.codecogs.com/svg.image?\mathrm{IN_0}) be the Interaction Net translated from a Neural Network ![NN](https://latex.codecogs.com/svg.image?\inline&space;\mathrm{NN}). Let ![IN_n](https://latex.codecogs.com/svg.image?\inline&space;\mathrm{IN_n}) be the state of the net +after ![n](https://latex.codecogs.com/svg.image?\inline&space;n) 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 (![n = 0](https://latex.codecogs.com/svg.image?\inline&space;n=0)): By the [Soundness of Translation](#soundness-of-translation), the initial net ![IN_0](https://latex.codecogs.com/svg.image?\mathrm{IN_0}) 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 ![NN](https://latex.codecogs.com/svg.image?\inline&space;\mathrm{NN}). +- Induction Step (![n -> n + 1](https://latex.codecogs.com/svg.image?\inline&space;n\to&space;n+1)): Assume ![[IN_n] = [NN]](https://latex.codecogs.com/svg.image?\inline&space;[\mathrm{IN_n}]=[\mathrm{NN}]). If ![IN_n](https://latex.codecogs.com/svg.image?\inline&space;\mathrm{IN_n}) is in normal form, the proof is complete. +Otherwise, there exists an active pair ![A](https://latex.codecogs.com/svg.image?\inline&space;A) that reduces ![IN_n to IN_{n+1}](https://latex.codecogs.com/svg.image?\inline&space;\mathrm{IN_n}\Rightarrow&space;\mathrm{IN_{n+1}}). +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. -- cgit v1.2.3