Monotone Operator Equilibrium Models (monDEQs) represent a class of models combining the powerful deep equilibrium paradigm with convergence guarantees. Further, their inherent robustness to adversarial perturbations makes investigating their certifiability a promising research direction. Unfortunately, existing approaches are either imprecise or severely limited in scalability. In this work, we propose the first scalable and precise monDEQ verifier, based on two key ideas: (i) a novel convex relaxation enabling efficient inclusion checks, and (ii) non-trivial mathematical insights characterizing the fixpoint operations at the heart of monDEQs on sets rather than concrete inputs. An extensive evaluation of our verifier on the challenging $\ell_\infty$ perturbations demonstrates that it exceeds state-of-the-art performance in terms of speed (two orders of magnitude) and scalability (an order of magnitude) while yielding 25% higher certified accuracies on the same networks.
翻译:单体操作器平衡模型(monDEQs)代表了将强大的深平衡范式与趋同保证相结合的一组模型。此外,对对抗性扰动的内在坚固性使得调查其可验证性成为充满希望的研究方向。 不幸的是,现有方法要么不精确,要么在可缩放性方面严重受限。在这项工作中,我们根据两个关键理念提出了第一个可缩放和精确的蒙DEQ验证器:(一) 新的松动性放松,允许高效率的包容检查,以及(二) 非三进制的数学洞察力,将定点操作定点定在集而不是具体投入中。我们对具有挑战性的 $\ell ⁇ infty perburbation 进行的广泛评估表明,从速度(两个数量级)和可缩放性(一个数量级)来看,它超过了最先进的速度(两个数量级)和可缩放性(一个数量级)的性能,同时在同一网络上产生25%的经认证的优度。