Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks

DOI10.1145/3501710.3519533MaRDI QIDQ6120722zbMATH OpenOpenAlexFDO

Authors James Ferlez, Haitham Khedr, Yasser Shoukry

Publication date 21 February 2024

Published in 25th ACM International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2111.09293

zbMATH Keywords

neural network verificationneural networksrectified linear units

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Abstract: In this paper, we present the tool Fast Box Analysis of Two-Level Lattice Neural Networks (Fast BATLLNN) as a fast verifier of box-like output constraints for Two-Level Lattice (TLL) Neural Networks (NNs). In particular, Fast BATLLNN can verify whether the output of a given TLL NN always lies within a specified hyper-rectangle whenever its input constrained to a specified convex polytope (not necessarily a hyper-rectangle). Fast BATLLNN uses the unique semantics of the TLL architecture and the decoupled nature of box-like output constraints to dramatically improve verification performance relative to known polynomial-time verification algorithms for TLLs with generic polytopic output constraints. In this paper, we evaluate the performance and scalability of Fast BATLLNN, both in its own right and compared to state-of-the-art NN verifiers applied to TLL NNs. Fast BATLLNN compares very favorably to even the fastest NN verifiers, completing our synthetic TLL test bench more than 400x faster than its nearest competitor.

Cites work

• A Partial Order on the Regions of R n Dissected by Hyperplanes
• An introduction to hyperplane arrangements
• AReN
• Branch and bound for piecewise linear neural network verification
• Deep neural networks and mixed integer linear optimization
• Formal verification of piece-wise linear feed-forward neural networks
• Improved geometric path enumeration for verifying ReLU neural networks
• Output Reachable Set Estimation for Switched Linear Systems and Its Application in Safety Verification
• Region configurations for realizability of lattice piecewise-linear models.
• Reluplex: an efficient SMT solver for verifying deep neural networks
• Reverse search for enumeration
• Verification of piecewise deep neural networks: a star set approach with zonotope pre-filter
• Verisig

Cited in

(1)

• Extracting forward invariant sets from neural network-based control barrier functions

This page was built for publication: Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6120722)