On Training and Verifying Robust Autoencoders

Autoencoders have become ubiquitous in machine learning thanks to their broad range of applications. Therefore we must be able to formally state and verify properties about their behaviour such as denoising or robustness. However, so far formal verification for autoencoders has almost not been addressed. Thus we introduce the first formal problem specification for robustness of autoencoders.Moreover we give a framework capable of proving the robustness property for autoencoders based on SMT solvers. Yet, because these SMT solvers are notoriously slow, the approach does not scale up to larger autoencoders. Therefore we describe a regularization scheme aimed both to increase the autoencoder’s robustness and to decrease the time required for verification.In our experiments we highlight the use of the new problem specification and compare our proposed regularization scheme to other, already existing ones. Using our approach, verification time becomes up to 21 times faster.