Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks
Logic in Computer Science
2025-10-21 v1 Machine Learning
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 ), 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.
Cite
@article{arxiv.2510.17622,
title = {Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks},
author = {Hongyi Duan and Haoyang Liu and Jian'an Zhang and Fengrui Liu and Yiyi Wang},
journal= {arXiv preprint arXiv:2510.17622},
year = {2025}
}