{"ID":2852826,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.17622","arxiv_id":"2510.17622","title":"Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks","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.","short_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...","url_abs":"https://arxiv.org/abs/2510.17622","url_pdf":"https://arxiv.org/pdf/2510.17622v1","authors":"[\"Hongyi Duan\",\"Haoyang Liu\",\"Jian'an Zhang\",\"Fengrui Liu\",\"Yiyi Wang\"]","published":"2025-10-20T15:05:14Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.LG\"]","methods":"[]","has_code":false}