Backsubstitution as matrix multiplication. The left ma-trix M k in Fig. 2 encodes bounds for ` -th layer neurons with polyhedral expressions defined over the neurons in layer 1 ≤ k < ` . The center matrix F k encodes con-straints for k -th layer neurons defined over the neurons in layer k − 1 . We focus on the computation of the entry ( h 2 ... See more

he affine transformation x ` i = ∑ j a ` − 1 i,j · x ` − 1 j + b i adds the bounds ∑ j a ` − 1 i,j · x ` − 1 i + b i ≤ x ` i ≤ ∑ j a ` − 1 i,j · x ` − 1 i + b i . Thus DeepPoly handles affine layers ex-actly. • x ` i = ReLU ( x ` − 1 i ) adds the bounds α ` i · x ` − 1 i + β ` i ≤ x ` i ≤ γ ` i · x ` − 1 i + δ ` i where the constants α ` i , β ` i ... See more