diff options
Diffstat (limited to '')
| -rw-r--r-- | proof.norg | 367 |
1 files changed, 367 insertions, 0 deletions
diff --git a/proof.norg b/proof.norg new file mode 100644 index 0000000..4ec18ce --- /dev/null +++ b/proof.norg @@ -0,0 +1,367 @@ +@document.meta +title: proof +description: +authors: ericmarin +categories: +created: 2026-03-16T11:34:52 +updated: 2026-03-16T18:31:41 +version: 1.1.1 +@end + +* Proof for translation from Pytorch representation to Interaction Net graph + + +* Proof for the Interaction Rules +** Mathematical Definitions + - Linear(x, q, r) = q*x + r %with q,r Real% + - Concrete(k) = k %with k Real% + - Add(a, b) = a + b + - AddCheckLinear(x, q, r, b) = q*x + (r + b) %with q,r Real% + - AddCheckConcrete(k, b) = k + b %with k Real% + - Mul(a, b) = a * b + - MulCheckLinear(x, q, r, b) = q*b*x + r*b %with q,r Real% + - MulCheckConcrete(k, b) = k*b %with k Real% + - ReLU(x) = IF (x > 0) THEN x ELSE 0 + - Materialize(x) = x + +** Rules +*** Formatting + Agent1 >< Agent2 => Wiring + + LEFT SIDE MATHEMATICAL INTERPRETATION + + RIGHT SIDE MATHEMATICAL INTERPRETATION + + SHOWING EQUIVALENCE + +*** 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) + + Linear(x, q, r) = term + Materialize(term) = out + out = q*x + r + + $$ Case 1: q = 0 => out ~ Concrete(r), x ~ Eraser + Concrete(r) = out + out = r + + 0*x + r = r => r = r + $$ + + $$ Case 2: q = 1, r = 0 => out ~ x + x = out + out = x + + 1*x + 0 = x => x = x + $$ + + $$ Case 3: q = 1 => out ~ TermAdd(x, Concrete(r)) + TermAdd(x, Concrete(r)) = out + out = x + r + + 1*x + r = x + r => x + r = x + r + $$ + + $$ Case 4: r = 0 => out ~ TermMul(Concrete(q), x) + TermMul(Concrete(q), x) = out + out = q*x + + q*x + 0 = q*x => q*x = q*x + $$ + + $$ Case 5: otherwise => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r)) + TermAdd(TermMul(Concrete(q), x), r) = out + out = q*x + r + + q*x + r = q*x + r + $$ + +**** Concrete(k) >< Materialize(out) => out ~ Concrete(k) + + Concrete(k) = term + Materialize(term) = out + out = k + + Concrete(k) = out + out = k + + k = k + +*** Add +**** Linear(x, q, r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r) + + Linear(x, q, r) = a + Add(a, b) = out + out = q*x + r + b + + AddCheckLinear(x, q, r, b) = out + out = q*x + (r + b) + + q*x + r + b = q*x + (r + b) => q*x + (r + b) = q*x + (r + b) + +**** Concrete(k) >< Add(out, b) => (1), (2) + + Concrete(k) = a + Add(a, b) = out + out = k + b + + $$ Case 1: k = 0 => out ~ b + b = out + out = b + + 0 + b = b => b = b + $$ + + $$ Case 2: otherwise => b ~ AddCheckConcrete(out, k) + AddCheckConcrete(k, b) = out + out = k + b + + k + b = k + b + $$ + +**** Linear(y, s, t) >< AddCheckLinear(out, x, q, r) => (1), (2), (3), (4) + + Linear(y, s, t) = b + AddCheckLinear(x, q, r, b) = out + out = q*x + (r + s*y + t) + + $$ Case 1: q,r,s,t = 0 => out ~ Concrete(0), x ~ Eraser, y ~ Eraser + Concrete(0) = out + out = 0 + + 0*x + (0 + 0*y + 0) = 0 => 0 = 0 + $$ + + $$ Case 2: s,t = 0 => out ~ Linear(x, q, r), y ~ Eraser + Linear(x, q, r) = out + out = q*x + r + + 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 + Linear(y, s, t) = out + out = s*y + t + + 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) + Materialize(Linear(x, q, r)) = out_x + Materialize(Linear(y, s, t)) = out_y + Linear(TermAdd(out_x, out_y), 1, 0) = out + out_x = q*x + r + out_y = s*y + t + out = 1*TermAdd(q*x + r, s*y + t) + 0 + Because TermAdd(a, b) is defined as "a+b": + out = 1*(q*x + r + s*y + t) + 0 + + 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) + + Concrete(j) = b + AddCheckLinear(x, q, r, b) = out + out = q*x + (r + j) + + Linear(x, q, r + j) = out + out = q*x + (r + j) + + q*x + (r + j) = q*x + (r + j) + +**** Linear(y, s, t) >< AddCheckConcrete(out, k) => out ~ Linear(y, s, t + k) + + Linear(y, s, t) = b + AddCheckConcrete(k, b) = out + out = k + s*y + t + + Linear(y, s, t + k) + out = s*y + (t + k) + + k + s*y + t = s*y + (t + k) => s*y + (t + k) = s*y + (t + k) + +**** Concrete(j) >< AddCheckConcrete(out, k) => (1), (2) + + Concrete(j) = b + AddCheckConcrete(k, b) = out + out = k + j + + $$ Case 1: j = 0 => out ~ Concrete(k) + Concrete(k) = out + out = k + + k + 0 = k => k = k + $$ + + $$ Case 2: otherwise => out ~ Concrete(k + j) + Concrete(k + j) = out + out = k + j + + k + j = k + j + $$ + +*** Mul +**** Linear(x, q, r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r) + + Linear(x, q, r) = a + Mul(a, b) = out + out = (q*x + r) * b + + MulCheckLinear(x, q, r, b) = out + out = q*b*x + r*b + + (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) + + Concrete(k) = a + Mul(a, b) = out + out = k * b + + $$ Case 1: k = 0 => out ~ Concrete(0), b ~ Eraser + Concrete(0) = out + out = 0 + + 0 * b = 0 => 0 = 0 + $$ + + $$ Case 2: k = 1 => out ~ b + b = out + out = b + + 1 * b = b => b = b + $$ + + $$ Case 3: otherwise => b ~ MulCheckConcrete(out, k) + MulCheckConcrete(k, b) = out + out = k * b + + k * b = k * b + $$ + +**** Linear(y, s, t) >< MulCheckLinear(out, x, q, r) => (1), (2) + + Linear(y, s, t) = b + MulCheckLinear(x, q, r, b) = out + 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) + Concrete(0) = out + out = 0 + + 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) + Materialize(Linear(x, q, r)) = out_x + Materialize(Linear(y, s, t)) = out_y + Linear(TermMul(out_x, out_y), 1, 0) = out + out_x = q*x + r + out_y = s*y + t + out = 1*TermMul(q*x + r, s*y + t) + 0 + Because TermMul(a, b) is defined as "a*b": + out = 1*(q*x + r)*(s*y + t) + 0 + + 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) + + Concrete(j) = b + MulCheckLinear(x, q, r, b) = out + out = q*j*x + r*j + + Linear(x, q * j, r * j) = out + out = q*j*x + r*j + + q*j*x + r*j = q*j*x + r*j + +**** Linear(y, s, t) >< MulCheckConcrete(out, k) => out ~ Linear(y, s * k, t * k) + + Linear(y, s, t) = b + MulCheckConcrete(k, b) = out + out = k * (s*y + t) + + Linear(y, s * k, t * k) = out + out = s*k*y + t*k + + 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) + + Concrete(j) = b + MulCheckConcrete(k, b) = out + out = k * j + + $$ Case 1: j = 0 => out ~ Concrete(0) + Concrete(0) = out + out = 0 + + k * 0 = 0 => 0 = 0 + $$ + + $$ Case 2: j = 1 => out ~ Concrete(k) + Concrete(k) = out + out = k + + k * 1 = k => k = k + $$ + + $$ Case 3: otherwise => out ~ Concrete(k * j) + Concrete(k * j) = out + out = k * j + + 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) + + Linear(x, q, r) = x + ReLU(x) = out + out = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 + + Materialize(Linear(x, q, r)) = out_x + Linear(TermReLU(out_x), 1, 0) = out + out_x = q*x + r + out = 1*TermReLU(q*x + r) + 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 + + 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) + + Concrete(k) = x + ReLU(x) = out + out = IF k > 0 THEN k ELSE 0 + + $$ Case 1: k > 0 => out ~ Concrete(k) + Concrete(k) = out + out = k + + IF true THEN k ELSE 0 = k => k = k + $$ + + $$ Case 2: k <= 0 => out ~ Concrete(0) + Concrete(0) = out + out = 0 + + IF false THEN k ELSE 0 = 0 => 0 = 0 + $$ |