P topk(Aj,: (1 X)),21 ho,j=Aj,: X P topk(Aj,: X) + P topk(A

We categorize existing implementations2 into 2 kinds: (1) for verification only (typically implemented on CPUs, including DeepZ[35], and DeepPoly[37])3 (2) for training certified defense (typically using more efficient, yet weaker or approximated bounds: convex outer4 adversarial polytope[45], DiffAI[28], IBP[9] andCROWN-IBP[50]). Ourcontributionisnot8 to improve tightness of LiRPA bounds, but the first framework that generalizes to general computational graphs in9 anautomatic manner. In CROWN[50], the quadratic bound is only applied to 2-layer networks and is hard to extend to14 multiplelayers,aswhenpropagatingaquadratic boundtothe3rdlayeritbecomes quadratic (x4)duetocorrelations15 between twoquadratic terms ("order explosion").