Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks
This work addresses the challenge of formal verification and analysis of neural networks for researchers and practitioners in machine learning and AI, offering a novel approach with practical applications in robustness and interpretability.
The paper tackles the problem of analyzing ReLU-type neural networks by developing a just-in-time piecewise-linear semantics system that compiles models into guarded continuous piecewise-linear transducers with shared guards. The result is a method that achieves anytime soundness, exactness on fully refined cells, monotone progress, guard-linear complexity, and supports various analysis tasks like region extraction, Jacobians, and certified Lipschitz bounds.
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.