Automatic Tensor-level Execution of Abstract Interpreters for Neural Networks

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: https://github.com/uiuc-focal-lab/constraintflow.git