Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks
Not on the map. Why?
Abstract (arXiv)
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 binomk2), 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.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 4 of its 10 references that are in the map. First posted on arXiv 20 Oct 2025.
Builds on
4 of 10 references.
References · 4
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 739
- 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 564
- 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
- 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
Built on by
Not cited yet.