Just-in-Time Piecewise-Linear Semantics for ReLU-type Networks

## Abstract

Abstract We present a JIT PL semantics for ReLU‑type networks that compiles models into a guarded CPWL transducer with shared guards. The system adds hyperplanes only when operands are affine on the current cell, maintains global lower/upper envelopes, and uses a budgeted branch‑and‑bound. We obtain anytime soundness, exactness on fully refined cells, monotone progress, guard‑linear complexity (avoiding global ( k 2 ) \binom{k}{2} ), dominance pruning, and decidability under finite refinement. The shared carrier supports region extraction, decision complexes, Jacobians, exact/certified Lipschitz, LP/SOCP robustness, and maximal causal influence. A minimal prototype returns certificates or counterexamples with cost proportional to visited subdomains.

## 1 Introduction and Positioning

##### Problem & motivation.

For neural networks whose computation DAG is composed of affine modules (FC/conv/mean-pool/inference-time BN/residual) and pointwise gates (ReLU/Leaky-ReLU/PReLU/Abs/Max), each output coordinate is a *continuous piecewise-linear* (CPWL) function of the input. This makes a wide range of geometric and formal tasks—e.g., region extraction, gradients/Jacobians, decision boundaries, Lipschitz analysis, robustness/ equivariance/ equivalence checks, and intervention/repair—*exactly* expressible at the level of CPWL fragments. The bottleneck is *expression explosion*: if we expand the network as a symbolic max/+ tree layer by layer, the number of linear fragments and comparators can grow as $2^{\Theta(N)}$ in the number of gates, making the “compile first, solve later” pipeline infeasible even for medium-size models.

##### Method overview.

We propose a unified symbolic carrier for CPWL networks: (i) a Symbolic Weighted Transducer (SWT) over the *function semiring* $\left(\mathrm{CPWL}^{\pm\infty},\,\oplus=\max,\,\otimes=+\right)$, where edges carry *CPWL weights* and *polyhedral guards*; (ii) a JIT-SWT execution semantics that performs *on-demand refinement* instead of a static global expansion. JIT-SWT maintains a shared DAG of lazy expressions (an e-graph of Max/Sum/Scale/Compose) and a *global guard library*. It inserts threshold/comparator hyperplanes only when a visited GuardSet requires them, constructs local minimal common refinements and winner regions on-the-fly, and always tracks sound *anytime envelopes* $(\underline{A},\overline{A})$ so that $\underline{A}\leq F\leq\overline{A}$ at all times. When all relevant faces inside a queried subdomain have been made explicit and the expression collapses to a single affine map, the envelopes meet and equal the true function—yielding *exactness on demand*.

##### Contributions.

- 1.
CPWL layer calculus and static SWT semantics.
We establish CPWL closure (AF‑1..5) and an *equivalent* network$\to$SWT compilation (SWT‑1).
- 2.
JIT‑SWT objects, invariants, and refiners.
We define the guard library/GuardSets and lazy e‑graph; propose three refiners
(ENSURE_SIGN, ENSURE_WINNER, ENSURE_COMMON_REFINE);
and prove *DYN‑1..6*: sound envelopes; exactness under local full refinement;
no regression; budgeted linear upper bounds in #splits/#new guards; correctness
of dominance pruning; and decidability under finite refinement.
- 3.
Decidable geometry & formal analysis on JIT.
We extract regions/gradients/Jacobians and compute extrema and *exact* Lipschitz
constants; robustness/equivalence/equivariance follow via product constructions and
branch‑and‑bound with certificates; causal interventions admit exact or anytime bounds.
- 4.
Small yet sufficient experiments.
FFN/CNN/GNN demonstrate machine‑precision forward equivalence after local refinement and
practical benefits: FFN—local Lipschitz correlates with FGSM success
(Top‑50 $100\%$ vs Bottom‑50 $14\%$ at $\varepsilon{=}0.25$);
CNN—$85\%$ translation‑equivariance pass with failures at padding boundaries;
GNN—permutation equivariance and Imax‑guided ablations
(Top‑5 removal $-2.94\%$ accuracy; Bottom‑5 $0\%$).

##### Related work.

*Max‑of‑affine/tropical* methods target *convex* CPWL but do not directly capture
general (possibly nonconvex) CPWL with shared guards (Butkovič, 2010).
*Weighted automata* traditionally use discrete alphabets and scalar weights
(Mohri, 2009); our SWT lifts weights to CPWL functions and augments edges
with polyhedral guards.
Neural verification via SMT/MILP/convex relaxations
(Katz et al., 2017; Ehlers, 2017; Tjeng et al., 2019; Wong & Kolter, 2018; Bunel et al., 2020)
is largely solver‑centric and end‑to‑end, lacking a reusable, incrementally refiable
*shared geometric object*. JIT‑SWT serves as that carrier: properties reduce to
finite affine comparisons/LP/SOCP on a *local* common refinement with anytime certificates,
without global enumeration. Our on‑demand refinement echoes
*abstract interpretation*/*CEGAR* (Cousot & Cousot, 1977; Clarke et al., 2000),
but lifted from program states to CPWL geometry with guard‑driven predicates
and certificate‑producing solvers.

Figure: Figure 1: Contribution map and framework overview. Networks $\rightarrow$ SWT (static semantics) $\rightarrow$ JIT‑SWT (on‑demand refinement) $\rightarrow$ unified geometry/verification/causality with anytime certificates and exactness under local full refinement.
Refer to caption: 1.png

**Table 1: Index of core statements. Labels align with the theorem tags used throughout.**
| Label | One‑line meaning (full proofs in the appendix) |
| --- | --- |
| AF‑1..5 | CPWL closure; homomorphism; continuity/convexity; a.e. differentiability; compositionality. |
| SWT‑1 | Equivalent compilation: SWT equals the network pointwise. |
| SWT‑3/4 | Decidable equivalence via common refinement; difference‑region automata. |
| SWT‑5 | Minimal guard complexity exists; decision is NP‑hard. |
| DYN‑1 | Sound anytime envelopes $\underline{A}\leq F\leq\overline{A}$. |
| DYN‑2/3 | Exactness under local full refinement; progress never regresses. |
| DYN‑4 | Budgeted linear upper bounds in #splits/#new guards. |
| DYN‑5 | Correctness of dominance pruning. |
| DYN‑6 | JIT‑decidability under finite refinement; certs/counterexamples. |

## 2 Setup and the Static Baseline: SWT Truth Semantics

##### CPWL and the function semiring (recap).

Let $\mathrm{CPWL}$ denote the class of continuous piecewise-linear real‑valued functions over $\mathbb{R}^{n}$, and let $\mathrm{CPWL}^{\pm\infty}$ further include the everywhere $-\infty$ function.
We work over the *function semiring*

$$ $K_{f}\;=\;\bigl(\mathrm{CPWL}^{\pm\infty},\ \oplus,\ \otimes,\ \mathbf{0},\ \mathbf{1}\bigr),\qquad(f\oplus g)(x)=\max\{f(x),g(x)\},\quad(f\otimes g)(x)=f(x)+g(x),$ $$

with $\mathbf{0}\equiv-\infty$, $\mathbf{1}\equiv 0$.
All network quantities (edge/node weights in the compilation graph) are CPWL functions, and all layerwise combinations are formed with pointwise $\max/+$.

##### AF‑1..AF‑5 (statements only; proofs in App. B ).

- •
AF‑1 (well‑definedness). Under our component set (affine/conv/mean‑pool/inference BN/residual; ReLU/LReLU/PReLU/Abs/Max) and DAG structure, every pre‑activation is CPWL and every activation remains in $K_{f}$.
- •
AF‑2 (pointwise homomorphism). Evaluating the expression at a point $x_{0}$ by the semiring homomorphism $h_{x_{0}}:f\mapsto f(x_{0})$ reproduces the numerical forward pass.
- •
AF‑3 (continuity; sufficient convexity). Outputs are CPWL and hence continuous; if all mixing coefficients entering each activation are nonnegative and the activation is convex and monotone (ReLU/LReLU/PReLU/Max), the network is convex. Abs preserves convexity only when applied directly to an affine atom.
- •
AF‑4 (a.e. differentiability). CPWL functions are affine on a finite polyhedral complex and are differentiable Lebesgue‑a.e.; Clarke subdifferentials at boundaries equal convex hulls of adjacent gradients.
- •
AF‑5 (closure under composition). Finite compositions of “affine + the above gates” remain CPWL.

##### Symbolic Weighted Transducer (SWT): static truth semantics.

We compile a network into a *guarded* symbolic weighted transducer

$$ $A=(Q,q_{\mathrm{in}},F,E,\ \mathsf{G},\mathsf{W},\ K_{f}).$ $$

Here $Q$ are states (structural sites / template instances), $q_{\mathrm{in}}\in Q$ is the initial state, $F\subseteq Q$ are final states, and $E\subseteq Q\times Q$ are directed edges.
Each edge $e\in E$ carries a *polyhedral guard* $\mathsf{G}(e)=\{x:Ax\leq d\}$ in H‑form drawn from a global guard library $\mathcal{H}$ (each normalized inequality is registered once), and a *CPWL weight* $\mathsf{W}(e)\in K_{f}$ (node weights similarly).
A path $\pi=e_{1}\ldots e_{T}$ is feasible at $x$ if $x\in\bigcap_{t}\mathsf{G}(e_{t})$, and its value is

$$ $\mathsf{val}_{A}(\pi,x)=\mathsf{W}(q_{\mathrm{in}})(x)\ \otimes\ \Bigl(\bigotimes_{t=1}^{T}\mathsf{W}(e_{t})(x)\Bigr)\ \otimes\ \mathsf{W}(q_{T})(x).$ $$

The SWT output is the semiring sum over feasible paths,

$$ $A(x)=\bigoplus_{\pi:\ q_{\mathrm{in}}\to F,\ x\models\pi}\ \mathsf{val}_{A}(\pi,x).$ $$

###### Theorem 2.1 (SWT‑1: equivalent compilation; proof in App. C.2 ) .

For any network $F$ built from our component set and any input $x$ in the domain,
the SWT $A_{F}$ obtained by the rules below satisfies $A_{F}(x)=F(x)$.

*One‑line essence.* Affine branches compose by $\otimes(=+)$ along paths; gate choices and pooling reduce to $\oplus(=\max)$ over guarded winners, so path‑wise accumulation and path‑set maximization match the numerical forward semantics pointwise.

###### Theorem 2.1 (SWT‑1: equivalent compilation; proof in App. C.2 ) .

##### Compilation rules at a glance (details in App. C.1 ).

We compile layer‑by‑layer while reusing the shared guard library $\mathcal{H}$ and never materializing global region partitions:

- 1.
Affine / residual / inference‑time BN.
For a fragment $(C,w,b)$ (guard $C$, affine $x\mapsto w^{\top}x+b$), an affine map $y=Wx+b_{0}$ yields $(C,\ \tilde{w}=Ww,\ \tilde{b}=Wb+b_{0})$.
Inference‑time BN is merged into the affine.
Residual sums become $\otimes$‑sums on the common guard $C$.
- 2.
ReLU / Leaky‑ReLU / PReLU / Abs (pointwise gates).
Introduce two guarded branches on $z(x)=w^{\top}x+b$:
$\text{(pos)}\;C^{+}=C\cap\{z\geq 0\}\ \leadsto\ (w,b),\qquad\text{(neg)}\;C^{-}=C\cap\{z\leq 0\}\ \leadsto\ \begin{cases}(0,0)&\text{ReLU}\\
(\alpha w,\alpha b)&\text{LReLU/PReLU}\\
(-w,-b)&\text{Abs}\end{cases}$
using *closed* guards ($\geq,\leq$) to keep ties on both sides; $\oplus$ resolves equality.
- 3.
Pointwise Max / MaxPool.
Given candidates $\{(C_{i},w_{i},b_{i})\}_{i=1}^{k}$ with common support $C_{\cap}=\bigcap_{i}C_{i}$, add comparators $\{(w_{i}{-}w_{j})^{\top}x+(b_{i}{-}b_{j})\geq 0\}$ to $\mathcal{H}$ and select the winner region
$C_{i}^{\star}=C_{\cap}\cap\bigcap_{j\neq i}\{(w_{i}-w_{j})^{\top}x+(b_{i}-b_{j})\geq 0\},\quad\text{carrying }(w_{i},b_{i}).$
- 4.
Convolution / mean‑pool.
Instantiate a per‑location *template* with *sliding‑window guards* encoding stride/padding; share kernel parameters by aliasing to avoid numeric duplication. Mean‑pool is affine.
- 5.
GNN (fixed graph).
Sum/mean aggregation compiles to sparse affine maps (template per node); max aggregation uses comparator guards; node‑MLPs follow the same affine+gate rules.
- 6.
Normalization.
All guard rows are $\ell_{2}$‑normalized; we adopt closed‑set convention throughout.

##### Size and acyclicity (informal SWT‑2; constants in App. C.3 ).

Because the network DAG compiles forward without back‑edges and guards are stored by *indices* into the shared library (we do not use regions as states), the SWT is acyclic; the number of states grows linearly with the number of affine sublayers and convolutional template instances, while the number of edges/guards is linear in these plus the number of *introduced comparator hyperplanes*.
This avoids per‑path duplication and isolates the exponential blow‑up solely to the (optional) global enumeration of winner comparisons—which we *do not* perform in the static object.

Figure: Figure 2: Static SWT compilation pipeline. Layer $\rightarrow$ guard intersections $\rightarrow$ candidate fragments $\rightarrow$ comparator guards $\rightarrow$ winner regions.
Refer to caption: 2.png

## 3 Dynamic Compilation (JIT–SWT): Objects, Refiners, and Guarantees

##### Objects and invariants.

We endow the static SWT (§2) with a *JIT* (on‑demand) execution semantics.
Let $\mathcal{H}=\{h_{\ell}(x):a_{\ell}^{\top}x\leq d_{\ell}\}_{\ell=1}^{M}$ be the global
*guard library* where each normalized halfspace is registered once.
A *GuardSet* is an ordered finite index set $S\subseteq\{1,\dots,M\}$
representing the polyhedron
$C(S)=\bigcap_{\ell\in S}\{x:\ a_{\ell}^{\top}x\leq d_{\ell}\}$.
Lazy expressions (*scalar* case) are e‑graph nodes with syntax

$$ $\texttt{Expr}\ ::=\ \texttt{Affine}(w,b)\mid\texttt{Sum}(\mathcal{E})\mid\texttt{Max}(\mathcal{E})\mid\texttt{Scale}(c,E)\mid\texttt{Bias}(b,E),$ $$

shared by structure hashing/union‑find.
Vector outputs use a componentwise family of scalar Exprs.

Invariants (I–III).
*I: unique guards.* Each inequality in $\mathcal{H}$ appears once; edges store
*indices* only (no explicit path intersections).
*II: on‑demand refinement.* New threshold/comparator hyperplanes are inserted
*only* on the *visited* GuardSet $S$, splitting $S$ locally into
$S\cup\{\ell\}$ and $S\cup\{\bar{\ell}\}$; no global pre‑partitioning.
*III: anytime envelopes.* At all times we maintain

$$ $\underline{A},\overline{A}:\ \ \forall x\in\mathcal{D},\qquad\underline{A}(x)\ \leq\ A(x)\ \leq\ \overline{A}(x),$ $$

where $A$ is the static SWT semantics (truth semantics). Envelopes are
propagated compositionally from local *LB/UB* on Exprs (below).

##### LB/UB oracle (structure rules).

For any GuardSet $S$ and expression $E$ we compute interval
$[\operatorname{LB}(E,S),\,\operatorname{UB}(E,S)]$ sound for $C(S)$: (^1^11Upgrades to exact LP/SOCP bounds are permitted anytime; proofs of soundness/monotonicity are in App. [D](https://arxiv.org/html/2510.17622v1#A4))

$$ $\displaystyle\operatorname{LB}(\texttt{Affine}(w,b),S)=\min_{x\in C(S)}w^{\top}x+b,\quad\operatorname{UB}(\texttt{Affine}(w,b),S)=\max_{x\in C(S)}w^{\top}x+b\ \ \text{(LP)};$ $\displaystyle\operatorname{LB}(\texttt{Sum}(\{E_{k}\}),S)=\sum_{k}\operatorname{LB}(E_{k},S),\quad\operatorname{UB}(\texttt{Sum}(\{E_{k}\}),S)=\sum_{k}\operatorname{UB}(E_{k},S);$ $\displaystyle\operatorname{LB}(\texttt{Scale}(c,E),S)=\!\!,\quad\operatorname{UB}(\texttt{Scale}(c,E),S)=\!\!;$ $\displaystyle\operatorname{LB}(\texttt{Bias}(b,E),S)=\operatorname{LB}(E,S)+b,\quad\operatorname{UB}(\texttt{Bias}(b,E),S)=\operatorname{UB}(E,S)+b;$ $\displaystyle\operatorname{LB}(\texttt{Max}(\{E_{k}\}),S)=\max_{k}\operatorname{LB}(E_{k},S),\quad\operatorname{UB}(\texttt{Max}(\{E_{k}\}),S)=\max_{k}\operatorname{UB}(E_{k},S).$ $$

##### Atomic refiners (3–5 lines each; full details in App. D.2 ).

*(i) ENSURE_SIGN$(z{=}\texttt{Expr},S)$:*
if $\operatorname{UB}(z,S)\leq 0$ commit the negative branch; if $\operatorname{LB}(z,S)\geq 0$
commit the positive; otherwise insert the threshold guard $\{z\geq 0\}$ into $\mathcal{H}$
(if absent) and split $S$ into $S^{\pm}$.
*(ii) ENSURE_WINNER$(\{E_{i}\},S)$:*
compute $[\mathrm{LB/UB}(E_{i},S)]$; prune dominated candidates $\{i:\ \max_{j}\operatorname{LB}(E_{j},S)\geq\operatorname{UB}(E_{i},S)\}$; if a unique $i^{\star}$ remains with $\operatorname{LB}(E_{i^{\star}},S)\geq\max_{j\neq i^{\star}}\operatorname{UB}(E_{j},S)$,
commit $i^{\star}$; else add one comparator $\{E_{p}\geq E_{q}\}$ chosen by a gap heuristic
and split $S$.
*(iii) ENSURE_COMMON_REFINE$(S;S_{1},S_{2})$:*
incrementally insert faces from $(S_{1}\cup S_{2})\setminus S$ until the relevant
sub‑expressions are comparable/addable on each child.

Figure: Algorithm 1 JIT–SWT Branch-and-Bound (B&B) driver (anytime)

##### Anytime envelopes and monotonicity.

###### Lemma 3.1 (Monotone envelope updates; App. D.1 ) .

Adding guards (shrinking $C(S)$) or tightening local bounds makes
$\underline{A}$ *nondecreasing* and $\overline{A}$ *nonincreasing* pointwise;
in particular $\underline{A}\leq A\leq\overline{A}$ is preserved.

###### Theorem 3.2 (DYN‑1: sound anytime envelopes; App. D.1 ) .

At any time during JIT execution, $\underline{A}(x)\leq A(x)\leq\overline{A}(x)$ holds over $\mathcal{D}$.

###### Lemma 3.1 (Monotone envelope updates; App. D.1 ) .

###### Theorem 3.2 (DYN‑1: sound anytime envelopes; App. D.1 ) .

##### Anytime exactness and no regression.

###### Definition 3.3 (Local full refinement) .

A GuardSet $S$ is *locally fully refined* if (i) all gate/comparator faces relevant to $S$
have been added to $\mathcal{H}$, and (ii) each output Expr collapses to a *single affine* on $C(S)$.

###### Theorem 3.4 (DYN‑2: exactness on $C(S)$ ; App. D.2 ) .

If $S$ is locally fully refined, then on $C(S)$ we have $\underline{A}=\overline{A}=A$.

###### Theorem 3.5 (DYN‑3: progress never regresses; App. D.2 ) .

Refining a GuardSet $S$ either keeps it as a tighter leaf (with tighter LB/UB) or splits it into children; previously exact regions remain exact and are never invalidated.

###### Definition 3.3 (Local full refinement) .

###### Theorem 3.4 (DYN‑2: exactness on C ​ ( S ) C(S) ; App. D.2 ) .

###### Theorem 3.5 (DYN‑3: progress never regresses; App. D.2 ) .

##### Budgeted complexity upper bounds.

###### Theorem 3.6 (DYN‑4; App. D.4 ) .

Let $B_{\textsf{split}}$ be the number of local splits and $B_{\textsf{guard}}$ the number of newly inserted hyperplanes (beyond the initial library size $|\mathcal{H}_{0}|$).
Then: (i) the number of active GuardSets is $\leq 1+B_{\textsf{split}}$; (ii) $|\mathcal{H}|\leq|\mathcal{H}_{0}|+B_{\textsf{guard}}$; (iii) the SWT node/edge count grows $O(N_{\mathrm{lin}}+T_{\mathrm{conv}}+B_{\textsf{guard}})$; (iv) the number of LP/SOCP calls is $O(B_{\textsf{split}}+B_{\textsf{guard}}+|Q|)$ under per‑step constant‑candidate policies.

###### Theorem 3.6 (DYN‑4; App. D.4 ) .

##### Dominance pruning.

###### Proposition 3.7 (DYN‑5; App. D.3 ) .

On $S$, if $\max_{x\in C(S)}(E_{\pi}(x)-E_{\pi^{\prime}}(x))\leq 0$ (e.g., obtained by an LP), then candidate $\pi$ can never win any max/gate on $C(S)$ and may be safely pruned from $S$’s candidate set.

###### Proposition 3.7 (DYN‑5; App. D.3 ) .

##### Decidability and tri‑valued answers.

###### Theorem 3.8 (DYN‑6: JIT‑decidability; App. D.3 ) .

For properties expressible with finitely many affine and second‑order cone constraints, if the JIT strategy is *fair* (every feasible, not‑yet fully refined GuardSet is eventually selected) and only finitely many faces can be added, then the B&B process decides the property: it returns either a *proof* (certificate $\operatorname{LB}\geq 0$ on a finite cover), or a *counterexample* (witness from $\operatorname{UB}<0$ on some $S$), otherwise *unknown* under budget—always sound thanks to Thm. [D.4](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem4).

###### Theorem 3.8 (DYN‑6: JIT‑decidability; App. D.3 ) .

##### Static–dynamic pointwise equivalence.

###### Definition 3.9 (Complete refinement cover) .

A finite family $\mathcal{S}=\{S_{t}\}$ is a complete refinement cover of $D$ if $D\subseteq\bigcup_{t}C(S_{t})$ and each $S_{t}$ is locally fully refined.

###### Theorem 3.10 (DYN‑7; App. D.3 ) .

If $D$ admits a complete refinement cover $\mathcal{S}$, then $\forall x\in D$:
$A_{\textsf{JIT}}(x)=A_{\textsf{stat}}(x)=F(x)$.

###### Definition 3.9 (Complete refinement cover) .

###### Theorem 3.10 (DYN‑7; App. D.3 ) .

##### Notes on ties and numerics.

All threshold/comparator guards are treated as closed ($\geq,\leq$), which guarantees coverage of $z{=}0$ events; implementations may use a small tolerance $\tau$ to handle floating‑point ties without affecting the formal semantics (App. [G](https://arxiv.org/html/2510.17622v1#A7)).

## 4 Decidable Analysis and Function Geometry on JIT

We now show how geometry (regions/gradients/Jacobians, extrema/Lipschitz) and
formal tasks (verification, equivariance, causality) become *decidable*
on top of the JIT–SWT semantics from §3. Throughout, proofs and full
algorithms are deferred to Appendix E–F.

### 4.1 Regions, Gradients, and Jacobians (GEO‑1/4)

##### Active fragments and local exactness.

Recall (Def. [3.3](https://arxiv.org/html/2510.17622v1#S3.Thmtheorem3)) that a GuardSet $S$ is *locally fully refined*
when all faces relevant to $S$ are present and every output expression collapses to a
single affine map on $C(S)$. In this case we write the scalar output as
$F(x)=w_{S}^{\top}x+b_{S}$ on $C(S)$ (or componentwise $F_{i}(x)=w_{S,i}^{\top}x+b_{S,i}$).

###### Theorem 4.1 (GEO‑1: on‑demand region extraction; App. E.1 ) .

Running JIT refinement restricted to a domain $D$ returns a set of *active fragments*
$\{(S_{\rho},w_{\rho},b_{\rho})\}_{\rho}$ whose (relative‑interior) union covers the visited
portion of $D$, and on each $C(S_{\rho})$ the function equals the affine law
$F(x)=w_{\rho}^{\top}x+b_{\rho}$.
If refinement continues until $D$ is covered by finitely many locally fully refined
GuardSets, this yields a complete CPWL region table for $F$ on $D$.

###### Theorem 4.1 (GEO‑1: on‑demand region extraction; App. E.1 ) .

##### Gradients/Jacobians and boundary representatives.

On the relative interior of each $C(S_{\rho})$, the gradient/Jacobian is constant:
$\nabla F(x)=w_{\rho}$ (or $J_{F}(x)=J_{\rho}$ for vector outputs).
At polyhedral boundaries, $F$ is not differentiable in general; we use Clarke
subdifferentials.

###### Theorem 4.2 (GEO‑4: a.e. exact Jacobian; App. E.1 ) .

Lebesgue‑a.e. $x\in D$ lies in the relative interior of some refined $C(S_{\rho})$,
and the JIT extractor returns $\nabla F(x)$ (or $J_{F}(x)$) exactly.
If $x$ lies on a boundary, a selection rule (e.g., minimum‑norm element from the
convex hull of adjacent gradients, obtained by a tiny QP) yields a representative
in the Clarke subdifferential.

###### Theorem 4.2 (GEO‑4: a.e. exact Jacobian; App. E.1 ) .

##### Practical readout on JIT.

Once $S$ is locally fully refined, we read $(w_{S},b_{S})$ by summing affine atoms
along the unique acyclic path fragments that remain active on $C(S)$.
For vector outputs we assemble $J_{S}$ row‑wise.

### 4.2 Extrema and Lipschitz (GEO‑2/5)

##### Anytime maxima/minima.

Let $D$ be a convex domain (box/polytope/$\ell_{p}$ ball).
JIT–B&B maintains

$$ $\underline{M}=\max_{S\subseteq D}\operatorname{LB}(F,S),\qquad\overline{M}=\max_{S\subseteq D}\operatorname{UB}(F,S),$ $$

which satisfy $\underline{M}\leq\max_{x\in D}F(x)\leq\overline{M}$ and tighten
monotonically (Thm. [D.4](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem4)).
When all visited $S$ are locally fully refined, each subproblem reduces to
affine maximization on a convex set, solved exactly by LP or SOCP.

###### Theorem 4.3 (GEO‑2: exact extrema after local refinement; App. E.3 ) .

If $D$ is covered by locally fully refined GuardSets $\{S\}$, then

$$ $\max_{x\in D}F(x)=\max_{S}\ \max_{x\in C(S)\cap D}\ \big(w_{S}^{\top}x+b_{S}\big),$ $$

with LP for polytope/$\ell_{\infty}$/$\ell_{1}$, SOCP for $\ell_{2}$ or polytope$\cap\ell_{2}$;
the minima are analogous.

###### Theorem 4.3 (GEO‑2: exact extrema after local refinement; App. E.3 ) .

##### Lipschitz constants.

For scalar $F$, the exact $L_{p}$ on $D$ equals the maximum dual‑norm of local gradients.
For vector $F:\ell_{p}\to\ell_{r}$, it equals the maximum operator norm of local Jacobians.

###### Theorem 4.4 (GEO‑5: piecewise maximum formula; App. E.4 ) .

If $D$ is covered by locally fully refined $\{S\}$, then

$$ $L_{p}(F;D)=\max_{S:\,C(S)\cap D\neq\varnothing}\ \|w_{S}\|_{p^{*}},\qquad L_{p\to r}(F;D)=\max_{S:\,C(S)\cap D\neq\varnothing}\ \|J_{S}\|_{p\to r}.$ $$

Before full refinement, JIT provides anytime bounds
$\underline{L}\leq L\leq\overline{L}$ by combining exact values on refined leaves
with sound relaxations on unresolved leaves (LP/SOCP based).

###### Theorem 4.4 (GEO‑5: piecewise maximum formula; App. E.4 ) .

### 4.3 Verification, Equivariance, and Causality (VER/CAU)

##### Property language and product construction.

We consider properties expressed by finite combinations of:
input constraints $x\in D$ (box/polytope/$\ell_{p}$ ball),
output thresholds/intervals $F_{k}(x)\leq u,\,F_{k}(x)\geq\ell$,
classification margins $F_{y}-\max_{j\neq y}F_{j}\geq\gamma$,
and relational constraints $|F(x)-F^{\prime}(x)|\leq\varepsilon$.
Each atomic constraint is compiled into a *counterexample transducer*
and composed (product) with the SWT of $F$, yielding a CPWL objective $g$ whose
violation corresponds to counterexamples. JIT–B&B on $g$ returns a tri‑valued
answer with certificates (Thm. [D.11](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem11)).

###### Theorem 4.5 (VER‑1: decidable specification checking; App. F.1 ) .

For the above property language, JIT–B&B returns True (with per‑leaf
LB certificates), False (with a witness point from LP/SOCP on some leaf),
or Unknown under budget—always sound and complete under finite refinement.

###### Theorem 4.5 (VER‑1: decidable specification checking; App. F.1 ) .

##### Robustness certification.

For a labeled sample $(x_{0},y)$, define the margin
$g(x)=F_{y}(x)-\max_{j\neq y}F_{j}(x)$. Over $B_{p}(x_{0},\epsilon)\cap D$, JIT refines
until $g$ is affine on leaves and solves
$\min g(x)$ by LP/SOCP per leaf. The minimum bound across leaves certifies
robustness; a negative minimum yields a counterexample.

###### Theorem 4.6 (VER‑2: robustness via JIT; App. F.2 ) .

On $B_{p}(x_{0},\epsilon)\cap D$, the JIT procedure produces an anytime lower bound
on the margin and, upon local full refinement, the *exact* minimum. Hence
“$g\geq\gamma$” is decidable under finite refinement with a certificate or a witness.

###### Theorem 4.6 (VER‑2: robustness via JIT; App. F.2 ) .

##### Equivariance checks.

Given input transform $\mathcal{T}_{g}$ and output transform $\mathcal{T}^{\prime}_{g}$
(e.g., CNN translations within an effective domain, or GNN permutations),
we check $H(x)=F(\mathcal{T}_{g}x)-\mathcal{T}^{\prime}_{g}(F(x))$.
Running JIT–B&B on $|H|$ over the appropriate domain yields either a uniform
upper bound $\leq\varepsilon$ with certificates, or an explicit violating input.

###### Theorem 4.7 (VER‑3: (approximate) equivariance; App. F.3 ) .

Over the effective domain, JIT decides exact equivariance ($H\equiv 0$) or
$\varepsilon$‑equivariance ($\|H\|_{\infty}\leq\varepsilon$) under finite refinement,
with counterexamples or per‑leaf bounds as certificates.

###### Theorem 4.7 (VER‑3: (approximate) equivariance; App. F.3 ) .

##### Causal interventions and maximal influence.

Consider an intervention that replaces a sub‑expression in the DAG by a CPWL policy
$P_{c}$, producing $F_{C}$ (App. [F.4](https://arxiv.org/html/2510.17622v1#A6.SS4)). Since CPWL is closed under the operations we use,
$g_{C}(x)=F(x)-F_{C}(x)$ is CPWL. The *maximal causal influence* on $D$ is

$$ $I_{\max}(C;D)=\sup_{x\in D}\ |g_{C}(x)|,$ $$

which JIT computes by running B&B on $g_{C}$ and $-g_{C}$ with anytime
bounds $\underline{I}\leq I_{\max}\leq\overline{I}$ and exact value upon full
refinement.

###### Theorem 4.8 (CAU‑1/2: decidable interventions; App. F.4 ) .

For CPWL interventions $C$ and convex $D$, JIT–B&B yields sound anytime bounds
on $I_{\max}(C;D)$ and the exact value once refined leaves cover $D$.

###### Theorem 4.8 (CAU‑1/2: decidable interventions; App. F.4 ) .

##### Notes on solvers and domains.

Affine maximization over boxes/polyhedra uses LP; over $\ell_{2}$ balls or polytope$\cap\ell_{2}$
uses SOCP; pure $\ell_{2}$ admits the closed form $w^{\top}x_{0}+b+\epsilon\|w\|_{2}$.
All calls are *local* to refined leaves; hence the global complexity follows the budgeted
bounds of Thm. [D.13](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem13).

Figure: Figure 3: Task–spec–solver map. Properties are compiled into CPWL objectives via product constructions and discharged on JIT leaves by small LP/SOCPs (and MIP when indicator constraints are explicitly encoded). The JIT envelopes provide anytime certificates; local full refinement gives exact answers.
Refer to caption: 3.png

## 5 Experiments

We report three small yet sufficient studies that exercise JIT–SWT on FFNs, CNNs, and GNNs, focusing on (i) *forward equivalence* to the original PyTorch models after local refinement, and (ii) one geometry/formal task per setting. To save space we summarize the key numbers here; the representative visuals are in Figs. [5](https://arxiv.org/html/2510.17622v1#A8.F5), [7](https://arxiv.org/html/2510.17622v1#A8.F7), [12](https://arxiv.org/html/2510.17622v1#A8.F12) and full setup is deferred to the appendix [H](https://arxiv.org/html/2510.17622v1#A8).

FFN (MNIST): local Lipschitz & robustness.
For correctly classified test samples, we JIT‑compile a local affine law $x\mapsto Wx+b$ per input and take $\|W\|_{2}$ as the *local* Lipschitz.
We find *machine‑precision* forward equivalence (avg. abs. error $1.13{\times}10^{-6}$) and a wide spread of local‑$L$ (most between 2–7; see [Figure 5](https://arxiv.org/html/2510.17622v1#A8.F5)).
Sorting by local‑$L$, the *Top‑50* most sensitive points exhibit 100% FGSM success at $\varepsilon{=}0.25$, vs. 14% on the *Bottom‑50*, confirming a strong correlation between local sensitivity and adversarial fragility.

CNN (CIFAR‑10 subset): translation equivariance.
On a small conv net with stride$=1$, padding$=1$, we verify forward equivalence on random samples (avg. abs. error $1.36{\times}10^{-7}$), then test $8$ integer shifts $\Delta\in\{-1,0,1\}^{2}\!\setminus\{(0,0)\}$. The *equivariance pass rate* is 85%.
Failures (58 total) concentrate at diagonal shifts ([Figure 7](https://arxiv.org/html/2510.17622v1#A8.F7)), consistent with boundary effects from zero padding that propagate through ReLU and global pooling.(^2^22Ablations with different padding fill values are in the appendix; the conclusion is robust.)

GNN (Karate Club): permutation equivariance & causal Imax.
For a 2‑layer GCN we obtain near‑exact forward equivalence (mean error $2.17{\times}10^{-6}$) and near‑exact permutation equivariance over 50 random permutations (mean error $6.80{\times}10^{-15}$).
We then compute *Imax* per hidden channel by intervening $h^{(2)}_{\cdot,k}\!\leftarrow\!0$ and running JIT–B&B over $\|\!\cdot\!\|_{\infty}$‑bounded input neighborhoods.
Channels ranked *Top‑5* by Imax cause a 2.94% accuracy drop when removed (vs. 0% for *Bottom‑5*); see [Figure 11](https://arxiv.org/html/2510.17622v1#A8.F11) for the distribution and [Figure 12](https://arxiv.org/html/2510.17622v1#A8.F12) for ablation bars.

Table: Table 2: One-page summary. Forward equivalence is at machine precision across all settings. Each geometry/formal task is discharged on JIT leaves by small LP/SOCPs, with anytime bounds and exactness upon local refinement.

##### Takeaways.

(i) JIT–SWT attains precise *per‑sample* linearization that is numerically identical to the original networks after local refinement; (ii) geometry is actionable—local Lipschitz pinpoints adversarially fragile points; (iii) JIT formal analysis scales to structure: translation equivariance violations are localized to padding faces; (iv) causal Imax separates crucial GNN channels from redundant ones and predicts ablation impact.

## 6 Conclusion and Limitations

##### Summary.

We introduced *SWT*, a symbolic carrier over the CPWL (max,+) semiring with polyhedral guards, and *JIT–SWT*, an on‑demand semantics that shares an expression DAG, inserts faces only on visited cells, and maintains sound anytime envelopes. Geometry and formal tasks—region/gradient/Jacobian extraction, extrema and exact/certified Lipschitz, robustness/equivalence/equivariance, and causal interventions—reduce to small LP/SOCP subproblems on local common refinements, yielding certificates or counterexamples without global enumeration. Compact FFN/CNN/GNN case studies demonstrate machine‑precision agreement and practical value.

##### Limitations.

(i) Guarantees cover DAGs with affine modules and pointwise max‑type gates; multiplicative modules (attention, LSTM/GRU) and training‑time BN fall outside CPWL and need sound PL relaxations. (ii) Decidability assumes *finite* refinements and a *fair* selection policy; under budgets we return a sound tri‑valued answer (True/False/Unknown). (iii) Influence‑type upper bounds derived from single‑fragment linearization are non‑certified unless the leaf is fully refined or tightened by a guard‑aware refinement.

##### Future work.

Certified PL lifts for multiplicative modules; compositional verified training/repair; parallel and learned refinement; matrix‑free Jacobian extraction for large conv/GNNs; richer property languages (temporal/relational) and tighter anytime relaxations with certificates.

## References

- Bunel et al. (2020)
Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip H. S. Torr, Pushmeet Kohli, and M. Pawan Kumar.
Branch and bound for piecewise linear neural network verification.
*arXiv preprint arXiv:1909.06588*, 2020.
- Butkovič (2010)
Peter Butkovič.
*Max-linear Systems: Theory and Algorithms*.
Springer London, 2010.
- Clarke et al. (2000)
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith.
Counterexample-guided abstraction refinement.
In *Computer Aided Verification (CAV)*, volume 1855 of *Lecture Notes in Computer Science*, pp. 154–169. Springer, 2000.
- Cousot & Cousot (1977)
Patrick Cousot and Radhia Cousot.
Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.
In *Proc. of the 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)*, pp. 238–252. ACM Press, 1977.
- Ehlers (2017)
Rüdiger Ehlers.
Formal verification of piece-wise linear feed-forward neural networks.
In *Automated Technology for Verification and Analysis (ATVA)*, volume 10482 of *Lecture Notes in Computer Science*, pp. 269–286. Springer, 2017.
- Katz et al. (2017)
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer.
Reluplex: An efficient SMT solver for verifying deep neural networks.
In *Computer Aided Verification (CAV)*, volume 10426 of *Lecture Notes in Computer Science*, pp. 97–117. Springer, 2017.
- Mohri (2009)
Mehryar Mohri.
Weighted automata algorithms.
In M. Droste, W. Kuich, and H. Vogler (eds.), *Handbook of Weighted Automata*, pp. 213–254. Springer, 2009.
- Tjeng et al. (2019)
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake.
Evaluating robustness of neural networks with mixed integer programming.
In *International Conference on Learning Representations (ICLR)*, 2019.
- Wong & Kolter (2018)
Eric Wong and J. Zico Kolter.
Provable defenses against adversarial examples via the convex outer adversarial polytope.
In *Proceedings of the 35th International Conference on Machine Learning (ICML)*, volume 80, pp. 5286–5295. PMLR, 2018.

## Appendix A Notation, Domains, and the Guard Library

This appendix fixes notations, domain conventions, and the canonicalization
rules for the global *guard library* used by SWT and JIT–SWT.
All statements here are design-level and compatible with the truth semantics in §2
and the JIT semantics in §3.

##### Basic sets and operators.

For a set $S\subseteq\mathbb{R}^{n}$, let $\operatorname{ri}(S)$, $\partial S$, and
$\operatorname{aff}(S)$ denote its relative interior, boundary, and affine hull.
For a family $\{S_{i}\}$, write $\bigcap S_{i}$ and $\bigcup S_{i}$ for intersection and union.
The indicator $\mathbb{I}[\cdot]$ takes values in $\{0,1\}$.

### A.1 Domains and norms

###### Definition A.1 (Input domains) .

We work with convex input domains $D\subseteq\mathbb{R}^{n}$ of the following types:

- 1.
Box/polytope (H–form).
$D=\{x\in\mathbb{R}^{n}:A_{D}x\leq d_{D}\}$ with $A_{D}\in\mathbb{R}^{m\times n}$.
- 2.
$\ell_{p}$ balls.
$D=B_{p}(x_{0},\epsilon)=\{x:\|x-x_{0}\|_{p}\leq\epsilon\}$ for $p\in\{1,2,\infty\}$.

When $D$ is not polyhedral (e.g., $p=2$), we treat $D$ as a second–order cone
constraint in local LP/SOCP subproblems; only *linear* faces are stored in the
global guard library (§[A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)).

###### Definition A.2 (Norms and duals) .

For $p\in[1,\infty]$, let $\|\cdot\|_{p}$ be the vector $p$–norm and $p^{*}$ its dual with
$1/p+1/p^{*}=1$ (by convention $1/\infty=0$). For a matrix or linear map $J$,
$\|J\|_{p\to r}=\sup_{\|v\|_{p}=1}\|Jv\|_{r}$.
We use the standard closed forms when applicable:
$\|J\|_{1\to 1}=\max_{j}\sum_{i}|J_{ij}|$,
$\|J\|_{\infty\to\infty}=\max_{i}\sum_{j}|J_{ij}|$, and
$\|J\|_{2\to 2}=\sigma_{\max}(J)$.

###### Definition A.1 (Input domains) .

###### Definition A.2 (Norms and duals) .

### A.2 Polyhedral guards in H–form and closed–set semantics

A (closed) halfspace is encoded by a normalized pair $(a,d)\in\mathbb{R}^{n}\times\mathbb{R}$ as

$$ $h(x)\;:\;a^{\top}x\leq d.$ $$

A polyhedron in H–form is an intersection of finitely many closed halfspaces.
We always interpret gate thresholds and comparator faces with *closed* inequalities
($\geq$ and $\leq$ on appropriate sides), so that “ties” (equality cases) belong to
both sides and are resolved semantically by $\oplus=\max$ in the function semiring.

### A.3 The global guard library ℋ \mathcal{H} : canonicalization and uniqueness

##### Normalization.

Each linear inequality is stored once in a global library
$\mathcal{H}=\{h_{\ell}(x):a_{\ell}^{\top}x\leq d_{\ell}\}_{\ell=1}^{M}$ under the following
canonicalization:

- 1.
Row normalization: $\|a_{\ell}\|_{2}=1$.
- 2.
Sign canonicalization: if the first nonzero entry of $a_{\ell}$ is negative,
multiply both sides by $-1$ to make it nonnegative; this makes
$(a,d)\sim(\alpha a,\alpha d)$ with $\alpha>0$ share a unique representative.
- 3.
Tie policy: for a threshold $\{z\geq 0\}$ we register *both* orientations
$\{z\geq 0\}$ and $\{z\leq 0\}$ as distinct indices, so equality is covered on either side.
We denote the reverse orientation of $\ell$ by $\bar{\ell}$.

##### Comparator faces.

For two affine forms $f(x)=w_{f}^{\top}x+b_{f}$ and $g(x)=w_{g}^{\top}x+b_{g}$,
the comparator face $\{f\geq g\}$ is represented by
$\big((w_{f}{-}w_{g}),\,(b_{f}{-}b_{g})\big)$ and normalized as above before insertion.

##### Storage discipline.

Edges in SWT/JIT store *only indices* into $\mathcal{H}$; intersections are not
materialized on edges (no “region as state”), cf. §2.3.

### A.4 GuardSets, feasibility, and leaf semantics

###### Definition A.3 (GuardSet) .

A *GuardSet* is a finite ordered index set $S\subseteq\{1,\dots,M\}$ representing
the polyhedron

$$ $C(S)\;=\;\bigcap_{\ell\in S}\{x:a_{\ell}^{\top}x\leq d_{\ell}\}.$ $$

We write $S\cup\{\ell\}$ (resp. $S\cup\{\bar{\ell}\}$) for adding an oriented face.

###### Definition A.4 (Feasibility cache) .

We maintain a cache $\mathsf{feas}:S\mapsto\{\textsf{unknown},\textsf{infeas},\textsf{feas}\}$,
queried/updated by a single LP feasibility test for $C(S)$. Certificates (a feasible point
or an infeasibility proof from the solver) may be stored alongside for reuse.

###### Definition A.5 (Leaves and active cover) .

At any time, the JIT refinement maintains a finite set of *leaf* GuardSets
$\mathcal{L}\subset 2^{\{1,\dots,M\}}$ such that:
(i) every visited $x$ belongs to at least one feasible $C(S)$ with $S\in\mathcal{L}$,
and (ii) whenever a leaf $S$ is split along a (possibly new) face $\ell$,
$S$ is *removed* from $\mathcal{L}$ and replaced by its children
$S^{+}=S\cup\{\ell\}$ and $S^{-}=S\cup\{\bar{\ell}\}$ that remain feasible.

###### Remark A.6 (Anytime envelopes are taken over leaves ) .

All lower/upper bounds $\operatorname{LB}(E,S)$ and $\operatorname{UB}(E,S)$ used to assemble the
anytime envelopes $(\underline{A},\overline{A})$ in §3 are aggregated only over
*current leaves* $S\in\mathcal{L}$ containing the query point $x$.
Removing a parent from $\mathcal{L}$ upon splitting ensures the monotonicity
$\underline{A}\uparrow$, $\overline{A}\downarrow$ proved in §3 (DYN–1/3).

###### Definition A.3 (GuardSet) .

###### Definition A.4 (Feasibility cache) .

###### Definition A.5 (Leaves and active cover) .

###### Remark A.6 (Anytime envelopes are taken over leaves ) .

### A.5 Lazy expression DAG (e–graph): syntax, semantics, and sharing

##### Syntax.

Scalar expressions are formed by the grammar

$$ $\texttt{Expr}\ ::=\ \texttt{Affine}(w,b)\ \mid\ \texttt{Sum}(\mathcal{E})\ \mid\ \texttt{Max}(\mathcal{E})\ \mid\ \texttt{Scale}(c,E)\ \mid\ \texttt{Bias}(b,E),$ $$

where $\mathcal{E}$ is a finite multiset of subexpressions, $c\in\mathbb{R}$, and
$\texttt{Affine}(w,b)(x)=w^{\top}x+b$. Vector outputs are tuples of scalar Exprs.

##### Pointwise semantics.

For $x\in\mathbb{R}^{n}$, the denotation ${\llbracket E\rrbracket}(x)$ is defined recursively by

$$ $\displaystyle{\llbracket\texttt{Affine}(w,b)\rrbracket}(x)=w^{\top}x+b,\quad{\llbracket\texttt{Bias}(b,E)\rrbracket}(x)={\llbracket E\rrbracket}(x)+b,$ $\displaystyle{\llbracket\texttt{Scale}(c,E)\rrbracket}(x)=c\cdot{\llbracket E\rrbracket}(x),\quad{\llbracket\texttt{Sum}(\{E_{i}\})\rrbracket}(x)=\sum_{i}{\llbracket E_{i}\rrbracket}(x),$ $\displaystyle{\llbracket\texttt{Max}(\{E_{i}\})\rrbracket}(x)=\max_{i}{\llbracket E_{i}\rrbracket}(x).$ $$

These agree with the function semiring $(\mathrm{CPWL}^{\pm\infty},\oplus,\otimes)$ via
$\oplus=\max$ and $\otimes=+$ (cf. §2).

##### Sharing and congruence.

Expressions are stored in an *e–graph* with hash–consing and congruence closure:

- 1.
Affine interning. Two affine atoms are identical iff their $(w,b)$
are componentwise equal (theory level) or equal within a fixed tolerance $\tau$
(implementation level; does not affect the closed–set semantics).
- 2.
AC canonicalization. Children of Sum/Max are stored in a
deterministic order (e.g., lexicographic by node id) so that $\texttt{Sum}(E_{1},E_{2})$ and
$\texttt{Sum}(E_{2},E_{1})$ share; likewise for Max.
- 3.
Common subexpression elimination. Any structurally equal subterm is stored once
and referenced by pointers; this enables whole–graph updates when a subterm’s bound is tightened.

##### Comparator nodes and winners.

Comparator faces introduced by Max (and gate sign tests) are not embedded as
Boolean nodes; instead they are materialized as linear faces registered in $\mathcal{H}$
(§[A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)) when a visited leaf $S\in\mathcal{L}$ requires disambiguation.
Winner selection is then expressed by restricting to the corresponding children
$S\cup\{\ell\}$ or $S\cup\{\bar{\ell}\}$.

### A.6 Ties, floating point tolerance, and determinism

All theoretical statements use closed guards and exact reals.
Implementations may adopt a small tolerance $\tau$ (e.g., $10^{-7}$) to decide numeric
equalities; when $|z(x)|\leq\tau$ at a hinge, both orientations are registered and explored
under JIT, preserving soundness of the envelopes in §3.

### A.7 Summary table of symbols

| Symbol | Type | Meaning |
| --- | --- | --- |
| $D,\ \mathcal{D}_{\rm in}$ | set | Input domain / global domain (§[A.1](https://arxiv.org/html/2510.17622v1#A1.Thmtheorem1)) |
| $B_{p}(x_{0},\epsilon)$ | set | $\ell_{p}$ ball (SOCP when $p{=}2$) |
| $\|\cdot\|_{p},\ p^{*}$ | number | Vector norm and its dual (§[A.2](https://arxiv.org/html/2510.17622v1#A1.Thmtheorem2)) |
| $\|J\|_{p\to r}$ | number | Operator norm of a linear map $J$ |
| $\mathcal{H}$ | library | Global guard library (§[A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)) |
| $h_{\ell}$ | halfspace | Guard $\{a_{\ell}^{\top}x\leq d_{\ell}\}$; reverse index $\bar{\ell}$ |
| $S$ | set of ids | GuardSet; $C(S)=\bigcap_{\ell\in S}h_{\ell}$ (§[A.3](https://arxiv.org/html/2510.17622v1#A1.Thmtheorem3)) |
| $\mathsf{feas}(S)$ | enum | Feasibility cache (§[A.4](https://arxiv.org/html/2510.17622v1#A1.Thmtheorem4)) |
| $\mathcal{L}$ | set | Current leaves (active cover; §[A.5](https://arxiv.org/html/2510.17622v1#A1.Thmtheorem5)) |
| Expr | DAG node | Lazy scalar expression (§[A.5](https://arxiv.org/html/2510.17622v1#A1.SS5)) |
| $\underline{A},\overline{A}$ | function | Anytime envelopes (aggregated over leaves) |

## Appendix B Proofs for AF-1..AF-5

This appendix supplies full proofs for the AF-series statements used in the main
text: CPWL closure (AF–1), pointwise homomorphism (AF–2),
continuity and sufficient convexity (AF–3), a.e. differentiability and Clarke
subgradients (AF–4), and closure under composition (AF–5).
We respect the closed-guard convention (both sides of hinges kept) fixed in
§[A](https://arxiv.org/html/2510.17622v1#A1).

### B.1 Preliminaries on CPWL functions and polyhedral complexes

###### Definition B.1 (CPWL) .

A function $f:\mathbb{R}^{n}\!\to\!\mathbb{R}$ is *continuous piecewise linear* (CPWL) if there exists
a finite polyhedral complex $\mathcal{C}=\{R_{\rho}\}$ that covers $\mathbb{R}^{n}$ such that for each
cell $R_{\rho}$, $f(x)=w_{\rho}^{\top}x+b_{\rho}$ holds on $R_{\rho}$ and adjacent cells agree on
their shared faces (continuity).

###### Lemma B.2 (Finite overlays) .

Let $\mathcal{C}_{1},\ldots,\mathcal{C}_{k}$ be finite polyhedral complexes in $\mathbb{R}^{n}$.
Then the common refinement
$\mathcal{C}=\operatorname{refine}(\mathcal{C}_{1},\ldots,\mathcal{C}_{k})$ obtained by
intersecting all cells is a finite polyhedral complex.

###### Proof.

Each $\mathcal{C}_{i}$ is finite and closed under taking faces.
Intersections of finitely many polyhedra are polyhedra, and the set of all nonempty
intersections of finitely many cells is finite. Face-compatibility follows from
face-compatibility of the inputs and distributivity of intersections over faces.
∎

###### Lemma B.3 (Basic CPWL closure) .

If $f,g$ are CPWL on $\mathbb{R}^{n}$, then $f+g$ and $\max\{f,g\}$ are CPWL.
If $A\in\mathbb{R}^{m\times n},b\in\mathbb{R}^{m}$, then $x\mapsto f(Ax{+}b)$ is CPWL on $\mathbb{R}^{m}$.

###### Proof.

Write $f=w_{\rho}^{\top}x+b_{\rho}$ on cells $R_{\rho}$ of $\mathcal{C}_{f}$ and
$g=u_{\sigma}^{\top}x+c_{\sigma}$ on cells $S_{\sigma}$ of $\mathcal{C}_{g}$.
On the overlay $\mathcal{C}=\operatorname{refine}(\mathcal{C}_{f},\mathcal{C}_{g})$,
both are affine, hence $f{+}g$ is affine cell-wise.
For $\max\{f,g\}$, further refine by the family of linear comparators
$\{(w_{\rho}{-}u_{\sigma})^{\top}x+(b_{\rho}{-}c_{\sigma})\geq 0\}$; on each side of each comparator
the winner is fixed and the result is affine. Finiteness is preserved by
Lemma [B.2](https://arxiv.org/html/2510.17622v1#A2.Thmtheorem2). For composition with $Ax{+}b$, pull back each cell
$R_{\rho}$ by $(Ax{+}b)$; preimages of polyhedra by an affine map are polyhedra, and
continuity is preserved, so $f\!\circ\!(Ax{+}b)$ is CPWL on a finite complex.
∎

###### Definition B.1 (CPWL) .

###### Lemma B.2 (Finite overlays) .

###### Proof.

###### Lemma B.3 (Basic CPWL closure) .

###### Proof.

### B.2 AF-1: Well-definedness (CPWL closure of the component set)

###### Theorem B.4 (AF–1) .

Under the component and DAG assumptions (affine/conv/mean-pool/inference BN/residual;
ReLU/LReLU/PReLU/Abs/Max), every pre-activation is CPWL and every activation remains in
$K_{f}=(\mathrm{CPWL}^{\pm\infty},\oplus=\max,\otimes=+)$.

###### Proof.

*Affine, residual, mean-pool, inference-time BN.*
Each is an affine map in the input; convolution with fixed stride/padding is a linear map,
hence affine. (Inference BN $y=\gamma\odot\frac{x-\mu}{\sigma}+\beta$ is affine with fixed
$\mu,\sigma,\gamma,\beta$.) By Lemma [B.3](https://arxiv.org/html/2510.17622v1#A2.Thmtheorem3), affine maps preserve CPWL.

*Pointwise gates.*
Let $z$ be a CPWL pre-activation.

$$ $\mathrm{ReLU}(z)=\max\{0,z\},\quad\mathrm{LReLU}_{\alpha}(z)=\max\{z,\alpha z\}\ (\alpha\!\in[0,1]),\quad\mathrm{PReLU}_{\alpha}(z)=\max\{z,\alpha z\}\ (\alpha\!\geq 0),$ $$

$$ $\mathrm{Abs}(z)=\max\{z,-z\},\qquad\mathrm{Max}(z_{1},\ldots,z_{k})=\max_{i}z_{i}.$ $$

Each right-hand side is a finite max of CPWL functions (affine multiples of $z$ or a finite
family $\{z_{i}\}$), hence CPWL by Lemma [B.3](https://arxiv.org/html/2510.17622v1#A2.Thmtheorem3).
The closed-guard convention ensures ties are covered on both sides and continuity is kept.

*DAG composition.*
Layerwise application of the above operations along a DAG composes CPWL maps with affine
maps and finite maxima; closure follows from Lemma [B.3](https://arxiv.org/html/2510.17622v1#A2.Thmtheorem3).
∎

###### Theorem B.4 (AF–1) .

###### Proof.

### B.3 AF-2: Pointwise homomorphism

###### Theorem B.5 (AF–2) .

For any input $x_{0}$, evaluation $h_{x_{0}}:K_{f}\to(\mathbb{R},\max,+)$ given by $h_{x_{0}}(f)=f(x_{0})$
is a semiring homomorphism. Therefore the SWT expression obtained from a network evaluates
to the same numeric forward value at $x_{0}$.

###### Proof.

By definition,
$h_{x_{0}}(f\oplus g)=(f\oplus g)(x_{0})=\max\{f(x_{0}),g(x_{0})\}=\max\{h_{x_{0}}(f),h_{x_{0}}(g)\}$,
and $h_{x_{0}}(f\otimes g)=(f\otimes g)(x_{0})=f(x_{0}){+}g(x_{0})=h_{x_{0}}(f){+}h_{x_{0}}(g)$.
Also $h_{x_{0}}(\mathbf{0})=-\infty$ and $h_{x_{0}}(\mathbf{1})=0$.
Hence $h_{x_{0}}$ is a semiring homomorphism.

A network compiled to an SWT is a finite DAG of $K_{f}$-weighted nodes/edges combined by
$\oplus$ (for selections/max) and $\otimes$ (for branch sums).
Evaluating the SWT via $h_{x_{0}}$ pushes evaluation through the DAG and returns exactly the
numeric forward pass (sum along the active branches; max across competing branches).
Induction on the topological order of the DAG completes the proof.
∎

###### Theorem B.5 (AF–2) .

###### Proof.

### B.4 AF-3: Continuity and sufficient convexity

###### Theorem B.6 (AF–3: continuity) .

Every network output coordinate is CPWL and hence continuous on $\mathbb{R}^{n}$.

###### Proof.

AF–1 shows all coordinates are CPWL. CPWL functions are continuous by definition of
polyhedral complexes with face-compatible affine pieces.
∎

###### Theorem B.7 (AF–3: sufficient convexity) .

Suppose that at every layer, each activation $\phi$ is convex and nondecreasing
(e.g., ReLU, LReLU with $\alpha\in[0,1]$, PReLU with $\alpha\geq 0$, pointwise Max),
and the *mixing coefficients* feeding each activation are entrywise nonnegative.
Then each output coordinate is convex. If $\mathrm{Abs}$ is used, convexity is preserved
only when $\mathrm{Abs}$ is applied directly to an affine pre-activation.

###### Proof.

Let $x\mapsto Ax{+}b$ be an affine pre-activation. Convexity is preserved under affine
precomposition and nonnegative linear combinations: if $u_{j}$ are convex and $\lambda_{j}\geq 0$,
then $\sum_{j}\lambda_{j}u_{j}$ is convex. If $\phi$ is convex and nondecreasing, then
$\phi\!\circ\!u$ is convex whenever $u$ is convex. These are standard closure rules.
Start from the input (convex), propagate through affine layers (convexity preserved),
through nonnegative summations (residual/additive merges), and through convex
nondecreasing activations (ReLU/LReLU/PReLU/Max), convexity is preserved at each step.
For $\mathrm{Abs}(t)=\max\{t,-t\}$: it is convex in $t$, but not monotone; in general
$\mathrm{Abs}\!\circ\!u$ need not be convex if $u$ is nonconvex CPWL. When $u$ is affine,
$\mathrm{Abs}\!\circ\!u$ is convex; this is the stated boundary case.
∎

###### Theorem B.6 (AF–3: continuity) .

###### Proof.

###### Theorem B.7 (AF–3: sufficient convexity) .

###### Proof.

### B.5 AF-4: a.e. differentiability and Clarke subdifferentials

###### Theorem B.8 (AF–4) .

Let $f$ be CPWL on $\mathbb{R}^{n}$. Then $f$ is differentiable Lebesgue-a.e., and on each cell
$R_{\rho}$ of a defining complex $\mathcal{C}$ we have $f(x)=w_{\rho}^{\top}x+b_{\rho}$ with
$\nabla f(x)=w_{\rho}$ for all $x\in\operatorname{ri}(R_{\rho})$. At a boundary point
$x\in\partial R_{\rho}$, the Clarke subdifferential is the convex hull of the neighboring
gradients:

$$ $\partial^{C}f(x)=\operatorname{conv}\{\,w_{\rho}:\ x\in R_{\rho}\,\}.$ $$

###### Proof.

The union of the relative interiors of the finitely many cells covers $\mathbb{R}^{n}$ up to a set
contained in a finite union of affine hyperplanes (cell boundaries), which has Lebesgue
measure zero. On each relative interior $f$ is affine, hence differentiable with constant
gradient $w_{\rho}$. The Clarke subdifferential of a locally Lipschitz function equals the
closed convex hull of the set of limiting gradients; for CPWL the only limits arise from
adjacent cells, yielding the stated formula.
∎

###### Theorem B.8 (AF–4) .

###### Proof.

### B.6 AF-5: Closure under finite compositions

###### Theorem B.9 (AF–5) .

Any finite composition of layers built from affine maps, residual (additive) merges,
and pointwise gates $\{\mathrm{ReLU},\mathrm{LReLU},\mathrm{PReLU},\mathrm{Abs},\mathrm{Max}\}$
yields a CPWL map.

###### Proof.

By AF–1 each individual layer maps CPWL inputs to CPWL outputs.
By Lemma [B.3](https://arxiv.org/html/2510.17622v1#A2.Thmtheorem3), affine pre/post-composition, finite sums, and finite maxima
preserve CPWL. Induction on the number of layers (topological order of the DAG) proves that
the overall composition is CPWL.
∎

###### Theorem B.9 (AF–5) .

###### Proof.

##### Remarks on convolution and pooling.

A discrete convolution with fixed kernel, stride, and padding is a linear operator
on the vectorized input; mean-pooling is also linear. Therefore they are covered by
the affine-case arguments above. Max-pooling is a finite pointwise maximum and falls
under Lemma [B.3](https://arxiv.org/html/2510.17622v1#A2.Thmtheorem3). Inference-time batch normalization is affine.

##### Closed guards and ties.

All thresholds/comparators are treated with closed inequalities ($\geq,\leq$) on both
sides, so $z{=}0$ lies in both guarded branches. This preserves continuity and ensures
that $\oplus=\max$ resolves ties without leaving gaps, consistent with the semantics
used in the experiments and implementation.

## Appendix C SWT Semantics and Equivalent Compilation (SWT-1/2/3/4/5)

This appendix formalizes the compilation of a CPWL network into a guarded
*Symbolic Weighted Transducer* (SWT), proves pointwise equivalence (SWT–1),
states size and acyclicity bounds with explicit counting conventions (SWT–2),
gives common refinement / difference-region constructions and correctness
(SWT–3/4), and provides an NP-hardness reduction for minimal-guard
realizations (SWT–5).

### C.1 Formal compilation rules

##### Object model and counting conventions.

We compile the network DAG to an acyclic SWT
$A=(Q,q_{\mathrm{in}},F,E,\mathsf{G},\mathsf{W},K_{f})$ with:

- •
States ($Q$). One state per *structural site*:
post-layer sites for affine modules (Dense/BN/MeanPool/Residual-add),
post-gate sites (ReLU/LReLU/PReLU/Abs/Max), and per-template sites for
convolution/GNN (defined below). We never use “region as state”.
- •
Edges ($E$). A dataflow edge $(u\!\to\!v)$ becomes one SWT edge unless
$v$ is a gate, in which case guarded multi-edges are created (two for
two-way gates; $k$ for Max-of-$k$).
- •
Guards ($\mathsf{G}$). Each edge stores an *index set* (GuardSet)
into the global library $\mathcal{H}$; intersections are formed on-the-fly,
not stored explicitly (cf. App. [A](https://arxiv.org/html/2510.17622v1#A1)).
- •
Weights ($\mathsf{W}$). CPWL weights in the function semiring
$K_{f}=(\mathrm{CPWL}^{\pm\infty},\oplus=\max,\otimes=+)$; along a path, weights
compose by $\otimes(=+)$; across alternative paths they combine by
$\oplus(=\max)$.

##### Affine / residual / mean-pool / inference-time BN.

Let a fragment $(C,w,b)$ denote guard $C$ and affine map $x\mapsto w^{\top}x+b$.
For $y=Wx+b_{0}$ we emit $(C,\tilde{w},\tilde{b})$ with
$\tilde{w}=Ww,\ \tilde{b}=Wb+b_{0}$.
Residual $\textsf{Sum}(x^{(1)},x^{(2)})$ contributes one post-sum state and
two incoming edges; weights add by $\otimes$ on the common guard.
Inference-time BN is merged into affine.

##### Two-way gates (ReLU/LReLU/PReLU/Abs).

Given pre-activation $z(x)=w^{\top}x+b$ on $C$, create two guarded edges
to the post-gate site (closed guards on both sides):

$$ $\displaystyle\textsf{pos:}\quad C^{+}=C\cap\{z\geq 0\}\ \leadsto\ (w,b),$ $\displaystyle\textsf{neg:}\quad C^{-}=C\cap\{z\leq 0\}\ \leadsto\$ $$

Insert the (normalized) threshold face $\{z\geq 0\}$ into $\mathcal{H}$ (both orientations
are registered; see App. [A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)).

##### Pointwise Max / MaxPool.

For candidates $\{(C_{i},w_{i},b_{i})\}_{i=1}^{k}$ with $C_{\cap}=\bigcap_{i}C_{i}$,
insert pairwise comparators $\{(w_{i}{-}w_{j})^{\top}x+(b_{i}{-}b_{j})\geq 0\}$ to $\mathcal{H}$
and create $k$ edges to the post-Max site, guarded by the winner regions

$$ $C_{i}^{\star}=C_{\cap}\ \cap\ \bigcap_{j\neq i}\{(w_{i}{-}w_{j})^{\top}x+(b_{i}{-}b_{j})\geq 0\}.$ $$

##### Convolution (template aliasing; sliding-window guards).

For a conv layer with kernel $K\in\mathbb{R}^{C_{\rm out}\times C_{\rm in}\times h\times w}$,
stride $(s_{x},s_{y})$, padding $(p_{x},p_{y})$, output spatial size $(H_{\rm out},W_{\rm out})$,
we instantiate one site per output channel-location
$r=(c,i,j)\in\{1..C_{\rm out}\}\times\{1..H_{\rm out}\}\times\{1..W_{\rm out}\}$,
with *template aliasing* of weights: each site references the same $K$ by index.
The receptive field constraint is captured by a rectangular sliding-window guard
$C_{r}=\{x:\ M_{r}x=\mathrm{vec}(x[\mathrm{patch}(i,j)])\}$ which in H-form is the
intersection of the input domain with the valid-range halfspaces implied by stride/padding
(i.e., pixels outside the padded canvas are fixed to the padding value and realized as
affine shifts). The linear map of conv at $r$ is an affine atom $(w_{r},b_{r})$ obtained by
composing im2col with $K_{c,:,:,:}$; see App. [I](https://arxiv.org/html/2510.17622v1#A9) for a matrix-free variant.

##### GNN on a fixed graph.

For an aggregation layer on $G=(V,E)$ with normalized adjacency $\hat{A}$ and output
channels $C_{\rm out}$, we instantiate $|V|\cdot C_{\rm out}$ sites, each referencing
shared parameters (template aliasing). Sum/mean aggregations compile to sparse affine
maps $(\hat{A}\otimes I)$; Max aggregation uses comparator guards across neighbor terms.
Per-node MLPs follow the affine+gate rules above.

###### Remark C.1 (No region as state; shared guard library) .

Edges store only guard indices.
Winner regions and guard intersections are materialized on demand (JIT) or symbolically
specified (static), but states are never duplicated per region. This is essential for the
size bounds in §[C.3](https://arxiv.org/html/2510.17622v1#A3.SS3).

###### Remark C.1 (No region as state; shared guard library) .

### C.2 Proof of SWT-1 (pointwise equivalence)

###### Theorem C.2 (SWT–1) .

For any input $x$, the SWT $A_{F}$ compiled by §[C.1](https://arxiv.org/html/2510.17622v1#A3.SS1) satisfies
$A_{F}(x)=F(x)$.

###### Proof sketch with a worked miniature.

Homomorphism. By AF–2, evaluation $h_{x}:K_{f}\!\to\!(\mathbb{R},\max,+)$ preserves
$\oplus/\otimes$. Hence it suffices to check that each module compiles to an
expression over $K_{f}$ whose $h_{x}$-evaluation equals the numeric forward of that
module at $x$.

Affine and residual. Along a path, $\otimes$ accumulates affine weights by
addition, matching numeric sums. A residual merge with fan-in two contributes two
incoming edges whose $h_{x}$-values add (same $C$), equal to the module’s numeric sum.

Two-way gates and Max. The closed guards ensure that at any $x$ exactly the
feasible *winner* edge(s) remain; the outgoing value is the $\oplus$ over those
edges, which equals the ordinary max (or gate rule) at $x$.

Miniature for parallel addition.
Consider $y=f_{1}(x)+f_{2}(x)$ realized by two branches merging into a post-sum state $q$.
Compilation creates edges $e_{1}:q_{f_{1}}\!\to q$ and $e_{2}:q_{f_{2}}\!\to q$ with weights
$\mathsf{W}(e_{i})=f_{i}$. There is a *single* path from $q_{\rm in}$ to $q$ passing
through the structure of $f_{1}$ and another passing through $f_{2}$ composed in series
via an intermediate “sum” node where we use $\otimes$ to combine the two branch
contributions on the *same* path (not via $\oplus$ across paths).
Thus $\mathsf{val}(\pi,x)=f_{1}(x){+}f_{2}(x)$ by $\otimes$, while $\oplus$ across
*alternative* guarded paths is reserved solely for max-type choices.
This construction (explicit in the compiler IR) eliminates any ambiguity between
sum and max.

Convolution / GNN. Each template instance is an affine map (linear with bias);
template aliasing shares parameters but does not affect per-instance semantics. Therefore,
$h_{x}$ on the compiled instance equals the numeric conv/GNN output at that site.

Induction on the DAG. Process nodes in topological order; at each step, the
compiled fragment preserves the module’s semantics at $x$. Hence $A_{F}(x)=F(x)$ globally.
∎

###### Remark C.3 (Empirical alignment) .

On FFN/CNN/GNN models, the compiled SWT/JIT forward agrees with PyTorch forward to
machine precision (mean absolute errors around $10^{-6}\!\sim\!10^{-7}$), matching the
predicted pointwise equivalence. See the per-sample error plots and tables in the
experiment report (Task 1/2/3). *This is not part of the proof, but confirms the
implementation adheres to the semantics.*

###### Theorem C.2 (SWT–1) .

###### Proof sketch with a worked miniature.

###### Remark C.3 (Empirical alignment) .

### C.3 SWT-2: acyclicity and size bounds with explicit constants

##### Counting parameters.

Let

$$ $\displaystyle N_{\textsf{aff}}=\text{number of affine sites (Dense/BN/MeanPool/Residual-post)},$ $\displaystyle N_{\textsf{gate2}}=\text{number of scalar two-way gates (ReLU/LReLU/PReLU/Abs)},$ $\displaystyle\mathcal{V}_{\max}=\{v:\ \text{pointwise Max site of arity }k_{v}\},\quad K_{\max}=\sum_{v\in\mathcal{V}_{\max}}k_{v},$ $\displaystyle\Gamma_{\max}=\sum_{v\in\mathcal{V}_{\max}}\binom{k_{v}}{2},\qquad\Gamma^{\pm}_{\max}=2\,\Gamma_{\max}\ \ (\text{both orientations}),$ $\displaystyle T_{\textsf{conv}}=\sum_{\ell\in\text{conv layers}}C^{(\ell)}_{\rm out}H^{(\ell)}_{\rm out}W^{(\ell)}_{\rm out},$ $\displaystyle T_{\textsf{gnn}}=\sum_{\ell\in\text{MP layers}}|V|\,C^{(\ell)}_{\rm out}.$ $$

Assume each affine/conv/GNN site has in-degree 1 except residual-post sites whose
in-degree is their fan-in (typically 2).

###### Proposition C.4 (Acyclicity) .

If the computation graph is a DAG, the compiled SWT is acyclic.

###### Proof.

Compilation preserves edge directions and introduces no back-edges; gate splits and
winner guards do not add cycles, only parallel guarded edges. States correspond to
post-module/template sites in the original topological order.
∎

###### Theorem C.5 (Size bounds with explicit constants) .

Under the counting above, the following hold for the *static* SWT:

$$ $\boxed{\ |Q|\ \leq\ 1\ +\ N_{\textsf{aff}}\ +\ T_{\textsf{conv}}\ +\ T_{\textsf{gnn}}\ +\ |\mathcal{V}_{\max}|\ +\ N_{\textsf{gate2}}\ }$ $$

$$ $\boxed{\ |E|\ \leq\ N_{\textsf{aff}}\ +\ T_{\textsf{conv}}\ +\ T_{\textsf{gnn}}\ +\ (\textstyle\sum\text{residual fan-ins})\ +\ 2N_{\textsf{gate2}}\ +\ K_{\max}\ }$ $$

$$ $\boxed{\ |\mathcal{H}|_{\rm planes}\ \leq\ N_{\textsf{gate2}}\ +\ \Gamma_{\max}\ ,\qquad|\mathcal{H}|_{\rm oriented}\ \leq\ 2N_{\textsf{gate2}}\ +\ \Gamma^{\pm}_{\max}\ }$ $$

where $|\mathcal{H}|_{\rm planes}$ counts distinct *hyperplanes* and
$|\mathcal{H}|_{\rm oriented}$ counts oriented halfspaces (our library stores both
orientations; cf. App. [A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)).

###### Proof.

Each structural site contributes one state, yielding the formula for $|Q|$ (plus
the initial state). Edges: every non-gate site with in-degree one contributes one
edge; each residual-post contributes exactly its fan-in many edges; each two-way
gate creates two guarded edges; each Max-of-$k$ site creates $k$ guarded edges.
Guards: every scalar two-way gate contributes one distinct plane (two orientations);
every Max-of-$k$ introduces $\binom{k}{2}$ distinct planes, equivalently
$2\binom{k}{2}$ oriented halfspaces across all winners. Summing proves the bounds.
∎

###### Remark C.6 (Comparator dominance) .

The edge/guard complexity is dominated by comparator faces: even when $|Q|$ is
linear in sites/templates, $|\mathcal{H}|$ scales with $N_{\textsf{gate2}}$
and $\Gamma_{\max}$. In JIT (§3), we avoid inserting all comparators upfront,
introducing them *on demand* per visited leaf, which empirically tracks the
accessed subdomains (cf. the modest split counts in the experiments).

###### Proposition C.4 (Acyclicity) .

###### Proof.

###### Theorem C.5 (Size bounds with explicit constants) .

###### Proof.

###### Remark C.6 (Comparator dominance) .

### C.4 SWT-3/4: common refinement and difference-region automata

##### Problem statements.

Given two acyclic SWTs $A_{1},A_{2}$ and a convex domain $D$, decide whether
$A_{1}\equiv A_{2}$ on $D$ (SWT–3), or construct the region
$\{x\in D:\ |A_{1}(x)-A_{2}(x)|>\varepsilon\}$ (SWT–4).

##### Algorithm (common refinement for equivalence).

- 1.
Unify guard libraries. Let $\mathcal{H}=\mathcal{H}_{1}\cup\mathcal{H}_{2}$
with canonicalization; represent $D$ as $S_{0}$ (App. [A](https://arxiv.org/html/2510.17622v1#A1)).
- 2.
Refine on demand. Maintain a queue of GuardSets $\mathcal{L}$ (leaves).
For a leaf $S$, evaluate both SWTs symbolically; if either side still contains
undecided gates/Max, insert the *relevant* faces for that side only and split $S$.
- 3.
Cellwise affine check. Once both sides degenerate to *single affine*
on $C(S)$, read $(w_{1,S},b_{1,S})$ and $(w_{2,S},b_{2,S})$.
If they are equal, mark $S$ as safe; otherwise solve the LP
$\min_{x\in C(S)\cap D}\ \|(w_{1,S}{-}w_{2,S})^{\top}x+(b_{1,S}{-}b_{2,S})\|_{\infty}$
to obtain a witness. Iterate until all leaves are safe (then $A_{1}\equiv A_{2}$), or a witness is found.

###### Theorem C.7 (Correctness and decidability (SWT–3)) .

The procedure above is sound. If only finitely many gate/comparator faces can be
inserted (finite network) and the strategy is fair (every feasible undecided leaf
is eventually processed), it terminates with a certificate of equivalence or a
counterexample.

###### Proof.

Soundness: on each leaf $S$ where both sides are single affine, equality reduces
to an affine-coefficient check; inequality yields an LP-feasible witness.
Termination under finiteness+fairness follows because the set of faces is finite and
each split strictly reduces uncertainty on $S$ until all leaves are affine on both sides.
∎

###### Theorem C.7 (Correctness and decidability (SWT–3)) .

###### Proof.

##### Difference-region automata (SWT–4).

Let $g=A_{1}-A_{2}$ (componentwise for vectors and then $\ell_{\infty}$).
On leaves where $g$ is affine, add two threshold guards $\{g\geq\varepsilon\}$
and $\{-g\geq\varepsilon\}$ to generate the polyhedral complex

$$ $\mathcal{R}_{\varepsilon}=\bigcup_{S\in\mathcal{L}}\Bigl[\bigl(C(S)\cap\{g\geq\varepsilon\}\bigr)\ \cup\ \bigl(C(S)\cap\{-g\geq\varepsilon\}\bigr)\Bigr].$ $$

The resulting automaton recognizes $\{x:\ |A_{1}(x)-A_{2}(x)|>\varepsilon\}$.

###### Proposition C.8 (Correctness (SWT–4)) .

$\mathcal{R}_{\varepsilon}$ equals $\{x\in D:\ |A_{1}(x)-A_{2}(x)|>\varepsilon\}$ and
each constituent region provides an LP witness by evaluating $g$’s affine form.

###### Proposition C.8 (Correctness (SWT–4)) .

### C.5 SWT-5: NP-hardness of minimal-face realization

##### Cost model (faces, not guards).

Let $\mathcal{H}=\{h_{\ell}(x):a_{\ell}^{\top}x\leq d_{\ell}\}_{\ell=1}^{M}$ be the global guard library
(canonicalized with *oriented* halfspaces; see App. [A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)).
An acyclic SWT $A$ uses a finite family of guarded edges, each guard being an index set
$S_{e}\subseteq\{1,\dots,M\}$ denoting $C(S_{e})=\bigcap_{\ell\in S_{e}}\{a_{\ell}^{\top}x\leq d_{\ell}\}$
(App. [A.4](https://arxiv.org/html/2510.17622v1#A1.SS4)). Define the *used-face set* and cost of $A$ by

$$ $\mathrm{faces}(A):=\bigcup_{e}S_{e}\subseteq\{1,\dots,M\},\qquad\mathrm{cost}(A):=|\mathrm{faces}(A)|,$ $$

i.e., each oriented halfspace from the shared library is counted once no matter how many edges reuse it
(consistent with the “unique-guard / no region-as-state” discipline).

##### Decision problem (MF–SWT).

Fix a finite guard library $\mathcal{H}$ and a finite affine basis
$\mathcal{B}=\{(w_{j},b_{j})\}_{j=1}^{B}$. Given a target $F$ that is realizable by some
acyclic SWT using only guards from $\mathcal{H}$ and affine atoms from $\mathcal{B}$,
decide whether there exists such an SWT $A$ with $\mathrm{cost}(A)\leq k$.

###### Theorem C.9 (SWT–5: NP-hardness) .

The decision problem MF–SWT is NP-hard via a polynomial reduction from Set-Cover.

###### Reduction.

Given a Set-Cover instance $(U,\mathcal{S},k)$ with
$U=\{1,\dots,m\}$ and $\mathcal{S}=\{S_{1},\dots,S_{r}\}$, construct
$(F,\mathcal{H},\mathcal{B})$ as follows.

*Domain and library.*
Work in $X\times Y$ with $X\subset\mathbb{R}^{2}$ and $Y=[0,1]^{r}$, so that the overall domain
$D:=X\times Y$ is convex polyhedral under the closed-guard convention
(App. [A.1](https://arxiv.org/html/2510.17622v1#A1.SS1), [A.2](https://arxiv.org/html/2510.17622v1#A1.SS2)).
Pick $m$ pairwise-disjoint tiny axis-aligned boxes $B_{i}\subset X$ (grid-separated).
Insert into $\mathcal{H}$ exactly the four oriented $X$-faces delimiting each $B_{i}$
(with canonical orientations; App. [A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)).
For each $j\in\{1,\dots,r\}$, also insert the single $Y$-face $\{y_{j}\geq\tfrac{1}{2}\}$
(its opposite orientation is stored as a distinct index by our convention; App. [A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)).

*Basis and target.*
Let $\mathcal{B}=\{(0,0),(0,1)\}$ (constants 0 and $1$). For each $i\in[m]$ define
$S_{i}:=\{\,j\in[r]:\,i\in S_{j}\,\}$, i.e., the set indices that contain element $i$.
Define the target $F$ *by an SWT over the above library* as the $\oplus=\max$ of edges of weight $1$
guarded by the “cylinders”

$$ $C_{i,j}:=B_{i}\times\{\,y:\ y_{j}\geq\tfrac{1}{2}\,\}\qquad(i\in[m],\ j\in S_{i}),$ $$

together with a default edge of weight 0 on $D$. Under the SWT truth semantics
(Sec. [C.1](https://arxiv.org/html/2510.17622v1#A3.SS1)–[C.2](https://arxiv.org/html/2510.17622v1#A3.SS2)), this realizes the function that equals $1$ on
$\bigcup_{i}\bigcup_{j\in S_{i}}C_{i,j}$ and 0 elsewhere.

*Forward direction ($\Rightarrow$).*
If there exists a set cover $\mathcal{C}\subseteq\mathcal{S}$ with $|\mathcal{C}|\leq k$, build an SWT that,
for each $j\in\mathcal{C}$ and each $i\in S_{j}$, includes one edge guarded by
$B_{i}\cap\{y_{j}\geq\tfrac{1}{2}\}$ and weight $1$ (the default 0-edge is kept).
By guard sharing, the distinct oriented $X$-faces used are exactly the $4m$ faces of the $B_{i}$’s, and
the distinct $Y$-faces used are precisely $\{\,|y_{j}\geq\tfrac{1}{2}|:\ j\in\mathcal{C}\,\}$.
Hence $\mathrm{cost}(A)=4m+|\mathcal{C}|\leq 4m+k$.

*Reverse direction ($\Leftarrow$).*
Suppose an acyclic SWT $A$ realizes $F$ with $\mathrm{cost}(A)\leq 4m+k$.
Because the only $X$-faces available in $\mathcal{H}$ are the four per $B_{i}$, any edge
that outputs $1$ and omits *some* face of a given $B_{i}$ would leak outside $B_{i}$ in $X$,
contradicting $F=0$ there. Thus all $4m$ oriented $X$-faces must lie in $\mathrm{faces}(A)$.
Let $J:=\{\,j:\ \{|y_{j}\geq\tfrac{1}{2}|\}\subseteq\mathrm{faces}(A)\,\}$; then $|J|\leq k$.
If $J$ were not a set cover, there would exist $i^{\star}\in U$ such that $S_{i^{\star}}\cap J=\varnothing$.
But then no guard of any $1$-weighted edge can contain a $Y$-face that activates on
$B_{i^{\star}}\times\{y\}$ for *any* $y$ with $y_{j}\geq\tfrac{1}{2}$ and $j\in S_{i^{\star}}$,
contradicting that $F=1$ on
$B_{i^{\star}}\times\{y:\ \exists j\in S_{i^{\star}},\ y_{j}\geq\tfrac{1}{2}\}$.
Therefore $J$ covers $U$, and $|J|\leq k$ yields a set cover of size at most $k$.

The reduction is polynomial in $(m,r)$ and uses only SWTs over the shared guard library with
closed guards and the $\oplus/\otimes$ semantics as specified in
Sec. [C.1](https://arxiv.org/html/2510.17622v1#A3.SS1)–[C.2](https://arxiv.org/html/2510.17622v1#A3.SS2) and App. [A.3](https://arxiv.org/html/2510.17622v1#A1.SS3)–[A.4](https://arxiv.org/html/2510.17622v1#A1.SS4).
∎

###### Remark C.10 (Convexity note) .

An H-representation encodes convex sets (intersections of halfspaces) and cannot represent an
arbitrary finite disjoint union. The construction above therefore counts *oriented halfspaces*
from the shared library and employs auxiliary coordinates $Y$ so that covering all required
cylinders enforces the use of membership faces $\{y_{j}\geq\tfrac{1}{2}\}$; the face budget then coincides
with the set-cover size up to the fixed constant $4m$.

###### Theorem C.9 (SWT–5: NP-hardness) .

###### Reduction.

###### Remark C.10 (Convexity note) .

##### Existence of a minimum.

Whenever $F$ is realizable by $(\mathcal{H},\mathcal{B})$, the set of attainable costs
$\{\mathrm{cost}(A):A\ \text{realizes }F\}$ is a nonempty subset of $\mathbb{N}$ and thus has a minimum
by well-ordering; denote it by $\mathrm{MC}_{\mathrm{faces}}(F;\mathcal{H},\mathcal{B})$.

## Appendix D JIT–SWT Semantics and Guarantees (DYN-1..DYN-7)

This appendix supplies complete proofs and algorithmic details for the JIT–SWT
semantics: (D.1) soundness and monotonicity of lower/upper bounds (LB/UB);
(D.2) formal refiners ENSURE_SIGN, ENSURE_WINNER,
ENSURE_COMMON_REFINE and their termination conditions;
(D.3) proofs of DYN–1..7 (incl. fairness and finite-refinement decidability,
plus certificate formats); and (D.4) budgeted complexity bounds.

Throughout we follow App. [A](https://arxiv.org/html/2510.17622v1#A1): guards are *closed*;
the global library $\mathcal{H}$ stores oriented halfspaces once (canonicalized);
a *GuardSet* $S$ denotes $C(S)=\bigcap_{\ell\in S}\{a_{\ell}^{\top}x\leq d_{\ell}\}$;
the current set of leaves is $\mathcal{L}$; and anytime envelopes are aggregated
*over leaves* containing the query point $x$.

### D.1 Soundness and Monotonicity of LB/UB (order-preserving constructors)

##### Local LB/UB oracle.

For a scalar lazy expression $E$ and a leaf $S\in\mathcal{L}$, the oracle yields
intervals $[\operatorname{LB}(E,S),\operatorname{UB}(E,S)]$ such that
$\operatorname{LB}(E,S)\leq\inf_{x\in C(S)}E(x)\leq\sup_{x\in C(S)}E(x)\leq\operatorname{UB}(E,S).$
The structural rules are:

$$ $\displaystyle\operatorname{LB}(\mathsf{Affine}(w,b),S)=\min_{x\in C(S)}w^{\top}x+b,\quad\operatorname{UB}(\mathsf{Affine}(w,b),S)=\max_{x\in C(S)}w^{\top}x+b;$ $\displaystyle\operatorname{LB}(\mathsf{Sum}\{E_{i}\},S)=\sum_{i}\operatorname{LB}(E_{i},S),\quad\operatorname{UB}(\mathsf{Sum}\{E_{i}\},S)=\sum_{i}\operatorname{UB}(E_{i},S);$ $\displaystyle\operatorname{LB}(\mathsf{Scale}(c,E),S)=,\quad\operatorname{UB}(\mathsf{Scale}(c,E),S)=;$ $\displaystyle\operatorname{LB}(\mathsf{Bias}(b,E),S)=\operatorname{LB}(E,S)+b,\quad\operatorname{UB}(\mathsf{Bias}(b,E),S)=\operatorname{UB}(E,S)+b;$ $\displaystyle\operatorname{LB}(\mathsf{Max}\{E_{i}\},S)=\max_{i}\operatorname{LB}(E_{i},S),\quad\operatorname{UB}(\mathsf{Max}\{E_{i}\},S)=\max_{i}\operatorname{UB}(E_{i},S).$ $$

(When desired, affine subcalls are solved by LP/SOCP to obtain *exact* local
bounds; otherwise any sound relaxation is permitted.)

###### Lemma D.1 (Soundness of structural LB/UB) .

The rules above are sound: for every constructor and every leaf $S\in\mathcal{L}$,
they produce intervals containing the true range of $E$ on $C(S)$.

###### Proof.

Induction on the syntax tree of $E$.
Affines: exact by linear optimization on a polyhedron. Sum/scale/bias: use
$\inf(f{+}g)\geq\inf f{+}\inf g$, $\sup(f{+}g)\leq\sup f{+}\sup g$ and the sign-aware
identities $\inf(cf)=c\,\inf f$ for $c\geq 0$, $\inf(cf)=c\,\sup f$ for $c<0$
(and similarly for $\sup$). Max: $\sup\max_{i}f_{i}=\max_{i}\sup f_{i}$ and
$\inf\max_{i}f_{i}\geq\max_{i}\inf f_{i}$.
∎

###### Lemma D.2 (Monotonicity under leaf restriction) .

Let $S^{\prime}\!=\!S\cup\{\ell\}$ be a child of $S$ (hence $C(S^{\prime})\subseteq C(S)$).
Then for every $E$,
$\operatorname{LB}(E,S^{\prime})\ \geq\ \operatorname{LB}(E,S),\quad\operatorname{UB}(E,S^{\prime})\ \leq\ \operatorname{UB}(E,S).$

###### Proof.

For affines, shrinking the feasible set can only increase the minimum and
decrease the maximum. For composite forms, the rules in Lemma [D.1](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem1)
are nondecreasing in each argument, so the inequalities propagate by induction.
∎

###### Lemma D.1 (Soundness of structural LB/UB) .

###### Proof.

###### Lemma D.2 (Monotonicity under leaf restriction) .

###### Proof.

##### Anytime envelopes and DAG propagation.

Define the scalar envelopes on leaves by

$$ $\underline{A}_{S}:=\operatorname{LB}(E_{\rm out},S),\qquad\overline{A}_{S}:=\operatorname{UB}(E_{\rm out},S),$ $$

and aggregate pointwise over leaves containing $x$ by
$\underline{A}(x)=\sup\{\underline{A}_{S}:S\in\mathcal{L},\ x\in C(S)\},\,\overline{A}(x)=\inf\{\overline{A}_{S}:S\in\mathcal{L},\ x\in C(S)\}.$

###### Lemma D.3 (Anytime propagation over the SWT DAG) .

If each module output obeys $\operatorname{LB}\leq\text{true}\leq\operatorname{UB}$ on every leaf, then the
composed network’s envelopes computed with the same rules satisfy
$\underline{A}\leq A\leq\overline{A}$ pointwise.

###### Proof.

Exact analogue of Lemma [D.1](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem1) lifted to the network DAG:
each node’s LB/UB is computed from its inputs by order-preserving constructors,
hence preserves the local sandwich on each leaf; aggregation over leaves preserves
the inequality.
∎

###### Theorem D.4 (DYN–1: sound anytime envelopes) .

At any time, for all $x$ we have $\underline{A}(x)\leq A(x)\leq\overline{A}(x)$.

###### Proof.

Combine Lemma [D.1](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem1), Lemma [D.3](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem3), and the definition
of aggregation over current leaves $\mathcal{L}$.
∎

###### Lemma D.5 (Monotone tightening) .

Replacing a leaf $S$ by children $S^{\pm}$ or tightening any local LB/UB
(internal upgrade to exact LP/SOCP bounds) yields
$\underline{A}\uparrow$ and $\overline{A}\downarrow$ pointwise.

###### Proof.

Leaf split: Lemma [D.2](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem2) on each child plus the use of
$\sup/\inf$ in the aggregation. Tightening local bounds: monotone in arguments.
∎

###### Remark D.6 (Empirical evidence of monotonicity) .

The convergence plot of the Imax B&B on the GNN case study (report, p. 7,
“Fig 3: Imax B&B Convergence”) shows global lower/upper bounds tightening
monotonically with iterations, matching Lemma [D.5](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem5).

###### Lemma D.3 (Anytime propagation over the SWT DAG) .

###### Proof.

###### Theorem D.4 (DYN–1: sound anytime envelopes) .

###### Proof.

###### Lemma D.5 (Monotone tightening) .

###### Proof.

###### Remark D.6 (Empirical evidence of monotonicity) .

### D.2 Formal Refiners and Termination Conditions

We assume a budgeted environment with counters for #splits and #new guards, and
a fair scheduler over feasible leaves (every feasible undecided leaf is eventually
selected). Below, “commit” means *rewrite* the local subexpression on $S$
accordingly (e-graph update), without adding new faces.

Figure: Algorithm 2 ENSURE_SIGN$(z,S)$: on-demand sign decision for a gate

Figure: Algorithm 3 ENSURE_WINNER$(\{E_{i}\},S)$: on-demand winner for Max

Figure: Algorithm 4 ENSURE_COMMON_REFINE$(S;S_{1},S_{2})$: minimal common refinement

##### Termination conditions (local).

For ENSURE_SIGN, termination on a leaf occurs when either
$\operatorname{UB}(z,S)\leq 0$ or $\operatorname{LB}(z,S)\geq 0$ (commit), or after one split.
For ENSURE_WINNER, termination occurs when pruning + bounds yield a
unique winner (commit) or after inserting one comparator and splitting once.
For ENSURE_COMMON_REFINE, the loop terminates because the difference
set $D$ is finite; each iteration inserts at most one face and splits once.

### D.3 Proofs of DYN–1..7 and Certificate Formats

We now discharge the DYN-series guarantees. DYN–1 was proved in
Theorem [D.4](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem4). We proceed with DYN–2..7.

###### Definition D.7 (Local full refinement) .

A leaf $S\in\mathcal{L}$ is *locally fully refined* if (i) all gate/comparator
faces relevant to expressions feeding the output on $S$ are registered in $\mathcal{H}$,
and (ii) every output component collapses to a *single affine* on $C(S)$.

###### Theorem D.8 (DYN–2: exactness on locally fully refined leaves) .

If $S$ is locally fully refined, then on $C(S)$ we have
$\underline{A}=\overline{A}=A$ (componentwise for vector outputs).

###### Proof.

When all relevant Max/gate choices are disambiguated on $S$, each output is
represented by a single affine atom on $C(S)$; for affines the LB/UB rules are
*tight* equalities. Composing along the acyclic SWT preserves equality,
hence $\underline{A}_{S}=\overline{A}_{S}=A|_{C(S)}$. Aggregation over leaves does not
alter values on $C(S)$.
∎

###### Theorem D.9 (DYN–3: progress never regresses) .

Refining a leaf $S$ either (a) tightens its local LB/UB without changing its guard
set (commit), or (b) replaces $S$ by children $S^{\pm}$ confined to $C(S)$.
In either case, previously exact leaves remain exact, and $\underline{A}\uparrow$,
$\overline{A}\downarrow$ pointwise.

###### Proof.

Case (a): local commit rewrites the expression to a stricter form (e.g., an affine),
hence tightens bounds; monotonicity follows from Lemma [D.5](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem5).
Case (b): children restrict the domain (Lemma [D.2](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem2)) and replace $S$
in $\mathcal{L}$; exact leaves are disjoint from $S$ and unaffected. Global monotonicity
follows again from Lemma [D.5](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem5).
∎

###### Proposition D.10 (DYN–5: correctness of dominance pruning) .

If $\max_{x\in C(S)}(E_{\pi}(x)-E_{\pi^{\prime}}(x))\leq 0$, then candidate $\pi$ can never win
any Max on $C(S)$ and may be removed from the candidate set of $S$.

###### Proof.

For all $x\in C(S)$, $E_{\pi}(x)\leq E_{\pi^{\prime}}(x)$, so $\max\{E_{\pi}(x),E_{\pi^{\prime}}(x)\}=E_{\pi^{\prime}}(x)$ pointwise; thus $\pi$ is never selected.
∎

###### Definition D.7 (Local full refinement) .

###### Theorem D.8 (DYN–2: exactness on locally fully refined leaves) .

###### Proof.

###### Theorem D.9 (DYN–3: progress never regresses) .

###### Proof.

###### Proposition D.10 (DYN–5: correctness of dominance pruning) .

###### Proof.

##### Branch-and-bound driver and tri-valued answers.

Let $g$ be a scalar objective encoding a property/specification (e.g., margin,
difference to zero), and $D$ be the input domain. The B&B over leaves maintains
global $\underline{M}=\max_{S\subseteq D}\operatorname{LB}(g,S)$ and
$\overline{M}=\max_{S\subseteq D}\operatorname{UB}(g,S)$ in a max-gap policy.

###### Theorem D.11 (DYN–6: JIT decidability under finite refinement and fairness) .

Assume (i) only finitely many gate/comparator faces can be introduced (finite
network), and (ii) the scheduler is *fair* over feasible undecided leaves.
Then B&B returns one of three outcomes, all sound:
Proof (a finite set of leaves $\{S_{i}\}$ with $\operatorname{LB}(g,S_{i})\geq 0$ covering $D$),
Counterexample (some $S$ with $\operatorname{UB}(g,S)<0$ and a witness $x^{\star}$ from LP/SOCP),
or Unknown under budget (with the tightest-gap leaf $S^{\star}$ reported).
Moreover, without budget limits the procedure *terminates* with Proof or
Counterexample.

###### Proof.

Soundness follows from DYN–1 and the fact that $\operatorname{LB}$ is a true lower bound and
$\operatorname{UB}$ a true upper bound on each leaf. Under finiteness of faces and fairness,
there are only finitely many distinct GuardSets that can appear; each split either
(1) commits a local decision or (2) introduces a new face, strictly reducing the
set of undecided leaves. Eventually all leaves become locally fully refined for $g$
and thus affine; then the decision reduces to finitely many LP/SOCP obligations,
which terminate. Certificates:
“Proof” collects $\{\operatorname{LB}(g,S_{i})\geq 0\}$; “Counterexample” adds the
witness $x^{\star}$; “Unknown” names $S^{\star}$ with its residual gap.
∎

###### Theorem D.12 (DYN–7: static–dynamic pointwise equivalence) .

If $D$ admits a finite cover by locally fully refined leaves $\{S_{t}\}$, then
$A_{\rm JIT}(x)=A_{\rm stat}(x)=F(x)$ for all $x\in D$.

###### Proof.

On each $C(S_{t})$, DYN–2 gives $A_{\rm JIT}=F$. Static SWT equals $F$ pointwise
by SWT–1. The sets $C(S_{t})$ cover $D$, so equality holds everywhere on $D$.
∎

###### Theorem D.13 (DYN–4: budgeted complexity bounds) .

Let $B_{\textsf{split}}$ be the total number of leaf splits, $B_{\textsf{guard}}$ the
number of *new* guards inserted into $\mathcal{H}$ beyond the initial size
$|\mathcal{H}_{0}|$, and $|Q_{0}|$ the static structure-site bound (App. [C.3](https://arxiv.org/html/2510.17622v1#A3.SS3)).
Then:

$$ $\#\text{leaves}\ \leq\ 1+B_{\textsf{split}},\qquad|\mathcal{H}|\ \leq\ |\mathcal{H}_{0}|+B_{\textsf{guard}},$ $$

$$ $\#\text{SWT nodes/edges}\ \leq\ O\!\big(|Q_{0}|+B_{\textsf{guard}}\big),\qquad\#\text{LP/SOCP calls}\ \leq\ O\!\big(B_{\textsf{split}}+B_{\textsf{guard}}+|\mathcal{L}|\big).$ $$

###### Proof.

Each split replaces one leaf by two, so leaves grow by at most one: $1+B_{\textsf{split}}$.
Only newly registered faces grow $|\mathcal{H}|$; reusing existing faces costs zero.
The SWT graph is a shared DAG; adding a new guard may add $O(1)$ edges/nodes to carry
the two orientations, yielding the stated $O(|Q_{0}|+B_{\textsf{guard}})$ bound.
Per-iteration, each split/register triggers $O(1)$ LP/SOCP solves (local LB/UB for
finitely many sub-expressions and a feasibility probe); summing over all iterations
gives the last bound.
∎

###### Remark D.14 (Practical counters and empirical scales) .

In the experiments, forward equivalence errors concentrate at $10^{-6}\!\sim\!10^{-7}$,
and B&B split counts / LP calls scale roughly linearly with budgets, matching
Theorem [D.13](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem13). See the tables and plots in the report:
FFN robustness (pp. 1–3), CNN equivariance (pp. 4–5), and GNN/Imax (pp. 6–8).

###### Theorem D.11 (DYN–6: JIT decidability under finite refinement and fairness) .

###### Proof.

###### Theorem D.12 (DYN–7: static–dynamic pointwise equivalence) .

###### Proof.

###### Theorem D.13 (DYN–4: budgeted complexity bounds) .

###### Proof.

###### Remark D.14 (Practical counters and empirical scales) .

### D.4 Cost Model for Branch-and-Bound

Let a B&B iteration pick the maximum-gap leaf $S$ for an objective $g$.
We detail its costs and the linear dependence on candidate counts and solver calls.

##### Per-iteration costs.

- •
Bound eval. For $m$ sub-expressions touching $S$,
$O(m)$ LB/UB queries; affines cost one LP max and one LP min each (dual reuse).
- •
Refiner. One of: ENSURE_SIGN, ENSURE_WINNER
(or ENSURE_COMMON_REFINE) executes a *single* split and optionally
registers *one* new face (comparator/threshold).
- •
Cache reuse. All $(S,\text{query})$ LP/SOCP results are memoized,
so repeated visits amortize to sublinear cost in practice.

##### Global bounds with candidates.

Let $C_{\max}$ be the maximum number of active Max/gate candidates touching any leaf.
Then under dominance pruning (Prop. [D.10](https://arxiv.org/html/2510.17622v1#A4.Thmtheorem10)) and per-step single-face
insertion, the total number of winner comparisons performed up to termination or
budget is $O(B_{\textsf{guard}}+|\mathcal{L}|\cdot C_{\max})$.

##### Memory.

With guard uniqueness and e-graph sharing, memory scales as
$O(|Q_{0}|+B_{\textsf{guard}}+|\mathcal{L}|)$; unreachable leaves and dead sub-expressions
may be reclaimed by reference counting without affecting semantics.

Takeaway.
JIT–SWT maintains sound anytime envelopes (DYN–1), reaches exactness upon local
full refinement (DYN–2), never regresses (DYN–3), prunes dominated candidates
correctly (DYN–5), and—under finite faces and fairness—decides properties with
certificates or counterexamples (DYN–6), while tracking budgets linearly in the
work performed (DYN–4). These guarantees align with the empirical curves and
tables in the report.

## Appendix E Function Geometry and Optimization (GEO-1..GEO-5)

This appendix develops geometry and optimization on top of JIT–SWT:
(E.1) on-demand extraction of active fragments and *minimal common
refinements*; (E.2) decision-boundary polyhedral complexes and distances;
(E.3) extrema and Lipschitz on common convex domains with LP/SOCP or
closed forms; (E.4) vector/operator norms—tractable families and NP-hard
families with anytime bounds.

Throughout, guards are *closed*, GuardSets store indices into the global
library, and *local full refinement* means all relevant faces have been
registered and each output component is a single affine map on the leaf
(App. [D](https://arxiv.org/html/2510.17622v1#A4)).

### E.1 On-demand active fragment extraction and minimal common refinement (GEO-1)

##### Active fragments.

For a scalar output $F$, a triple $(S,w,b)$ is an *active fragment*
if $S$ is a leaf GuardSet and $F(x)=w^{\top}x+b$ on $C(S)$.
When $S$ is locally fully refined, $(S,w,b)$ is *determined*.

Figure: Algorithm 5 RegionExtract$(A,D)$: on-demand active fragments over $D$

###### Definition E.1 (Minimal common refinement on a leaf) .

Given two GuardSets $S_{1},S_{2}$, the *minimal common refinement* of a current
leaf $S$ w.r.t. $(S_{1},S_{2})$ is the finite family
$\{\,S\cup T:\ T\subseteq(S_{1}\cup S_{2})\setminus S,\ C(S\cup T)\neq\varnothing,\ \text{and no two children merge}\,\},$
obtained by inserting only faces in $(S_{1}\!\cup\!S_{2})\setminus S$ until the
target sub-expressions are *comparable/addable* on each child.

###### Lemma E.2 (Minimality and finiteness) .

Algorithm [5](https://arxiv.org/html/2510.17622v1#alg5) with ENSURE_COMMON_REFINE produces a
refinement satisfying Def. [E.1](https://arxiv.org/html/2510.17622v1#A5.Thmtheorem1). The loop terminates because
$(S_{1}\cup S_{2})\setminus S$ is finite, and each iteration inserts at most one face.

###### Proof.

Each iteration chooses a face in the finite difference set and splits $S$ once.
No superfluous face is added because the loop stops as soon as the sub-expressions
become comparable/addable; hence minimality. Finiteness is immediate.
∎

###### Theorem E.3 (GEO–1: correctness and coverage) .

At any time, the set $\mathcal{R}$ returned by RegionExtract is a family of
pairwise interior-disjoint polyhedra $\{C(S)\}$ on which $F$ equals the recorded
affine law. If refinement proceeds until $D$ is covered by locally fully refined
leaves, $\mathcal{R}$ is a complete CPWL region table on $D$.

###### Proof.

Local full refinement implies single-affine and hence exact readout on each leaf.
Leaf splits only subdivide $C(S)$ (closed guards, face-compatible), so interiors
do not overlap. Finite coverage yields a region table by union.
∎

###### Definition E.1 (Minimal common refinement on a leaf) .

###### Lemma E.2 (Minimality and finiteness) .

###### Proof.

###### Theorem E.3 (GEO–1: correctness and coverage) .

###### Proof.

### E.2 Decision-boundary polyhedral complexes (GEO-3)

Let $F:\mathbb{R}^{n}\!\to\!\mathbb{R}^{m}$ be CPWL; for $i\neq j$, define the margin
$g_{ij}=F_{i}-F_{j}$. On a locally fully refined leaf $S$, $g_{ij}(x)=w_{\rho,ij}^{\top}x+b_{\rho,ij}$ is affine.

###### Theorem E.4 (Piecewise-flat decision set) .

Let $D$ be a convex domain and assume $D$ is covered by locally fully refined
leaves $\{S_{\rho}\}$. Then

$$ $DB_{ij}:=\{x\in D:\ g_{ij}(x)=0\}=\bigcup_{\rho}\Bigl(C(S_{\rho})\cap\{w_{\rho,ij}^{\top}x+b_{\rho,ij}=0\}\Bigr),$ $$

a finite polyhedral complex whose pieces are faces of codimension at most 1,
pairwise face-compatible.

###### Proof.

On each $C(S_{\rho})$ the zero set of an affine function is an affine hyperplane
(or empty or the whole cell). Intersecting with polyhedra preserves polyhedra and
face-compatibility. Finiteness follows from the finite cover.
∎

###### Proposition E.5 (Local distance to the boundary) .

For $x\in\operatorname{ri}(C(S_{\rho}))$ and $w_{\rho,ij}\neq 0$,
$\mathrm{dist}\!\left(x,DB_{ij}\cap C(S_{\rho})\right)=\frac{|w_{\rho,ij}^{\top}x+b_{\rho,ij}|}{\|w_{\rho,ij}\|_{2}}.$

###### Theorem E.4 (Piecewise-flat decision set) .

###### Proof.

###### Proposition E.5 (Local distance to the boundary) .

##### Anytime inner/outer approximations.

Without full refinement, use the envelopes $\underline{g}_{ij},\overline{g}_{ij}$ to
obtain
$\{x:\ \overline{g}_{ij}(x)\leq 0\}\subseteq\{x:\ g_{ij}(x)\leq 0\}\subseteq\{x:\ \underline{g}_{ij}(x)\leq 0\}.$
Refining the maximal-gap leaves (App. [D](https://arxiv.org/html/2510.17622v1#A4)) shrinks the sandwich.

### E.3 Extrema and Lipschitz on common convex domains (GEO-2/GEO-5)

Let $D$ be a convex feasible set (polytope/box/$\ell_{p}$ ball or their intersections).

##### Anytime global extrema.

Maintain
$\underline{M}=\max_{S\subseteq D}\operatorname{LB}(F,S),\ \ \overline{M}=\max_{S\subseteq D}\operatorname{UB}(F,S),$
which satisfy $\underline{M}\leq\max_{x\in D}F(x)\leq\overline{M}$ and tighten
monotonically (DYN–1/3). When leaves over $D$ are locally fully refined, each
subproblem is *affine maximization* and solved exactly.

###### Theorem E.6 (Affine maximization on standard domains) .

Let $f(x)=w^{\top}x+b$. Then:

- 1.
Polytope $D=\{x:Ax\leq d\}$: LP
$\max\{w^{\top}x+b:Ax\leq d\}$.
- 2.
Box $D=[\ell,u]$: closed form
$\max w^{\top}x+b=\sum_{i}w_{i}\,(\,u_{i}\mathbf{1}_{w_{i}\geq 0}+\ell_{i}\mathbf{1}_{w_{i}<0}\,)+b$.
- 3.
$\ell_{\infty}$-ball $D=B_{\infty}(x_{0},\epsilon)$: LP; closed form
$w^{\top}x_{0}+b+\epsilon\|w\|_{1}$.
- 4.
$\ell_{1}$-ball $D=B_{1}(x_{0},\epsilon)$: LP via epigraph
$\sum_{i}t_{i}\leq\epsilon,\ -t_{i}\leq x_{i}-x_{0,i}\leq t_{i}$; closed form
$w^{\top}x_{0}+b+\epsilon\|w\|_{\infty}$.
- 5.
$\ell_{2}$-ball $D=B_{2}(x_{0},\epsilon)$: SOCP or closed form
$w^{\top}x_{0}+b+\epsilon\|w\|_{2}$.
- 6.
Polytope$\cap\ell_{2}$-ball: SOCP
$\max\{w^{\top}x+b:\ Ax\leq d,\ \|x-x_{0}\|_{2}\leq\epsilon\}$.

###### Proof.

(1) is linear programming; (2) coordinatewise choice; (3)(4) are $\ell_{1}/\ell_{\infty}$
duality; (5) follows from Cauchy–Schwarz; (6) is a standard second-order cone form.
∎

###### Theorem E.6 (Affine maximization on standard domains) .

###### Proof.

##### Exact Lipschitz after refinement (scalar).

For $F$ scalar and $D$ covered by locally fully refined leaves,

$$ $L_{p}(F;D)=\max_{S:\,C(S)\cap D\neq\varnothing}\ \|w_{S}\|_{p^{*}}.$ $$

*Anytime bounds* use refined leaves for the lower bound and safe relaxations
for unresolved leaves for the upper bound (e.g., interval slopes or layerwise
operator-norm products).

##### Vector case.

For $F:\ell_{p}\to\ell_{r}$, with Jacobian $J_{S}$ on each refined leaf,

$$ $L_{p\to r}(F;D)=\max_{S:\,C(S)\cap D\neq\varnothing}\ \|J_{S}\|_{p\to r}.$ $$

Before full refinement, use
$\underline{L}=\max_{S\ \text{refined}}\|J_{S}\|_{p\to r},\ \overline{L}=\max_{S}U_{p\to r}(S),$
where $U_{p\to r}(S)$ is any sound leaf-wise upper bound (e.g., bounding
intermediate slopes by LP/SOCP or multiplying induced norms layerwise).

### E.4 Vector/operator norms: tractable vs NP-hard, and anytime handling

For a matrix $A\in\mathbb{R}^{m\times n}$,
$\|A\|_{p\to r}:=\sup_{\|x\|_{p}=1}\|Ax\|_{r}$.
The following families are computationally *tractable* (polynomial):

###### Proposition E.7 (Closed forms and efficient computation) .

For any $A$:

$$ $\displaystyle\|A\|_{1\to 1}=\max_{j}\sum_{i}|a_{ij}|\quad(\text{max column sum}),$ $\displaystyle\|A\|_{\infty\to\infty}=\max_{i}\sum_{j}|a_{ij}|\quad(\text{max row sum}),$ $\displaystyle\|A\|_{1\to\infty}=\max_{i,j}|a_{ij}|,$ $\displaystyle\|A\|_{2\to 2}=\sigma_{\max}(A)\quad(\text{spectral norm; power/SVD}),$ $\displaystyle\|A\|_{2\to\infty}=\max_{i}\|A_{i,:}\|_{2},\qquad\|A\|_{1\to 2}=\max_{j}\|A_{:,j}\|_{2}.$ $$

The next families are *NP-hard* in general, hence used with anytime
lower/upper bounds at unresolved leaves:

###### Proposition E.8 (NP-hard families (decision version)) .

Computing $\|A\|_{\infty\to 1}$, $\|A\|_{\infty\to 2}$, or $\|A\|_{2\to 1}$ is
NP-hard. Consequently exact global $L_{p\to r}(F;D)$ for these pairs reduces to
maximizing an NP-hard quantity over leaves; nevertheless JIT yields *anytime*
bounds that converge upon full refinement when a leaf-wise exact oracle is available
or when unresolved leaves shrink to zero measure.

###### Proposition E.7 (Closed forms and efficient computation) .

###### Proposition E.8 (NP-hard families (decision version)) .

##### Anytime scheme on JIT leaves.

For each leaf $S$:

- •
Lower bound $\underline{L}_{S}$: choose any $v$ with $\|v\|_{p}=1$ and
evaluate $\|J_{S}v\|_{r}$; for $2\to 2$, one power-iteration step gives a valid
$\|J_{S}v\|_{2}$; for $\infty\to 1$, use a sign vector $v\in\{\pm 1\}^{n}$.
- •
Upper bound $\overline{L}_{S}$: relaxations by dual norms, Gershgorin-type
bounds, or layerwise induced-norm products inside the leaf (tightened by LP/SOCP
when gates are unresolved but ranges are bounded).
- •
Aggregation: $\underline{L}=\max_{S\ \text{refined}}\underline{L}_{S}$ and
$\overline{L}=\max_{S}\overline{L}_{S}$; monotone tightening follows from DYN–1/3.

##### Complexity remarks.

GEO‑1..5 are *decidable* under the finite-refinement/fairness hypotheses
(App. [D](https://arxiv.org/html/2510.17622v1#A4)); worst-case exponential (number of reachable fragments),
but budgeted cost obeys the linear upper bounds of DYN–4. Leaf-wise LP/SOCP
obligations are polynomial and—empirically—dominate runtime.

Takeaway.
Geometry (regions/boundaries/gradients) and optimization (extrema/Lipschitz)
reduce on JIT to small LP/SOCP problems on a local common refinement, with
*anytime* bounds (DYN–1/3) and *exactness on demand* (DYN–2).
This matches the FFN/CNN/GNN observations in the experiment report.

## Appendix F Verification, Equivariance, and Causality (VER-1/2/3, CAU-1/2)

This appendix formalizes the property language and the *product transducer*
construction (F.1), derives robustness certification procedures including
LP/SOCP subproblems and *tight big-M* from GuardSet bounds (F.2), treats
equivariance for CNNs (effective domains under stride/padding) and GNNs
(F.3), and proves closure and anytime/exact computation of causal influence
$I_{\max}$ via branch-and-bound (F.4). All results are consistent with the
JIT–SWT semantics and guarantees in App. [D](https://arxiv.org/html/2510.17622v1#A4).

### F.1 Property language and product construction (VER-1)

##### Atomic predicates.

Let $F:\mathbb{R}^{n}\to\mathbb{R}^{m}$ be compiled to an SWT (static) and run under JIT semantics.
We consider universally quantified properties over a convex input set $D$:

$$ $\displaystyle\phi\;::=\;$ $\displaystyle x\in D\ \wedge\ \bigwedge_{k\in\mathcal{K}}\psi_{k}(x),$ $\displaystyle\psi_{k}(x)\;::=\;$ $\displaystyle\underbrace{F_{i}(x)\geq\ell}_{\text{lower threshold}}\ \big|\ \underbrace{F_{i}(x)\leq u}_{\text{upper threshold}}\ \big|\ \underbrace{F_{y}(x)-\max_{j\neq y}F_{j}(x)\geq\gamma}_{\text{classification margin}}$ $\displaystyle\big|\ \underbrace{|F(x)-F^{\prime}(x)|_{\infty}\leq\varepsilon}_{\text{relational/equivalence}}\ \big|\ \underbrace{a^{\top}F(x)\geq b}_{\text{linear output constraint}}$ $$

where $F^{\prime}$ is another SWT or a specification transducer (e.g., symmetry).

##### Violation objectives.

Each atomic predicate is reduced to a CPWL *objective* $g_{k}:\mathbb{R}^{n}\to\mathbb{R}$
for which “$g_{k}(x)\geq 0$” encodes satisfaction:

$$ $\displaystyle F_{i}\geq\ell\ \leadsto\ g_{k}(x)=F_{i}(x)-\ell,\qquad F_{i}\leq u\ \leadsto\ g_{k}(x)=u-F_{i}(x),$ $\displaystyle F_{y}-\max_{j\neq y}F_{j}\geq\gamma\ \leadsto\ g_{k}(x)=F_{y}(x)-\max_{j\neq y}F_{j}(x)-\gamma,$ $\displaystyle|F-F^{\prime}|_{\infty}\leq\varepsilon\ \leadsto\ g_{k}(x)=\varepsilon-\max_{r}|F_{r}(x)-F_{r}^{\prime}(x)|,$ $\displaystyle a^{\top}F\geq b\ \leadsto\ g_{k}(x)=a^{\top}F(x)-b.$ $$

Conjunction $\bigwedge_{k}\psi_{k}$ is handled by $g(x)=\min_{k}g_{k}(x)$, and we
finally check $\forall x\in D:\ g(x)\geq 0$. Since $\min$ is implementable as
$-\max$ of CPWL terms, $g$ remains CPWL.

##### Product transducer.

Write $A_{F}=(Q_{F},E_{F},\mathsf{G}_{F},\mathsf{W}_{F})$ for (the relevant part of) the SWT
of $F$ and $A_{g}=(Q_{g},E_{g},\mathsf{G}_{g},\mathsf{W}_{g})$ for the transducer computing
$g$ from the network outputs (built only from $\mathsf{Max}/\mathsf{Sum}/\mathsf{Scale}/\mathsf{Bias}$ on CPWL
weights). Define the product

$$ $A_{\otimes}=\big(Q_{F}\times Q_{g},\ E_{\otimes},\ \mathsf{G}_{\otimes},\ \mathsf{W}_{\otimes}\big),$ $$

with edges $((p,\alpha)\!\to\!(q,\beta))$ whenever $(p\!\to\!q)\in E_{F}$ and
$(\alpha\!\to\!\beta)\in E_{g}$, guard $\mathsf{G}_{\otimes}=\mathsf{G}_{F}\cap\mathsf{G}_{g}$
(guard-index union), and weight $\mathsf{W}_{\otimes}=\mathsf{W}_{F}\otimes\mathsf{W}_{g}$
(semiring $+$). As both components are CPWL-weighted and guards are polyhedral,
$A_{\otimes}$ is again a guarded CPWL transducer.

###### Theorem F.1 (VER–1: product correctness and decidability) .

Let $g$ be constructed from $\phi$ as above and $D$ be convex. Running JIT B&B
(App. [D](https://arxiv.org/html/2510.17622v1#A4)) on $A_{\otimes}$ over $D$ yields a tri-valued outcome:
Proof (a finite leaf cover $\{S_{i}\}$ with $\operatorname{LB}(g,S_{i})\geq 0$),
Counterexample (a leaf $S$ with $\operatorname{UB}(g,S)<0$ and a witness $x^{\star}$),
or Unknown under budget—all *sound*. Under finite refinement and
fair selection, the procedure terminates with Proof or
Counterexample.

###### Proof.

Soundness is DYN–1: $\operatorname{LB}\leq g\leq\operatorname{UB}$ on every leaf. If all active leaves
satisfy $\operatorname{LB}\geq 0$ and cover $D$, then $g\geq 0$ on $D$. If some leaf has
$\operatorname{UB}<0$, solving $\min_{x\in C(S)\cap D}g(x)$ (LP/SOCP on refined leaves)
produces a witness $x^{\star}$. Termination under finite faces and fairness is
DYN–6; the product preserves CPWL/guarded structure, so the assumptions apply.
∎

###### Theorem F.1 (VER–1: product correctness and decidability) .

###### Proof.

##### Certificate format.

A proof returns $\{(S_{i},\operatorname{LB}(g,S_{i}))\}$ whose polyhedra cover $D$. A
counterexample returns $(S,x^{\star},g(x^{\star}))$ with feasibility KKT/solver logs
(optionally) and the active guard indices on $S$.

### F.2 Robustness certification: LP/SOCP and tight big- M M (VER-2)

We consider the local robustness property around $(x_{0},y)$:

$$ $\forall x\in D\cap B_{p}(x_{0},\epsilon):\quad g(x):=F_{y}(x)-\max_{j\neq y}F_{j}(x)\ \geq\ \gamma\quad(\gamma\geq 0).$ $$

##### Method A: exact convex subproblems on refined leaves.

Once leaves covering $D\cap B_{p}(x_{0},\epsilon)$ are *locally fully refined*,
$g(x)=w_{S}^{\top}x+b_{S}$ on each $S$. Then the global minimum is

$$ $\min_{x\in D\cap B_{p}(x_{0},\epsilon)}g(x)=\min_{S}\ \min_{x\in C(S)\cap D\cap B_{p}(x_{0},\epsilon)}(w_{S}^{\top}x+b_{S}),$ $$

where each inner problem is LP for polytope/$\ell_{\infty}/\ell_{1}$ and SOCP for
$\ell_{2}$ or polytope$\cap\ell_{2}$ (App. [E.3](https://arxiv.org/html/2510.17622v1#A5.SS3)). The minimum across
leaves is exact.

###### Theorem F.2 (VER–2A: robustness via leafwise convex programs) .

The procedure above yields an *anytime* lower bound
$\underline{g}_{\min}\leq\min g$ that increases monotonically with refinement
and equals the exact minimum once the domain is covered by fully refined leaves.
Hence the property “$g\geq\gamma$” is *decidable* (finite refinement) with
either a certificate $\min g\geq\gamma$ or a counterexample $x^{\star}$.

###### Proof.

DYN–1 gives $\operatorname{LB}$ monotonicity; exactness on refined leaves follows from
GEO–2 and DYN–2.
∎

###### Theorem F.2 (VER–2A: robustness via leafwise convex programs) .

###### Proof.

##### Method B: MIP with tight big- M M from GuardSet bounds.

On a leaf $S$, some gates/comparators may remain unresolved; introduce binary
variables $\delta\in\{0,1\}$ to encode branch selection and use leaf-specific
bounds to build *tight* big-$M$ constraints.

ReLU. Let $z=w^{\top}x+b$ with leaf-wise interval
$L\leq z\leq U$ obtained from $[\operatorname{LB},\operatorname{UB}]$. With $y=\max\{0,z\}$:

$$ $\displaystyle y\ \geq\ z,\qquad y\ \geq 0,$ $\displaystyle y\ \leq\ z-L(1-\delta),\qquad y\ \leq\ U\,\delta,\qquad\delta\in\{0,1\}.$ $$

If $U\leq 0$ (resp. $L\geq 0$), $\delta$ can be fixed to 0 (resp. $1$) and
constraints reduce to the affine branch.

Pointwise Max. For $y=\max_{i}e_{i}(x)$ with leaf-wise bounds
$L_{i}\leq e_{i}(x)\leq U_{i}$, introduce $\delta_{i}\in\{0,1\}$ with
$\sum_{i}\delta_{i}=1$ and

$$ $y\ \geq\ e_{i}(x)\ \ \forall i,\qquad y\ \leq\ e_{i}(x)+(U_{\max,-i})\,(1-\delta_{i})\ \ \forall i,$ $$

where $U_{\max,-i}=\max_{j\neq i}U_{j}-\!L_{i}$ (tightest valid $M$ on $S$).

###### Lemma F.3 (Tightness on a leaf) .

The big-$M$ values above are *minimal valid* on $C(S)$: decreasing any
$M$ violates feasibility for some $x\in C(S)$. Consequently, the linear
relaxations are the strongest among all big-$M$ encodings that use only
interval information of the involved expressions on $S$.

###### Proof.

For ReLU, $y\leq z-L(1-\delta)$ must hold for $z=L$ when $\delta=0$; any smaller
$M$ cuts off the true point $(z=L,y=0)$. Similarly $y\leq U\delta$ must hold at
$z=U$ with $\delta=1$. For Max, the $i$-th upper constraint must accommodate any
$j\neq i$ with $e_{j}=U_{j}$ while $e_{i}=L_{i}$; hence $M\geq U_{j}-L_{i}$, and the maximum
over $j\neq i$ is necessary.
∎

###### Theorem F.4 (VER–2B: correctness of big- $M$ robustness) .

On any leaf $S$, the MIP built from the constraints above is *exact* for the
encoded subgraph; if all leaves covering $D\cap B_{p}(x_{0},\epsilon)$ are included
(and comparators modeled where needed), the resulting global MIP decides robustness
with a certificate (dual bound $\geq\gamma$) or a counterexample. Using the linear
relaxation yields a sound lower bound on the margin (no false proofs).

###### Proof.

Exactness per leaf with binaries follows from standard mixed-integer encodings and
Lemma [F.3](https://arxiv.org/html/2510.17622v1#A6.Thmtheorem3). Global correctness is a disjoint union of leaf models
(over closed guards), which covers $D\cap B_{p}$; soundness of relaxations follows
from over-approximation of the feasible set.
∎

###### Lemma F.3 (Tightness on a leaf) .

###### Proof.

###### Theorem F.4 (VER–2B: correctness of big- M M robustness) .

###### Proof.

### F.3 Equivariance checking and effective domains (VER-3)

##### Abstract statement.

Given an input transform $\mathcal{T}_{g}:\mathbb{R}^{n}\!\to\!\mathbb{R}^{n}$ and an output transform
$\mathcal{T}^{\prime}_{g}:\mathbb{R}^{m}\!\to\!\mathbb{R}^{m}$, we check

$$ $H(x)\ :=\ F(\mathcal{T}_{g}x)\ -\ \mathcal{T}^{\prime}_{g}(F(x))\ \equiv\ 0\quad\text{on }D.$ $$

Construct an SWT for $H$ by composing $A_{F}$ with the transducers of
$\mathcal{T}_{g}$ and $\mathcal{T}^{\prime}_{g}$; then run JIT B&B on $|H|$ with a tolerance
$\varepsilon$ (if approximate equivariance is desired).

##### CNN translations: effective domain and admissible shifts.

Consider a planar CNN with $L$ convolutional (or pooling) layers, kernel sizes
$k_{\ell}$ (odd), paddings $p_{\ell}\geq 0$, and strides $s_{\ell}\in\mathbb{N}$; activations
are pointwise (ReLU/Leaky/Abs/MaxPool). Let the set of admissible integer shifts be

$$ $\mathcal{S}_{\mathrm{adm}}=\big\{\,\Delta\in\mathbb{Z}^{2}:\ \Delta\ \text{is a multiple of }\ s_{\mathrm{tot}}=\textstyle\prod_{\ell=1}^{L}s_{\ell}\,\big\},$ $$

so that downsampling aligns on the output grid. For a finite shift set
$\mathcal{S}\subseteq\mathcal{S}_{\mathrm{adm}}$, define the *effective domain*
$D_{\mathrm{eff}}$ by cropping the input with a safety margin

$$ $M\ :=\ \max_{\Delta\in\mathcal{S}}\|\Delta\|_{\infty}\ +\ \sum_{\ell=1}^{L}\max\!\Big(0,\ \big\lfloor\tfrac{k_{\ell}-1}{2}\big\rfloor-p_{\ell}\Big),$ $$

i.e., the set of inputs whose every receptive field of radius
$\lfloor(k_{\ell}-1)/2\rfloor$ stays strictly inside the unpadded region
for all shifts in $\mathcal{S}$.

###### Theorem F.5 (Sufficient condition for CNN translation equivariance) .

For any $\Delta\in\mathcal{S}$ and any $x\in D_{\mathrm{eff}}$, a CNN as above
satisfies
$F(\mathcal{T}_{\Delta}x)=\mathcal{T}^{\prime}_{\Delta}(F(x))$
exactly, where $\mathcal{T}_{\Delta}$ is the input shift and $\mathcal{T}^{\prime}_{\Delta}$
is the corresponding shift on the final feature grid. If $\varepsilon\geq 0$,
then $\|F(\mathcal{T}_{\Delta}x)-\mathcal{T}^{\prime}_{\Delta}(F(x))\|_{\infty}\leq\varepsilon$
holds by running VER–1 with the objective $\varepsilon-|H|$.

###### Proof.

Convolution commutes with discrete translation on positions whose receptive
fields do not cross the padded boundary; the crop margin $M$ enforces this for
all layers. Pointwise activations commute with translation. For strides, restricting
to shifts multiple of $s_{\mathrm{tot}}$ preserves grid alignment. Composition
yields the claim by induction over layers.
∎

###### Theorem F.5 (Sufficient condition for CNN translation equivariance) .

###### Proof.

##### GNN permutation equivariance.

Let $P$ be a node-permutation matrix for a fixed graph structure, and let
$\mathcal{T}_{P}(X)=PX$ on features with the corresponding output permutation
$\mathcal{T}^{\prime}_{P}(Y)=PY$. For sum/mean aggregation and pointwise MLP updates,

$$ $F(PX)=P\,F(X)\quad\text{holds on all }X,$ $$

since permutation commutes with degree-normalized adjacency in these cases.
Thus VER–1 checks exact or $\varepsilon$-equivariance by the same product
construction with $H(X)=F(PX)-PF(X)$.

### F.4 Causal interventions and maximal influence (CAU-1/2)

##### Intervention model and closure.

Let the SWT DAG contain a sub-expression $E$ (e-graph node). An intervention
$C$ replaces $E$ by a CPWL policy $P_{c}$, producing a new network $F_{C}$ with the
same graph shape. Because CPWL is closed under $\mathsf{Max}/\mathsf{Sum}/\mathsf{Scale}/\mathsf{Bias}$ and
affine composition, both $F_{C}$ and the pointwise difference
$g_{C}(x)=F(x)-F_{C}(x)$ are CPWL.

###### Theorem F.6 (CAU–1: closure under CPWL interventions) .

For any intervention $C$ that replaces a sub-expression by a CPWL policy,
$F_{C}$ and $g_{C}=F-F_{C}$ are CPWL on $\mathbb{R}^{n}$ and admit guarded SWT/JIT compilations
with the same guard library extended by faces introduced by $P_{c}$.

###### Proof.

By structural induction using the CPWL closure from App. [B](https://arxiv.org/html/2510.17622v1#A2) and the guarded
composition rules of App. [C](https://arxiv.org/html/2510.17622v1#A3): replacing one CPWL component preserves CPWL of the
whole; subtraction preserves CPWL as $\text{CPWL}-\text{CPWL}=\text{CPWL}$.
∎

###### Theorem F.6 (CAU–1: closure under CPWL interventions) .

###### Proof.

##### Maximal causal influence.

Given a convex domain $D$ and a vector norm $\|\cdot\|_{r}$, define

$$ $I_{\max}(C;D)\ :=\ \sup_{x\in D}\ \|g_{C}(x)\|_{r}.$ $$

Run B&B on the scalar objective $h(x)=\|g_{C}(x)\|_{r}$ with anytime envelopes.

###### Theorem F.7 (CAU–2: anytime bounds and exactness on refinement) .

Let $\underline{I}=\max_{S\subseteq D}\operatorname{LB}(h,S)$ and
$\overline{I}=\max_{S\subseteq D}\operatorname{UB}(h,S)$ be the global bounds maintained by
B&B. Then $\underline{I}\leq I_{\max}\leq\overline{I}$ and
$\underline{I}\nearrow,\ \overline{I}\searrow$ with refinement.
If leaves covering $D$ are locally fully refined and $r=\infty$, then

$$ $I_{\max}=\max_{S}\ \max_{i}\ \max\big\{\max_{x\in C(S)\cap D}(a_{S,i}^{\top}x+b_{S,i}),\ \max_{x\in C(S)\cap D}(-a_{S,i}^{\top}x-b_{S,i})\big\},$ $$

where $g_{C}(x)=(A_{S}x+b_{S})$ on leaf $S$ and the inner maxima are LPs,
yielding an *exact* value; for $r\in\{1,2\}$ one obtains anytime bounds by
leafwise convex majorants and induced-norm arguments.

###### Proof.

Anytime bounds follow from DYN–1/3 applied to $h$. For $r=\infty$, on each
refined leaf $h(x)=\max_{i}|a_{S,i}^{\top}x+b_{S,i}|$, so $I_{\max}$ is the
maximum of finitely many affine maxima (LPs) over a finite leaf cover, hence
exact. For $r\in\{1,2\}$, use $\|A_{S}x+b_{S}\|_{r}\leq\|A_{S}\|_{p\to r}\|x\|_{p}+\|b_{S}\|_{r}$
when $D$ includes an $\ell_{p}$ ball and standard SOCP/LP upper bounds otherwise;
lower bounds arise from evaluating at candidate points or directions.
∎

###### Theorem F.7 (CAU–2: anytime bounds and exactness on refinement) .

###### Proof.

##### Complexity and certificates.

The total number of local solves is linear in the number of splits and newly
introduced faces (DYN–4). A proof returns either a global upper bound
$\overline{I}$ below a threshold of interest or an exact $I_{\max}$ with the
attaining leaf and witness points (LP/SOCP solutions); a counterexample is any
$x$ with $\|g_{C}(x)\|_{r}$ exceeding a user threshold.

Summary.
VER–1 provides a uniform reduction of properties to CPWL objectives via a
product construction; VER–2 discharges robustness either exactly on refined
leaves by LP/SOCP or via tight big-$M$ MIPs using GuardSet bounds; VER–3 gives
sufficient conditions and a practical domain for CNN translation (and GNN
permutation) equivariance; and CAU–1/2 show that CPWL interventions preserve
closure and admit certified anytime (and exact for $\|\cdot\|_{\infty}$) computation
of maximal causal influence.

## Appendix G Micro-Pseudocode and Detailed Complexity

### G.1 Counters, Cost Model, and Caching Interface

##### Per-leaf structural counters.

For a current leaf $S$ and the scalar output expression $E_{\mathrm{out}}$:

- •
$a(S)$: # of distinct affine atoms $\mathsf{Affine}(w,b)$ reachable from $E_{\mathrm{out}}$ on $S$;
- •
$m(S)$: # of Max nodes touched on $S$;
- •
$c(S)$: # of *active* candidates across all Max/gates on $S$ after dominance pruning;
- •
$g(S)$: # of undecided sign tests (ReLU/LReLU/PReLU/Abs) on $S$;
- •
$d(S)$: # of distinct comparator/threshold faces from parents $(S_{1},S_{2},\ldots)$ needed to compare/add sub-expressions on $S$ (for minimal common refinement).

##### LP/SOCP cost primitives.

- •
Affine LB/UB on $S$: two LPs on $C(S)$ (or one LP by dual reuse plus a sign switch);
- •
$\ell_{2}$ ball (or polytope$\cap\ell_{2}$): one SOCP per bound;
- •
Feasibility of $C(S)$: one LP; cached thereafter.

##### Caching and keys.

A bound query uses key $\langle S,\mathrm{id}(E),\mathrm{sense}\rangle$, where $\mathrm{sense}\in\{\operatorname{LB},\operatorname{UB}\}$.
If a leaf $S$ is split into children $S^{\pm}$, cached bounds on $S$ serve as *warm starts* but are not reused verbatim; children recompute exact local bounds. We expose:

$$ $\texttt{CacheHitRate}=h_{\mathrm{LP}}\in[0,1],\quad\texttt{CacheReuseFactor}=\rho\in[0,1],$ $$

so the expected LP calls per affine-bound query is $(1-h_{\mathrm{LP}})\cdot(1-\rho)+\rho\cdot\text{(reduced)}$.
All complexity bounds below are presented as *worst-case* ($h_{\mathrm{LP}}{=}0$) and *amortized* (symbolic $h_{\mathrm{LP}}$).

##### Global refinement counters.

Let $B_{\textsf{split}}$ be the total #leaf splits, $B_{\textsf{guard}}$ the #new faces inserted into $\mathcal{H}$ (beyond the initial library), and $\mathcal{L}$ the current leaf set. Denote $|Q_{0}|$ the static structure-site bound (states/templates from the compilation graph).

### G.2 LB/UB Engine: Fine-Grained Pseudocode and Cost

Figure: Algorithm 6 EvalBoundsOnLeaf$(S,E)$: structural LB/UB on a leaf $S$

##### Cost per call.

Let $a_{S}$ be the #affine leaves of the syntax DAG of $E$ reachable on $S$ (after e-graph sharing).

$$ $\text{LPs per call of {EvalBoundsOnLeaf}}\ \leq\ 2\,a_{S}\cdot(1-h_{\mathrm{LP}}),\qquad\text{SOCPs}\ \leq\ 2\,a_{S}^{(\ell_{2})}\cdot(1-h_{\mathrm{LP}}).$ (1) $$

All other constructors are $O(1)$ arithmetic on scalars.

### G.3 ENSURE_SIGN : Pseudocode and Complexity

Figure: Algorithm 7 ENSURE_SIGN$(z,S)$ (local)

##### Per-invocation cost and bound.

One call makes at most one *threshold insertion* and one *split*.
Bound cost $\leq 2\,a_{z}(1-h_{\mathrm{LP}})$ LPs (from $z$); no other LPs are mandatory.
Hence over the whole run,

$$ $\#\text{thresholds}\ \leq\ B_{\textsf{guard}},\qquad\#\text{splits}\ \leq\ B_{\textsf{split}}.$ $$

### G.4 ENSURE_WINNER : Pseudocode, Pruning, and Complexity

Figure: Algorithm 8 ENSURE_WINNER$(\{E_{i}\}_{i=1}^{k},S)$ (local)

##### Per-invocation LP bound.

Let $k^{\prime}$ be the remaining candidates after pruning. Then

$$ $\text{LPs}\ \leq\ 2\,\Big(\sum_{i=1}^{k^{\prime}}a_{S}(E_{i})\Big)\cdot(1-h_{\mathrm{LP}}),$ $$

where $a_{S}(E_{i})$ is #affine atoms under $E_{i}$ reachable on $S$.
Each call inserts *at most one* comparator face and makes *one split*.

##### Total comparator bound.

Because each call inserts a single face, total introduced comparators is
$\leq B_{\textsf{guard}}$; this *strictly* improves over static all-pairs
$\sum\binom{k_{v}}{2}$.

### G.5 ENSURE_COMMON_REFINE : Pseudocode and Complexity

Figure: Algorithm 9 ENSURE_COMMON_REFINE$(S;S_{1},S_{2})$

##### Complexity.

The loop performs at most $|S_{1}\cup S_{2}|-|S|$ iterations; each iteration makes
one split and may insert one new face. No mandatory LPs are required unless
feasibility of a child is queried.

### G.6 B&B Driver: Micro-Policy, Certificates, and Complexity

Figure: Algorithm 10 JIT-B&B$(A,D,g)$: any-time solver on objective $g$

##### Per-iteration LP/SOCP bound.

Let $A_{g}(S)$ be the #affine atoms of $g$ reachable on $S$.
Then one B&B iteration makes at most

$$ $2\,A_{g}(S)\cdot(1-h_{\mathrm{LP}})+\Theta(1)\quad\text{LPs}\qquad(\text{plus SOCPs if $D$ involves $\ell_{2}$ balls}),$ $$

for bound updates, plus the cost of the chosen refiner as in
Sections [G.3](https://arxiv.org/html/2510.17622v1#A7.SS3)–[G.5](https://arxiv.org/html/2510.17622v1#A7.SS5).
If $\operatorname{UB}(g,S)<0$, an additional LP/SOCP is solved to obtain $x^{\star}$.

##### Certificates (format).

Proof: a finite cover $\{(S_{i},\operatorname{LB}(g,S_{i})\geq 0)\}$; Counterexample:
$(S,x^{\star},g(x^{\star}))$; Unknown: $(S^{\star},\operatorname{LB},\operatorname{UB})$.

### G.7 End-to-End Bounds, Amortization with Caching, and Proofs

###### Theorem G.1 (Global guard/leaf/cardinality bounds) .

With budgets $(B_{\textsf{split}},B_{\textsf{guard}})$ and initial guard size $|\mathcal{H}_{0}|$,

$$ $\#\mathrm{leaves}\ \leq\ 1+B_{\textsf{split}},\qquad|\mathcal{H}|\ \leq\ |\mathcal{H}_{0}|+B_{\textsf{guard}},\qquad\#\mathrm{nodes/edges}\ \leq\ O(|Q_{0}|+B_{\textsf{guard}}).$ $$

###### Proof.

Each split replaces one leaf by two (leaf count $+1$). Only registering a *new*
face increases $|\mathcal{H}|$. The shared SWT DAG grows only along edges touched by
new faces; each face triggers $O(1)$ additions, giving $O(|Q_{0}|+B_{\textsf{guard}})$.
∎

###### Theorem G.2 (Total LP/SOCP calls: worst-case and amortized) .

Let $A^{\star}=\max_{S\in\mathcal{L}_{\max}}A_{g}(S)$ be the peak affine-atom count of $g$
on any visited leaf, and let $\kappa$ be a constant bounding the number of sub-expressions
whose bounds are refreshed per iteration. Then

$$ $\#\mathrm{LP}\ \leq\ O\!\big((B_{\textsf{split}}+B_{\textsf{guard}}+|\mathcal{L}|)\cdot\kappa\cdot A^{\star}\big)\quad\text{(worst-case, no cache)},$ $$

and, with hit rate $h_{\mathrm{LP}}$,

$$ $\mathbb{E}[\#\mathrm{LP}]\ \leq\ (1-h_{\mathrm{LP}})\cdot O\!\big((B_{\textsf{split}}+B_{\textsf{guard}}+|\mathcal{L}|)\cdot\kappa\cdot A^{\star}\big).$ $$

The same holds for SOCPs when $\ell_{2}$ balls are present (with $A^{\star}$ restricted to
affines whose domains couple to $\ell_{2}$ constraints).

###### Proof.

Per iteration bound from Section [G.6](https://arxiv.org/html/2510.17622v1#A7.SS6); multiply by the number of
iterations (bounded by $B_{\textsf{split}}+B_{\textsf{guard}}+|\mathcal{L}|$ since each
iteration either commits or inserts a single face and splits once). Amortized form
follows by linearity of expectation with hit rate $h_{\mathrm{LP}}$.
∎

###### Theorem G.3 (Comparator/threshold insertions and candidate complexity) .

Let $C_{\max}=\max_{S}c(S)$ be the peak active-candidate count per leaf after
dominance pruning. Under the single-face-per-step policy,
the total number of winner comparisons introduced is $O(B_{\textsf{guard}}+|\mathcal{L}|C_{\max})$.

###### Proof.

Each call of ENSURE_WINNER inserts at most one comparator. Across at most
$|\mathcal{L}|$ active leaves and $C_{\max}$ candidates per leaf, the number of
*attempted* comparisons is bounded by $|\mathcal{L}|C_{\max}$; only a subset
materializes into registered faces, upper bounded by $B_{\textsf{guard}}$.
∎

###### Corollary G.4 (Memory) .

With guard uniqueness and e-graph sharing, memory is
$O(|Q_{0}|+B_{\textsf{guard}}+|\mathcal{L}|)$; reclaiming unreachable leaves and dead
sub-expressions (reference counting) keeps this bound tight during execution.

###### Theorem G.1 (Global guard/leaf/cardinality bounds) .

###### Proof.

###### Theorem G.2 (Total LP/SOCP calls: worst-case and amortized) .

###### Proof.

###### Theorem G.3 (Comparator/threshold insertions and candidate complexity) .

###### Proof.

###### Corollary G.4 (Memory) .

### G.8 Correctness of Caching and Monotone Tightening

###### Lemma G.5 (Cache correctness under splits) .

Let a cached pair $(\operatorname{LB}(E,S),\operatorname{UB}(E,S))$ be exact on leaf $S$. After splitting $S$
into children $S^{\pm}$, the cached pair remains a valid *outer* sandwich on
each child: $\operatorname{LB}(E,S)\leq\inf_{x\in C(S^{\pm})}E(x)\leq\sup_{x\in C(S^{\pm})}E(x)\leq\operatorname{UB}(E,S)$;
recomputing on $S^{\pm}$ tightens these bounds (monotone).

###### Proof.

$C(S^{\pm})\subseteq C(S)$; thus $\inf_{C(S^{\pm})}\!\geq\!\inf_{C(S)}$ and
$\sup_{C(S^{\pm})}\!\leq\!\sup_{C(S)}$, giving a valid (possibly loose) sandwich.
Exact recomputation on $S^{\pm}$ cannot be looser than the parent bounds.
∎

###### Theorem G.6 (Global monotonicity with caching) .

If cached bounds are only replaced by tighter values and leaves are only refined
by splits or commits, then the global anytime envelopes satisfy
$\underline{A}\uparrow$ and $\overline{A}\downarrow$ pointwise during the whole run.

###### Proof.

Immediate from Lemma [G.5](https://arxiv.org/html/2510.17622v1#A7.Thmtheorem5) and the order-preserving constructors of
the LB/UB engine (App. [G.2](https://arxiv.org/html/2510.17622v1#A7.SS2)): local tightening propagates
monotonically through the DAG and the leaf aggregation ( $\sup/\inf$ ).
∎

Takeaway.
The micro-algorithms in §[G.3](https://arxiv.org/html/2510.17622v1#A7.SS3)–[G.6](https://arxiv.org/html/2510.17622v1#A7.SS6) ensure each step
(*i*) inserts at most one face and makes at most one split, (*ii*) triggers
a constant number of bound-refresh calls, and (*iii*) benefits linearly from
caching. Theorems [G.1](https://arxiv.org/html/2510.17622v1#A7.Thmtheorem1)–[G.6](https://arxiv.org/html/2510.17622v1#A7.Thmtheorem6) provide verifiable upper bounds
and establish correctness and anytime monotone tightening for the full JIT–SWT loop.

###### Lemma G.5 (Cache correctness under splits) .

###### Proof.

###### Theorem G.6 (Global monotonicity with caching) .

###### Proof.

## Appendix H Extended Experimental Details and Additional Results

This appendix expands the empirical section with full protocols, hyper‑parameters, and additional visualizations for the three case studies: (A) FFN on MNIST, (B) CNN on CIFAR‑10, and (C) GNN on the Karate Club graph.

### H.1 Experiment A: FFN—Local Lipschitz vs. Robustness

##### Goal.

Validate that the JIT‑SWT compiler recovers the local affine piece at a queried input and use it to estimate the *per‑sample* local Lipschitz constant; evaluate its correlation with single‑step adversarial robustness (FGSM).

##### Setup.

- •
Data. MNIST with standard train/test splits and normalization. Code: transforms.ToTensor() + Normalize((0.1307,),(0.3081,)).
- •
Model. FFN $784\!\to\!128\!\to\!64\!\to\!10$ with ReLU activations. Training: Adam, lr$=10^{-3}$, 5 epochs, CE loss.
- •
Compiler. SWT_Compiler compiles the per‑sample local affine piece $(W,b)$; the local Lipschitz is $\|W\|_{2}$.
- •
Adversary. FGSM with $\epsilon=0.25$ in input space; attack is evaluated on the top/bottom‑$N$ samples ranked by local Lipschitz (with $N=50$).

##### Protocol.

For each correctly classified test sample $x$, compile a local affine piece $f(x^{\prime})\equiv Wx^{\prime}+b$ in a neighborhood of $x$. Record the per‑sample max absolute forward discrepancy $|f(x)-A(x)|_{\infty}$ and the local Lipschitz $\|W\|_{2}$. Then attack the top‑$N$ (High‑L) and bottom‑$N$ (Low‑L) groups using FGSM; report attack success rate (ASR).

##### Results.

The average dynamic compilation error across $9760$ correctly classified samples is $1.13\times 10^{-6}$ ([Figure 4](https://arxiv.org/html/2510.17622v1#A8.F4)). The empirical distribution of per‑sample local Lipschitz values concentrates between 2 and 7 ([Figure 5](https://arxiv.org/html/2510.17622v1#A8.F5)). The High‑L group has mean $6.6012$ vs. $2.2332$ for Low‑L.
Under FGSM $\epsilon=0.25$, ASR is $100\%$ for High‑L and $14\%$ for Low‑L ([Table 3](https://arxiv.org/html/2510.17622v1#A8.T3)), confirming a strong positive correlation between local Lipschitz and adversarial susceptibility.

**Table 3: FFN—Local Lipschitz and robustness summary.**
| Avg dynamic compile error (9760 samples) | $1.13\times 10^{-6}$ |
| --- | --- |
| Global Lipschitz upper bound $L_{\text{upper}}$ | $22.9303$ |
| Avg local‑L (Top 50) | $6.6012$ |
| Avg local‑L (Bottom 50) | $2.2332$ |
| ASR (Top 50, $\epsilon=0.25$) | $100.00\%$ |
| ASR (Bottom 50, $\epsilon=0.25$) | $14.00\%$ |

Figure: Figure 4: FFN per‑sample dynamic compilation error on MNIST (log scale): max absolute discrepancy between compiled affine piece and PyTorch forward across correctly classified test samples; mean shown as dashed line.
Refer to caption: Sample.png

Figure: Figure 5: Distribution of per‑sample local Lipschitz constants ($\ell_{2}$) on the MNIST test set.
Refer to caption: Distribution.png

### H.2 Experiment B: CNN—Translation Equivariance

##### Goal.

Validate compiler applicability to CNNs and quantify translation equivariance under small integer shifts; visualize boundary effects.

##### Setup.

- •
Data. CIFAR‑10 subset: 1000 train and 200 test images per class (normalized to mean/std 0.5).
- •
Model. CNN_A: $\text{Conv(3$\to$16,3$\times$3,s=1,p=1)}\to$ReLU$\to\text{Conv(16$\to$32,3$\times$3,s=1,p=1)}\to$ReLU$\to$GlobalAvgPool$\to$Linear(32$\to$10); trained for 5 epochs with Adam (lr$=10^{-3}$), CE loss.
- •
Shifts. All $(\Delta x,\Delta y)\in\{-1,0,1\}^{2}\setminus\{(0,0)\}$ with zero padding upon rolling.
- •
Test. For 100 random test images, we compile a local piece before and after shift and compare class predictions; we report pass rate and a heatmap of failures over $(\Delta x,\Delta y)$.

##### Results.

Mean per‑sample dynamic compilation error over 100 images is $1.36\times 10^{-7}$ ([Figure 6](https://arxiv.org/html/2510.17622v1#A8.F6)). The equivariance pass rate over all shifts is $\mathbf{0.850}$. Failures concentrate on diagonal shifts, consistent with boundary effects introduced by padding/stride ([Figure 7](https://arxiv.org/html/2510.17622v1#A8.F7)).

Figure: Figure 6: CNN per‑sample dynamic compilation error on CIFAR‑10 (log scale).
Refer to caption: CNN.png

Figure: Figure 7: Equivariance failure heatmap over $(\Delta x,\Delta y)\in\{-1,0,1\}^{2}\!-\!\{(0,0)\}$; brighter indicates more failures. Diagonals (e.g., $(-1,-1)$, $(-1,1)$) account for most failures due to boundary padding.
Refer to caption: Equivariance.png

### H.3 Experiment C: GNN—Property Verification and Causal Influence

##### Goal.

(1) Verify compilation equivalence and permutation equivariance for a two‑layer GCN; (2) quantify *maximum causal influence* (Imax) of hidden channels via intervention under bounded input perturbations; (3) confirm Imax as an importance signal by ablation.

##### Setup.

- •
Graph. Zachary’s Karate Club ($|V|{=}34$). Features: node degree, clustering coefficient, and first 4 Laplacian eigenvectors (standardized).
- •
Model. GCNConv–ReLU–GCNConv–ReLU–Linear with hidden dim 16; trained 200 epochs (Adam, lr$=10^{-2}$) on the full graph.
- •
Compilation & Verifications. SWT_Compiler with node‑wise shapes and normalized adjacency; (i) *Compilation equivalence:* random noisy inputs around the training features; (ii) *Permutation equivariance:* 50 random node permutations with degree‑normalized adjacency recomputed per permutation.
- •
Imax (B&B). For each hidden channel $k\!\in\!\{0,\dots,15\}$, we intervene by zeroing channel $k$ at layer 2 and compute
$I_{\max}\!=\!\sup_{\|X-X_{0}\|_{\infty}\leq 0.1}\!\|F(X)-F_{C}(X)\|_{\infty}$
by a branch&bound solver over an $\ell_{\infty}$ ball (§[H.3.1](https://arxiv.org/html/2510.17622v1#A8.SS3.SSS1)); we then ablate Top‑5 / Bottom‑5 channels and compare accuracies.

##### Results.

Compilation equivalence (100 probes): mean error $2.17\times 10^{-6}$, max $3.77\times 10^{-6}$ ([Figure 8](https://arxiv.org/html/2510.17622v1#A8.F8)). Permutation equivariance (50 perms): mean error $6.80\times 10^{-15}$, max $1.07\times 10^{-14}$ ([Figure 9](https://arxiv.org/html/2510.17622v1#A8.F9)). The Imax B&B convergence for channel 0 is shown in [Figure 10](https://arxiv.org/html/2510.17622v1#A8.F10). Ranking all channels by Imax produces the Top‑5 $\{0,1,8,11,12\}$ and Bottom‑5 $\{4,6,7,10,13\}$ ([Figure 11](https://arxiv.org/html/2510.17622v1#A8.F11)). Ablating Top‑5 reduces accuracy from $100\%$ to $97.06\%$ (drop $2.94\%$), while ablating Bottom‑5 has no impact ($100\%$ vs. $100\%$); see [Figure 12](https://arxiv.org/html/2510.17622v1#A8.F12) and [Table 4](https://arxiv.org/html/2510.17622v1#A8.T4).

Figure: Figure 8: GNN compilation equivalence: per‑probe max absolute error (log scale).
Refer to caption: Compilation.png

Figure: Figure 9: Permutation equivariance across 50 random permutations: histogram of max absolute errors (log scale).
Refer to caption: GNN.png

Figure: Figure 10: Imax B&B convergence for channel 0: global lower/upper bounds over iterations and uncertainty gap.
Refer to caption: Channel_0.png

Figure: Figure 11: Imax distribution across 16 hidden channels; Top‑5 (salmon) and Bottom‑5 (light green) highlighted.
Refer to caption: Imax.png

Figure: Figure 12: Ablation study: baseline vs. removing Top‑5 vs. removing Bottom‑5 channels.
Refer to caption: Performance_Impact.png

**Table 4: GNN—verification and Imax ablation summary.**
| Max compilation error | $3.77\times 10^{-6}$ |
| --- | --- |
| Mean compilation error | $2.17\times 10^{-6}$ |
| Max equivariance error | $1.07\times 10^{-14}$ |
| Mean equivariance error | $6.80\times 10^{-15}$ |
| Baseline accuracy | $100.00\%$ |
| Accuracy after removing Top‑5 | $97.06\%$ |
| Performance drop (Top‑5) | $2.94\%$ |
| Accuracy after removing Bottom‑5 | $100.00\%$ |
| Performance drop (Bottom‑5) | $0.00\%$ |

#### H.3.1 Imax branch&bound details

We consider the $\ell_{\infty}$ ball $\{X:\|X\!-\!X_{0}\|_{\infty}\leq 0.1\}$; its H‑representation is
$A=\begin{bmatrix}I\\
-I\end{bmatrix},\,d=\begin{bmatrix}X_{0}+\epsilon\\
-(X_{0}-\epsilon)\end{bmatrix},$
with $\epsilon=0.1$ and $X_{0}$ the baseline features (vectorized). On each B&B node, a feasible center is obtained via LP; both the original and intervened models are compiled at that point to local affine forms, whose difference yields per‑facet lower/upper bounds on $\|F-F_{C}\|_{\infty}$. Subdomains are split along the dimension with largest interval range, halving at the mid‑point, until budget/precision criteria are met. Implementation: BranchAndBoundSolver using SciPy HiGHS.

## Appendix I Implementation and Robustness Details (Reproducibility)

This section records engineering decisions that make our results easy to reproduce and stress‑test. Wherever possible we point to the precise implementation sites in the released code.

### I.1 ReLU guard polarity and tie handling

Guard polarity. When a pre‑activation $z_{i}(x)=w_{i}^{\top}x+b_{i}$ passes through ReLU, the active (non‑negative) branch should add the guard

$$ $z_{i}(x)\geq 0\iff(-w_{i})^{\top}x\leq b_{i},$ $$

and the inactive (non‑positive) branch should add

$$ $z_{i}(x)\leq 0\iff\;w_{i}^{\top}x\leq-\,b_{i}.$ $$

In the reference implementation, the polarity is encoded in ReLuTransition.apply by appending one linear inequality per unit to the current guard (H‑polytope). Concretely, the active branch correctly appends A += -w_i, d += -b_i, whereas the inactive branch should append A += +w_i, d += -b_i. If you see d += b_i on the inactive branch, flip the sign to -b_i to match the formulas above (one‑line fix).

Ties. The theoretical semantics use *closed* guards on both sides of the hinge so that the $z_{i}(x)=0$ hyperplane is covered from either side. In code we detect activity by a strict test on the numeric pre‑activation (pre_act_flat > 0) and thus fall to the “negative” side at exact tie. If desired, you can (i) add a tolerance band and duplicate both guards when $|z_{i}(x)|\leq\tau$, or (ii) keep closed guards by switching to >= on the active side and <= on the inactive side; the global tolerance constant lives at FP_TOLERANCE = 1e-5.

##### Where to patch.

compiler.py $\rightarrow$ ReLuTransition.apply and the file‑level constant FP_TOLERANCE.

### I.2 Consistent scipy.linprog bounds

We solve small LPs inside the branch‑and‑bound (B&B) loop. Recommendation: pass explicit per‑variable bounds as $\texttt{bounds}=[(\texttt{None},\texttt{None})]\times n$ for all calls. This avoids backend‑specific behavior and makes the code portable across SciPy versions.

*Where used.* (i) In Guard.is_feasible(), bounds are already constructed per dimension. (ii) In BranchAndBoundSolver._get_bounds_in_guard() we set bounds=[(None,None)] * input_dim (good). (iii) In BranchAndBoundSolver.solve() the range queries use bounds=(None,None); although accepted by SciPy as a global bound pair, we recommend unifying it to the list form for consistency. All three sites are in compiler.py.

### I.3 Convolutional Jacobians: practicality and a matrix‑free option

What the release does. The current Conv2dTransition.apply materializes the linear map of a convolution by building an *im2col‑style* matrix $W_{\mathrm{conv}}\in\mathbb{R}^{(C_{\text{out}}H_{\text{out}}W_{\text{out}})\times(C_{\text{in}}H_{\text{in}}W_{\text{in}})}$ and composing it with the running affine piece $(W,b)$. This is exact and works well at the CIFAR‑10 scale we use (32$\times$32) but can be memory‑heavy for larger inputs.

Matrix‑free alternative (recommended for large inputs). Replace the explicit $W_{\mathrm{conv}}$ with a *linear operator* that supports the actions $v\mapsto W_{\mathrm{conv}}v$ and $u\mapsto W_{\mathrm{conv}}^{\top}u$ using PyTorch’s conv primitives:

$$ $W_{\mathrm{conv}}v\;\equiv\;\mathrm{conv}(v\ \text{reshaped}),\qquad W_{\mathrm{conv}}^{\top}u\;\equiv\;\mathrm{conv_transpose}(u\ \text{reshaped}).$ $$

Then propagate the affine piece without ever constructing $W_{\mathrm{conv}}$ explicitly. This drop‑in operator fits our automaton because every composition step only needs the product $W_{\mathrm{new}}\!\cdot\!W$ and $W_{\mathrm{new}}\!\cdot\!b$. In practice, implement a small wrapper class with matvec and rmatvec, and gate between the dense and matrix‑free paths by input size. The convolution path in the CNN experiment invokes SWT_Compiler(..., initial_shape=(3,32,32)) and then hits Conv2dTransition during trace.

Note. Our GCN path already avoids materializing the graph conv Jacobian symbolically; it computes the linear map by probing the layer with basis vectors once and reuses the result, which is tractable on Karate Club. For larger graphs, the same matrix‑free pattern applies.

### I.4 CNN translation fill value after normalization

When CIFAR‑10 images are normalized to mean 0.5 and std 0.5, the dynamic range is roughly $[-1,1]$. In the shift_image routine we currently zero‑fill the wrapped border after torch.roll, which injects a mid‑gray value and slightly biases the equivariance test at the padded faces. To emulate “black” padding in the normalized space, set the border to $-1$ instead of 0:

This function lives in exp2.py under the CNN experiment.

### I.5 Entry point, seeds, and deterministic settings

Single entry point. All experiments can be reproduced via

$$ python run.py --exp {1,2,3} $$

for FFN/CNN/GNN respectively. The dispatcher is defined in run.py.

Seeding and determinism. We fix a global seed ($\texttt{SEED}=2025$) and set deterministic flags for CUDA/cuDNN at module import time; this covers PyTorch RNGs and reduces non‑determinism during convolutions. See the seed block at the top of compiler.py.

Data loaders. The FFN/CNN training loops use standard PyTorch data loaders; in the CIFAR‑10 setup we set num_workers=2. For byte‑for‑byte determinism, set num_workers=0 and shuffle=False (or fix the sampler seed) during training; evaluation and all compiler‑based analyses are deterministic given the saved weights. The MNIST/CIFAR‑10 pipelines and model definitions reside in exp1.py and exp2.py; the GNN pipeline (Karate) is in exp3.py.

##### B&B solver knobs.

The Imax computation uses a compact branch‑and‑bound with LP relaxations; max_iter and tolerance control the budget/precision trade‑off. See BranchAndBoundSolver and its use sites in the GNN experiment.

## Peer Reviews

confidence: 5
contribution: 3
initial_rating: 2
presentation: 1
questions: 1. Can the authors provide a clearer roadmap of how the theorem families (AF, SWT, DYN, GEO, VER, CAU) relate to each other and to the overall method? Specifically, which results are novel contributions versus foundational CPWL preliminaries?
2. The scope of the paper in the literature is lacking; there are literally hundreds of papers on neural network verification now, and the paper cites <10, none more recent than 2020. Either can the authors place the paper better in the existing vast literature and compare it qualitatively to what exists, or add comparisons against VNN-COMP benchmarks (and participating tools, eg, Marabou, alpha-beta-Crown, nnenum, NNV, NeuralSAT, Pyrat, etc.) and report wall-clock time, memory usage, and certified accuracy compared?
3. The decidability result (DYN-6) assumes finite refinement and fairness. In practice, how often does the system return UNKNOWN under realistic budgets?
soundness: 2
strengths: - The problem formulation is clear. Unrolling ReLU layer-by-layer results in exponentially growing computational complexity. This paper proposed a principled approach with formal guarantees. 
- Guard-sharing and unified representation are neat contributions. Inserting comparator faces only when needed yields better computational complexity. Having a single object support multiple verification tasks (Lipschitz, robustness) through a common LP/SOCP interface could meaningfully simplify verification pipelines.
summary: The paper proposes JIT-SWT, a just-in-time semantics for analyzing ReLU-type networks as continuous piecewise-linear (CPWL) functions. The main idea is to compile networks into guarded transducers with shared guards, then refine on-demand rather than enumerating all fragments upfront. This method could avoid the computational explosion and will benefit the scalability aspect of tasks, including computing Lipschitz constant, robustness checking, etc. The main contributions are summarized as follows:
1. The framework for calculus and static compilation rules for CPWL NNs. 
2. JIT refinement with soundness guarantee and complexity bounds. 
3. Geometry and verification procedures leveraging the shared carrier
4. Experiments on MNIST/CIFAR-10/Karate Club demonstrating compiler correctness and correlations with network properties
weaknesses: - The paper is hard to read. The main text still feels like navigating a theorem catalog rather than a coherent story. The paper is dense with theorem families and heavy notations. It lacks descriptions of theoretical results and their role in the proposed method. Table 1 helps a bit, but a major streamlining pass is needed. 
- Results AF-1 through AF-5 appear to be standard CPWL preliminaries (closure, continuity, differentiability). The paper should explicitly delineate which theoretical results are novel versus which are foundational background, making it easier to assess the core technical contributions.
- The experiments lack comparisons with existing works. We have no information about runtime and memory consumption relative to state-of-the-art tools, like benchmarks in VNN-COMP. Without baseline comparisons, the practical value remains unclear.

---

confidence: 4
contribution: 3
initial_rating: 6
presentation: 3
questions: 1. You mention "certified PL lifts for multiplicative modules" (like Attention/Softmax) as future work. Do you envision these relaxations fitting neatly into the current SWT guard structure, or will they require a fundamental redesign of the semantic carrier to handle fundamentally non-linear/non-convex regions efficiently?
2. Comparison with Incomplete Verifiers: How does JIT-SWT compare in wall-clock time against state-of-the-art incomplete verifiers (such as $\alpha,\beta$-CROWN) when the goal is only to find a sound bound rather than an exact one? Does the overhead of the unified SWT structure make it competitive for purely bounded verification tasks on larger networks?
3. Sensitivity to Scheduler & Budget: The decidability guarantees rely on a "fair scheduler" and sufficient budgets. In practice, how sensitive is the quality of the returned bounds to the choice of micro-policy (e.g., max-gap vs. round-robin) when operating under tight computational budgets?
soundness: 3
strengths: 1. Unified Theoretical Framework: The primary strength is the unification of disparate geometric and formal tasks into a single symbolic carrier. Instead of specialized algorithms for Lipschitz estimation vs. robustness verification, the JIT-SWT provides a common substrate where these become differing objectives on the same refinement engine.
2. Anytime Guarantees & Monotonicity: The proofs for sound anytime envelopes (DYN-1) and monotonic progress without regression (DYN-3) are theoretically satisfying. This allows the method to act as both an exact verifier (given enough time) and an approximate certifier under budget constraints.
3. Budgeted Complexity: Explicitly bounding the complexity (number of active GuardSets, library size) linearly by the number of splits and inserted guards (DYN-4) is a strong theoretical contribution, distinguishing it from purely exponential worst-case static analysis.
4. Decidability: The proof that properties expressible with finite affine/SOC constraints are decidable under fair JIT refinement strategies (DYN-6) places the method on solid formal ground.
summary: The paper proposes a "Just-in-Time" (JIT) Symbolic Weighted Transducer (SWT) framework to model ReLU-based neural networks. Unlike traditional static analysis that suffers from exponential explosion by eagerly materializing all regions, this approach performs on-demand refinement. It maintains sound anytime lower/upper envelopes and guarantees exactness when cells are locally fully refined. The authors demonstrate that this unified "carrier" can support diverse tasks—including region extraction, exact Jacobian computation, Lipschitz estimation, robustness verification, and causal influence analysis—by reducing them to sequence of local Linear Programming (LP) or Second-Order Cone Programming (SOCP) problems.
weaknesses: 1. Scalability Concerns: While "JIT" mitigates immediate exponential explosion, the reliance on solving LPs/SOCPs in the inner loop of the Branch-and-Bound driver 8 represents a significant computational bottleneck. The experimental validation is limited to very small-scale problems (MNIST FFNs, subsets of CIFAR-10 with tiny CNNs, Karate Club GNNs). There is little evidence this approach can scale to standard Deep RL policy networks (e.g., ResNet-50 size or Transformer-based policies), where the number of active paths can be overwhelmingly large even for local properties.
2. Restriction to CPWL: The framework is rigorously defined only for CPWL networks (affine + Max/ReLU type gates). Modern state-of-the-art architectures, particularly in RL (Transformers, world models), rely heavily on non-CPWL operations like Softmax, Attention, and LayerNorm. The paper notes this limitation and suggests "sound PL relaxations" as future work11, but without this, its applicability to current high-impact models is severely limited.
3. Practicality of "Exact" Metrics: While exact Lipschitz or $I_{max}$ computation is theoretically appealing, in many DL/RL applications, tight upper bounds (obtainable faster via specialized abstract interpretation methods like $\alpha,\beta$-CROWN) are often sufficient. The paper does not extensively compare the cost-benefit ratio of JIT-SWT against state-of-the-art incomplete verifiers on larger benchmarks.

---

confidence: 3
contribution: 3
initial_rating: 6
presentation: 2
questions: Is this approach the first one of its kind? Have other solutions been proposed in the past? How does JIT-SWT compare to them? If it is the first of its kind, what were the challenges in the past that prevented JIT-SWT from happening? What were the insights that allowed to overcome these challenges?

What are the scalability limits of this approach?

Can more concepts be moved into the appendix so there is room for more intuitions and examples that can help readers who are not very familiar with this topic understand the quality of this work?
soundness: 3
strengths: Originality: The formalization seem novel and the idea of bridging algebraic formalisms and neural verification seems new.

Quality: Comprehensive theoretical framework with proofs of soundness, decidability, and budgeted complexity bounds.
summary: The paper introduces Just-in-Time Symbolic Weighted Transducers (JIT-SWT) as an execution semantics for CPWL neural networks.

Rather than completely expanding a ReLU network's exponentially large region decomposition, JIT-SWIT builds a guarded CPWL transducer and refines it on demand during the analysis.

The framework support sound any time envelopes, exactness on fully refined cells, formal reasoning tasks, and some experiments on FFNs, CNNs, GNNs.
weaknesses: Accessibility: The main text is quite dense and does not provide enough background, motivation, or illustrations for several of the definitions and proofs in the paper. A brief paragraph before each definition or at the beginning of each subsection providing an intuition on why the concepts are needed, or how they work at an intuitive level would be appreciated.

Scalability: Experiments are on small networks and restricted settings. A clearer discussion on when this can be applied and when it cannot would be appreciated.

Related work: It is not clear if this is the only solution out there for neural verification, geometry, and causal analysis. Are there other solutions that could be used for this? If yes, how does this compare to them? In which regards is this solution better?

---

confidence: 2
contribution: 3
initial_rating: 4
presentation: 1
questions: 1. Have you compared your algorithm to other state-of-the-art methods, and if so, how does it perform?
soundness: 3
strengths: Owed to requirements in many applications, the formal analysis of learned functions, particularly neural networks, is receiving and has received significant attention in ML research in the recent years. This paper introduces a (to my knowledge) completely novel idea in this context. The algorithm is highly flexible in tackling a wide range of different analysis tasks. The paper evaluates this new method thoroughly from a theoretical perspective. Detailed proofs are provided in an appendix.
summary: The paper introduces a new neural network reasoning method based on a compilation of the network into an automaton with polyhedral edge guards and node and edge weight matrices. The authors show that any neural network with piecewise linear activation functions can be represented exactly in this automata language. A dynamic ("just in time") expansion of the automaton is developed to analyze different properties (e.g., robustness, equivalence, etc) over the network's input-output behavior. To this end, the method features mechanisms to propagate input constraints and to introduce dynamically additional hyperplanes refining the guards if necessary. A thorough theoretical analysis studies a wide range of properties of this method, such as correctness and completeness for different analysis tasks, and the connection to concepts from geometry. A small empirical study show cases the flexibility of the developed method.
weaknesses: The write-up is very dense. Essentially, the main text is just a lose connection of different theoretical results, without providing a clear coherent story, or even explaining how the proposed method works exactly. Some of the introduced processing steps seem to be needed for some specific analysis task only, yet the paper lacks any sort of explanation when some steps are executed, in which order, and what context they are relevant. An overview of the overall method such as in the form of pseudocode would greatly improve comprehensibility. As it stands now, the paper is impossible to digest for non-expert readers. The general telegraph style of the write-up is not exactly beneficial for the clarity either.

The purpose of the experimental evaluation is also unclear. Given that the authors propose a new method for existing and well-researched problems, I would expect to see a comparison to state-of-the-art methods. Nevertheless, the authors just ran their methods on three different analysis tasks and different network architectures. This might show case the versatility of the proposed method, but apart from this it is not clear what to conclude from the results. Questions like the following remain open, but are really what should be shown in the empirical study: How does the method scale? Are the shown results in any sense "impressive", e.g., in terms of dealing with network sizes so far beyond reach or handling properties that were so far not considered? How is the method placed with respect to other approaches? How effective is the algorithm, in terms of bound propagation and in terms of the number on-demand splits generated vs. unfolding the complete computation tree.

The paper certainly makes a major contribution, but given its current presentation and the unclear experiment design, it needs another thorough revision.


Decision: Reject