Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918164207501312 |
|---|---|
| author | Duan, Hongyi Liu, Haoyang Zhang, Jian'an Liu, Fengrui Wang, Yiyi |
| author_facet | Duan, Hongyi Liu, Haoyang Zhang, Jian'an Liu, Fengrui Wang, Yiyi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_17622 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks Duan, Hongyi Liu, Haoyang Zhang, Jian'an Liu, Fengrui Wang, Yiyi Logic in Computer Science Machine Learning 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. |
| title | Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks |
| topic | Logic in Computer Science Machine Learning |
| url | https://arxiv.org/abs/2510.17622 |