diff options
Diffstat (limited to 'docs/proof.md')
| -rw-r--r-- | docs/proof.md | 562 |
1 files changed, 562 insertions, 0 deletions
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 +\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. |