为ReLU网络设计高效精确的语义分析系统，支持实时验证与推理。
Just-In-Time Piecewise-Linear Semantics for ReLU-type Networks
- 基于共享超平面的分段线性转换器，动态生成判定区域。
- 实现任意时间正确性，完全细化单元下精确计算，复杂度可控。
- 适合需要形式化验证的高安全性模型，如自动驾驶、医疗系统。
我们提出一种针对ReLU型网络的即时编译分段线性语义系统，将模型编译为具有共享判定条件的带约束分段线性转换器。系统仅在当前单元上为仿射操作数添加超平面，维护全局上下包络，并采用预算化的分支定界法。该方法实现了任意时间正确性、完全细化单元下的精确性、单调进展、判定条件线性复杂度（避免全局$inom{k}{2}$），支持主导剪枝与有限细化下的可判定性。共享载体支持区域提取、决策复形、雅可比计算、精确/认证的Lipschitz常数、基于LP/SOCP的鲁棒性分析及最大因果影响。最小原型可在访问子域成本内返回证书或反例。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。