# ExtendAIST: Exploring the Space of AI-in-the-Loop System Testing
## 3 Extendaist
### Design
Since some activation functions are non-linear, the formal verification is transformed into a Mixed Integer Program (MIP) with the value of binary variables \(\delta_{a}\), where \(\delta_{a}=\{0,1\}\). The binary variable \(\delta_{a}\) indicates the phase of activation function ReLU. If \(\delta_{a}=0\), the activation function is blocked and the output of related neuron will be 0; otherwise, the activation function is passed and the output of related neuron will be equal to its input value. #### 4.4.4 Symbolic Interval Analysis (EP_SIA)

Symbolic interval analysis [35] utilizes the symbolic interval arithmetic to obtain the accurate range of DNN's output according to the ranges of input variables. * ReluVal. Given an input range \(X\), subintervals of \(X\) and security property \(P\). DNN is secure if no value in range \(X\) and its subintervals violate property \(P\), that is, any value from range \(X\) satisfies \(P\); otherwise DNN is insecure if there exists one adversarial example in \(X\) violating \(P\), that is, there exists at least one subinterval containing an adversarial example to make property \(P\) unsatisfied. #### 4.4.5 Reachability Analysis (EP_RA)

To eliminate the limitation of network scale for formal verification, safety verification can also be transformed into reachability analysis [36]. * DeepGo. If all values in the output range, the lower and upper bounds \([l,u]\), correspond to an input in input subspace \(X^{{}^{\prime}}\subseteq[0,1]^{n}\), then the network \(f\) is reachable and the reachability diameter is \(D(X^{{}^{\prime}};f)=u(X^{{}^{\prime}})-l(X^{{}^{\prime}})\). The network \(f\) is said to be safe for the input \(x\in X^{{}^{\prime}}\) if all inputs in \(X^{{}^{\prime}}\) have the same label to \(x\), as shown in Equation (16). \[Cov_{ANC}=\frac{n_{activated}}{N}\]6 (16)

#### 4.4.6 Abstract Interpretation (EP_AI)

Since the scale of input data and neural network are tremendous, it is infeasible to verify whether individual input satisfies the safety properties precisely. To overcome this obstacle, an abstract domain is used to approximate the concrete domain and verify the safety properties against abstract domain directly, referred to as the abstract interpretation theory [96; 97]. The following existing techniques in point EP_AI show the application of abstract interpretation on AIS testing. * AI\({}^{2}\). AI\({}^{2}\)[37] proposes to employ the zonotope domain to represent the abstract elements in neural network and output the abstract elements in each layer. Finally, the safety of network is determined by verifying whether the label of abstract output in the output layer is consistent with that of the concrete output. * Symbolic propagation. To improve the precision and efficiency of DNN safety verification, [PERSON] et al. [38] proposed a symbolic propagation method based on the abstract interpretation by representing the values of neurons symbolically and propagating them from the input layer to output layer forwardly. A more precise range of output layer is computed by the interval abstract domain based on the symbolic representation of output layer. ### Evaluation Dataset (EP_ED)

#### 4.5.1 Description

Since the machine learning based AI-in-the-loop system is a data-driven system, it is essential to design datasets adaptive for diverse application areas to conduct the training, testing, and evaluation procedures. There mainly exist five kinds of datasets for different purposes: image classification, self driving, natural language processing, speech recognition, and Android malware detection. Therefore, we take the common dataset as the super extension point EP_CD and the five kinds of datasets as the sub-extension points named EP_IC, EP_SD, EP_NALP, EP_SR, and EP_AMD. Based on the above, researchers can design more datasets for diverse scenarios and different learning, testing, and evaluation tasks. The existing techniques and common datasets in each sub-extension point are displayed as follows.