1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
\subsection{Soundness of Reduction}
\label{sec:soundness-of-reduction}
\begin{property}
A valid IN satisfies the following properties:
\begin{itemize}
\item \textbf{Acyclic}: the net forms a forest where the roots are the free wires representing
the network outputs.
\item \textbf{Orientation}: carrier agents always have their principal ports oriented toward the outputs,
while operator and intermediate agents always have their principal ports oriented toward the
inputs. No interaction rule introduces carriers facing the input nor operators or
intermediates facing the output.
\item \textbf{Restricted Interaction}: the net is constructed such that active pairs only occur between a
carrier agent and an operator/intermediate agent. Because of \textbf{Orientation}, neither
carrier nor operator agents interact with agents of the same type. Terminal agents do not
interact with computational operators because they are wrapped in a \textit{Linear} agent.
\end{itemize}
\end{property}
\begin{theorem}
Let $\text{IN}_0$ be the valid IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be
the IN after $n$ reduction steps, then:
\begin{equation}
\forall n \in \mathbb{N} \quad \llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket
\end{equation}
\end{theorem}
\begin{proof}
We will proceed by induction on the number $n$ of reduction steps:
\paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial
$\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly
match the mathematical definition of the ONNX operators in $\text{NN}$; it follows that:
\begin{equation}
\llbracket \text{IN}_{0} \rrbracket = \llbracket \text{NN} \rrbracket
\end{equation}
\paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$.
If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair
$A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}},
the mathematical definition is preserved after any reduction step; it follows that:
\begin{equation}
\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket
\end{equation}
By the inductive hypothesis:
\begin{equation}
\llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{NN} \rrbracket
\end{equation}
By the principle of mathematical induction, $\text{IN}_n$ remains semantically equivalent to the
original $\text{NN}$ at every step of the reduction process.
\end{proof}
\begin{theorem}
For any valid $\text{IN}_0$ translated from a neural network $\text{NN}$, the reduction process
$\text{IN}_0 \to \text{IN}_1 \to \dots \to \text{IN}_n$ reaches a unique normal form, an IN with no active pair, in a
finite number of steps $n$.
\end{theorem}
\begin{proof}
We define a potential function $\Phi$. We need to show that:
\begin{equation}
\Phi(\text{IN}_n) > \Phi(\text{IN}_{n+1}) \quad \forall n \in \mathbb{N}
\end{equation}
The potential function is defined as:
\begin{equation}
\Phi(\text{IN}_n) = \sum_{a \in \text{Agents}(\text{IN}_n)} \begin{cases}
4 + 3^{D-d(a)} & \text{ if }a\text{ is of type computational operator} \\
3 + 3^{D-d(a)} & \text{ if }a\text{ is of type intermediate} \\
1 + 3^{D-d(a)} & \text{ if }a\text{ is a \textit{Materialize} agent} \\
3^{D-d(a)} & \text{ if }a\text{ is of type structural operator} \\
0 & \text{ if }a\text{ is a carrier, terminal}
\end{cases}
\end{equation}
where $d(a)$ is the distance of the agent $a$ from the nearest output wire and $D$ the maximum depth
of $\text{IN}_0$,
We observe that every reduction step $n \to n+1$ strictly reduces $\Phi$:
\begin{itemize}
\item \textbf{Carrier with Computational Operator}: If a carrier $c$ interacts with an operator agent $o$, it
either gets pruned into a new carrier agent closer to the root:
\begin{equation}
\Phi(\text{IN}_n) = 4 + 3^{D-d(c)} > 0 = \Phi(\text{IN}_{n+1})
\end{equation}
or absorbed into an intermediate agent:
\begin{equation}
\Phi(\text{IN}_n) = 4 + 3^{D-d(c)} > 3 + 3^{D-d(c)} = \Phi(\text{IN}_{n+1})
\end{equation}
\item \textbf{Carrier with Intermediate}: If a carrier $c$ interacts with an intermediate agent $i$, it
either gets pruned into a new carrier agent closer to the root:
\begin{equation}
\Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1})
\end{equation}
or temporary Linear agents are wired with \textit{Materialize} agents, which are then forced to
interact to produce terminal agents, then wrapped into a new \textit{Linear} agent:
\begin{equation}
\begin{aligned}
\Phi(\text{IN}_n) &= 3 + 3^{D-d(i)} \\
&> 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} \\
&= 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1})
\end{aligned}
\end{equation}
If the carrier $c$ interacts with a \textit{Materialize} agent $i$:
\begin{equation}
\Phi(\text{IN}_n) = 1 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1})
\end{equation}
\item \textbf{Carrier with Structural Operator}: If a carrier $c$ interacts with a \textit{Dup} or \textit{Eraser}
agent $a$, it traverses the agent structure:
\begin{equation}
\Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
\end{equation}
if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermAdd} or \textit{TermMul}, two new agents are created at
each auxiliary port:
\begin{equation}
\Phi(\text{IN}_n) = 3^{D-d(a)} > 2 * 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
\end{equation}
if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermReLU}, one new agent is created at the
auxiliary port:
\begin{equation}
\Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1})
\end{equation}
if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermConcrete} or \textit{TermSymbolic}, no new agents are
created:
\begin{equation}
\Phi(\text{IN}_n) = 3^{D-d(a)} > 0 = \Phi(\text{IN}_{n+1})
\end{equation}
\end{itemize}
Since $\Phi$ is a non-negative, strictly decreasing function, the reduction
process must terminate in a finite number of steps $n$.
Additionally, since each active pair has exactly one applicable rule, the reduction is
deterministic. Strong confluence follows immediately, meaning that the normal form is unique
regardless of the order in which rules are applied.
\end{proof}
|
