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

TL;DR

This work introduces a just‑in‑time Symbolic Weighted Transducer (SWT) to provide exact, certificate‑driven analysis of ReLU‑type networks by modeling them as guarded CPWL maps. The static SWT encodes networks with a shared guard library and polyhedral guards, enabling on‑demand refinement via JIT–SWT that maintains sound envelopes and never regresses. Key contributions include CPWL closure results, a dynamic refinement framework with three refiners, and decidability under finite refinement, along with a geometry/verification pipeline (regions, Jacobians, Lipschitz, robustness, equivariance, causality) that reduces to tractable LP/SOCP steps and yields certificates or counterexamples. The approach yields machine‑precision forward equivalence and actionable geometric insights (e.g., local Lipschitz relating to adversarial robustness) across FFN, CNN, and GNN experiments, providing a scalable, certificate‑driven alternative to solver‑centric verification. Practical impact lies in enabling per‑region readouts, certified robustness bounds, and causal analyses on standard architectures with rigorous guarantees under finite refinement budgets.

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 $\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.

Figures (12)

• 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.
• Figure 2: Static SWT compilation pipeline. Layer $\rightarrow$ guard intersections $\rightarrow$ candidate fragments $\rightarrow$ comparator guards $\rightarrow$ winner regions.
• 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.
• 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.
• Figure 5: Distribution of per‑sample local Lipschitz constants ($\ell_2$) on the MNIST test set.

Theorems & Definitions (118)

• Theorem 2.1: SWT‑1: equivalent compilation; proof in App. \ref{['app:swt:equiv']}
• Theorem 3.2: DYN‑1: sound anytime envelopes; App. \ref{['app:jit:lbub']}
• Definition 3.3: Local full refinement
• Theorem 3.4: DYN‑2: exactness on $C(S)$; App. \ref{['app:jit:refiners']}
• Theorem 3.5: DYN‑3: progress never regresses; App. \ref{['app:jit:refiners']}
• Theorem 3.6: DYN‑4; App. \ref{['app:jit:cost']}
• Proposition 3.7: DYN‑5; App. \ref{['app:jit:dyn-proofs']}
• Theorem 3.8: DYN‑6: JIT‑decidability; App. \ref{['app:jit:dyn-proofs']}
• Definition 3.9: Complete refinement cover
• Theorem 3.10: DYN‑7; App. \ref{['app:jit:dyn-proofs']}