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

TL;DR

Fast BATLLNN is a highly efficient verification tool that rapidly checks box-like output constraints of Two-Level Lattice Neural Networks, significantly outperforming existing methods in speed and scalability.

Contribution

The paper introduces Fast BATLLNN, a novel verification algorithm that leverages TLL architecture properties to achieve faster performance than existing polynomial-time algorithms.

Findings

Fast BATLLNN verifies TLL NNs more than 400x faster than competitors.

It effectively handles box-like output constraints within convex polytopes.

The method demonstrates superior scalability and performance in synthetic benchmarks.

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.