Quality Guarantees for Autoencoders via Unsupervised Adversarial Attacks

Abstract

Autoencoders are an essential concept in unsupervised learning. Currently, the quality of autoencoders is assessed either internally (e.g.. based on mean square error) or externally (e.g.. by classification performance). Yet, there is no possibility to prove that autoencoders generalize beyond the finite training data, and hence, they are not reliable for safety-critical applications that require formal guarantees also for unseen data. To address this issue, we propose the first framework to bound the worst-case error of an autoencoder within a safety-critical region of an infinite value domain, as well as the definition of unsupervised adversarial examples that cause such worst-case errors. Technically, our framework reduces the infinite search space for a uniform error bound to checking satisfiability of logical formulas in Linear Real Arithmetic. This allows us to leverage highly-optimized SMT solvers, a strategy that is very successful in the context of deductive software verification. We demonstrate our ability to find unsupervised adversarial examples as well as formal quality guarantees both on synthetic and real-world data.