Autoencoders are an essential concept in unsupervised learning. Currently, the quality of autoencoders is assessed either internally (e.g., by 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 requiring formal guarantees 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 on a real-world dataset from the medical domain.
Autoencoders are widely used for many unsupervised learning tasks such as cluster analysis [
However, a major shortcoming of these approaches is that they cannot provide a formal guarantee in terms of the maximum deviation between input and output of the autoencoder as it is evaluated on test data only (i.e., with a finite number of inputs). This lack of formal quality guarantees for autoencoders leads to a very limited applicability of such unsupervised learning schemes for safety-critical applications. For instance, it is particularly important to consider the maximum deviation when working with data containing clusters. In such situations the autoencoder should not mix up the clusters because otherwise the autoencoder’s results are meaningless. If the maximum deviations for the respective clusters are small enough though, the autoencoder provably keeps the clusters separated.
To address this and other shortcomings of unsupervised learning with autoencoders, we provide
the first methodology to bound an autoencoder’s worst-case error in a safety-critical region.
Inspired by the vast literature on supervised adversarial attacks [
Following a popular approach in the area of software verification, we reduce the problem of
ifnding an unsupervised adversarial example to a satisfiability check of a formula in linear Real
Arithmetic [
In general, an autoencoder tries to reproduce its input; that is, it is trained to compute () = . However, it does so while propagating it through a latent space which typically has less dimensions than the input/output space. This latent space serves as an information bottleneck and therefore introduces errors to the identity function the autoencoder is supposed to learn. However, as most applications of autoencoders rely on a good approximation of the identity function, we are naturally interested in quantifying its error. More precisely, our goal is to give formal guarantees in terms of the maximum deviation from the identity function.
As a first step towards this goal, we define the notion of adversarial examples of autoencoders. Intuitively, such adversarial examples are inputs on which the “distance” between the input and the output of the autoencoder is larger than a (user-defined) threshold > 0.
Definition 1 (-adversarial examples). Let : R → R be an autoencoder, dist : R × R → R+ a distance function, and > 0. An -adversarial example is a point ∈ R such that dist (, ()) > (i.e., a point on which the input and output of deviate more than ).
Note that our definition of -adversarial examples is not restricted to inputs in the training or test sets but allows any input ∈ R. In the context of safety-critical systems, however, it is not enough to identify individual -adversarial examples, but it is necessary to know the worst-case (i.e., maximum) error an autoencoder produces. As we cannot expect to find a global maximum of the unbounded error, we restrict the region for which we want to calculate the worst-case error.
Definition 2 (Worst-case error of autoencoders). Let : R → R be an autoencoder, dist : R × R → R+ a distance function, and ⊆ R an (infinite) safety-critical region of inputs. Then, the worst-case error of in is defined as
wce(, ) = sup {︀ dist (︀ , ())︀ ∈ R+ | ∈ }︀ (i.e., the largest deviation of an input in the region from its output).
Definition 2 serves as our novel quality criterion for autoencoders that reflects how good the identity function is learned in the specific region of interest. It overcomes the limitation of classical quality metrics that are defined on finite test data only. In total, this leads us to the main problem statement.
Problem 1 (QUGA: Quality Guarantees for Autoencoders). Given a region ⊆ R, an autoencoder : R → R and a distance function dist : R × R → R+, compute wce(, ).
In general, computing the worst-case error is a very challenging and computationally intractable problem. Hence in the next section we introduce a restricted, solvable version of it.
In this section we outline a framework for computing -adversarial examples and the worst-case error of autoencoders in a restricted and hence computationally tractable version of Problem 1. The following restrictions are designed in such a way that the solution framework remains applicable to a wide range of autoencoders used in practice: 1. We assume the the neurons of the autoencoder have linear or ReLU (Rectified Linear
Unit) activation functions. 2. We assume the distance function to be the 1 or ∞-norm. 3. We assume the safety-critical region to be a finite union of convex compact polytopes. 4. We approximate the worst-case error up to a user-defined accuracy.
Given these assumptions we can encode the problem of finding an -adversarial example in a
given region as an instance of the SMT problem [
Theorem 1. Let be an autoencoder, a region, dist a distance function, > 0, and ae as defined above. Then, the following two properties hold: 1. If contains an -adversarial example, then ae is satisfiable.
2. If ae is satisfiable, then any solution of ae is an -adversarial example in . In order to approximate the worst-case error in a region we can thereafter exploit this property by performing a binary search over the values of and keeping track of lower and upper bounds on the worst-case error.
We demonstrate our QUGA framework on the ECG5000 dataset (Figure 1), by evaluating the unsupervised training based on two time series clusters. The goal of a traditional evaluation would be to show that all training objects are clearly separated in the latent space. In contrast, we care about all possible (infinitely many) objects in two safety-critical areas (green and red) that need to be distinguishable in the latent space. In Figure 2 we see the resulting corridors (green and red) into which points from the corresponding critical regions can be mapped. As the two corridors do not overlap on all timesteps (e.g., in time 137) the autoencoder keeps the two safety-critical classes apart allowing for the use of the latent space representations for follow up tasks such as, e.g., classification.
QUGA overcomes major shortcomings of unsupervised learning with autoencoders. We provide the first methodology to bound the error of an autoencoder in a safety-critical region. With our solution framework based on SMT solvers we propose to search for adversarial examples and the worst-case error in the infinite search space of a safety-critical region. Our QUGA approach formulates the autoencoder, the safety-critical region, and the error of the loss function with a logical conjunction of linear constraints. This allows us to prove separation of the input data in the latent space for further downstream applications.