arXiv cs.CL· Avaljot Singh, Yasmin Chandini Sarita, Aditya Mishra, Gagandeep Singh, Charith Mendis·· 12 小时前AI 评分31
Neuton：自动将神经元级抽象解释器规范编译为张量级可执行程序
Automatic Tensor-level Execution of Abstract Interpreters for Neural Networks
AI 导读
Neuton 框架可将神经元级 DNN 认证器规范自动翻译为张量级可执行程序，无需手写张量编程。它通过基于栈的 IR 与形状分析推断广播、维度扩展和归约等隐式张量操作，并用领域重写规则优化常见操作序列，还提出面向认证器稀疏性的 gBCSR 稀疏张量格式。
正文 · 原文
Abstract:Developing new abstract interpretation-based DNN certifiers is difficult because their mathematical design is expressed at the neuron level, while implementations must operate at the tensor level. Existing libraries such as auto_LiRPA, IVAN, and ERAN support fixed sets of certifiers; extending them requires expertise in formal methods and tensor programming. Domain-specific languages such as ConstraintFlow let researchers specify certifiers at the neuron level, but cannot run them on real DNNs.
We present Neuton, a framework that automatically translates neuron-level certifier specifications into tensor-level executables, enabling new DNN certifiers without manual tensor programming. Neuton makes three contributions. First, a stack-based intermediate representation (IR) and shape analysis infer implicit tensor operations, including broadcasts, dimension expansions, and reductions, required for correct execution. Second, domain-specific rewrite rules optimize common tensor operation sequences into more efficient equivalents. Third, gBCSR is a sparse tensor format using variable-sized, layer-aligned blocks over a non-zero default value, tailored to DNN certifier sparsity.
We prove that translation preserves neuron-level semantics. We evaluate Neuton on 8 certifiers and 32 DNN benchmarks. Neuton compiles four existing certifiers and produces the first executable implementations of four others: two previously specified but never run, and two new designs. These expose precision-runtime trade-offs unavailable in existing libraries. For example, SkipPoly matches DeepPoly's precision on all 32 DNNs while running as fast or faster on half. Neuton's runtime on existing certifiers is competitive with hand-optimized libraries. Code: this https URL
| Subjects: | Computation and Language (cs.CL) |
| Cite as: | arXiv:2507.20055 [cs.CL] |
| (or arXiv:2507.20055v2 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2507.20055 arXiv-issued DOI via DataCite |
Submission history
From: Avaljot Singh [view email]
[v1]
Sat, 26 Jul 2025 20:38:29 UTC (4,660 KB)
[v2]
Fri, 16 Oct 2026 17:43:47 UTC (852 KB)
来源：arXiv cs.CL · arxiv.org