Effective Random Test Generation for Deep Learning Compilers

Our generation follows a topological order of operations in computation graph. We say node a precedes node b, or b succeeds a, if there exists a path, where a appears earlier than b in the path. Each time we generate a node, this node does not precedes any existing node. For example, as the graph shown in Figure 2, followed by a topological order, i.e., operation $Add$ then operation $Concat$, our approach instantiates operations one by one. For each operations, we first instantiate its type and the number of incoming edges.

In this way, our approach resolves the constraints by partitioning them into several subparts. Each subpart corresponds to a single operation and its related edges. Furthermore, because the output of operations could be determined only by the input and attributes, we rewrite the constraints by substituting the output as a function of the input and attributes. In our example, the constraints are as follows, where $Spec_{op}(V)$ is defined as a set of constraints on $V$ that specifies from the specification of an operation with type $op$, $f_{op}$ denotes the mathematical function of the operation with type $op$:

After resolving constraints with instantiating operations in the graph by their topological order, our goal turns to instantiate each single operation by solving constraints related to the operation (in our example, they are $Spec_{Add}(p,q)$ and $Spec_{Concat}(axis,r,s)$), as shown in the next part.

The instantiation of a new operation includes assigning the value to its operation type, attributes, input (incoming edge(s)) (output of the operation is excluded as explained before). As a concrete example, assume we already instantiate a computation graph with a single Add operation (with $p$ and $q$ as its input as shown in the red part of Figure 3), now we extend the instantiation by appending a new operation into the computation graph.

Assume we instantiate type of the new operation as Concat, and the number of incoming edges of the new operation as two in our example. We now set symbol variables for the input and attributes of the operation. In the example of Concat, we denote variable $ax$ for the attribute $axis$, and variable $x$ and $y$ as two incoming edges (note, $ax$, $x$ and $y$ are just symbol variables, which will be assigned with values later, such as assigning $r$ to $x$).

For each incoming edge, i.e., each tensor in the input, instead of instantiating the whole tensor, we focus on instantiating the structure of the tensor first due to that the semantic specifications are only related to tensor structure. For an edge $x$, we setup a set of symbol variables to substitute $x$ in the constraints, including $d_{x}$ (denoting the dimension size of $x$, i.e., $dim_{x}$) and $x_{i}$ (denoting each dimension’s length of $x$, i.e., $x[i]$). In this way, the constraints could be further specified as follows:

To sample a random solution to the above constraints, our approach instantiates variables in a well-designed order: first are variables related to $x$; then attribute $axis$; finally variables related to $y$. In our example, the order is as follows: $d_{x}$; $x_{i}$; $axis$; $d_{y}$; $y_{i}$. Note, in the order, variables related to the same tensor are ordered together in a group, also, within the group, instantiation of the dimension size (e.g., $d_{x}$) is ahead of the length of each dimension (e.g., $x_{i}$). The detailed illustration and explanation of the order are shown in Section III-C.

Followed by this order, we are able to simplify the constraints to quantifier-free and unknown-function-free by the elimination technique mentioned in Section II-C; also controllably choose ways for instantiating unassigned tensors, i.e., instantiating the tensor as an instantiated one such as $r$ for $x$; or as the output from a tensor placeholder such as $s$ for $y$. Details are shown in Section III.

With above simplification, the constraints belong to propagation logic which is decidable. Thus, we are able to conduct constraint solving by constraint propagation [apt2003principles] to find solutions. In addition, the constraint propagation will not produce an empty domain (which causes the instantiation inconsistent) due to the good property as explained in next part, resulting in the overall process being backtrack-free.

Based on the graph theory and the theory of constraint satisfaction problem (CSP) [apt2003principles], our instantiation-based solver holds some good properties due to characteristics of constraints on deep learning models. We draw main conclusions here, formal definitions and detailed explanations are shown in Section III.

The first property is called graph-level directional consistency. For any semantically valid computation graph with a topological order on operations as $(O_{1},O_{2},...,O_{i})$, we can consistently extend the instantiation to include $O_{i+1}$ (with topological order as $(O_{1},O_{2},...,O_{i},O_{i+1})$) as long as ensuring satisfaction of constraints related to $O_{i+1}$.

The second property is called operation-level global consistency. For constraints related to each single operation, after determining operation’s type and the number of tensors in the input, by taking attributes as a variable and each tensor in the input of the operation as a variable, this CSP, which consists of constraints on the operation level, is globally consistent: any consistent instantiation of a subset of the variables can be extended to a consistent instantiation of all of the variables without backtracking [dechter1992local].

A tensor $t$ is a generalized vector, like N-D array (N is a positive integer). The structure of tensor $t$ is defined as a set $Str_{t}$, denoting the structural information of the tensor. $Str_{t}$ includes (1) a numerical value $dim_{t}$ that denotes $t$’s dimension size and (2) a variable-length array that denotes each dimension’s length of tensor $t$ (i.e., $t[i]$ as the i-st dimension’s length).

An operation $n$ is defined as a function with tensor(s) as input and output. It has some parameters: we denote $Op_{n}$ as its type ($Op_{n}\in AllOps$, $AllOps$ is a unverisal set which contains all types of operations), $Attr_{n}$ as a set which contains attributes of the operation (such as strides in Conv operation, and axis in SoftMax operation). Also, $Input_{n}=\{in_{1},in_{2},...\}$ is a set which contains one or more tensors as the input of $n$, and $Output_{n}=\{out_{1},out_{2},...\}$ as the output of $n$. Specially, $Attr_{n}$ contains a special attribute $Indegree_{n}$ as the number of tensors in $Input_{n}$, i.e., $Indegree_{n}=|Input_{n}|$.

A tensor placeholder $tp$ is simply a variable, denoting a tensor to which the specific data will be assigned later. A tensor placeholder that denotes tensor $p$ could be created with merely $Str_{p}$, without need of specific data.

A computation graph $G$ is defined as an ordered triple $(V_{G},E_{G},\psi_{G})$, where the set $V_{G}$ denotes the nodes, the set $E_{G}$ denotes the edges. An element in $V_{G}$ is either an operation or a tensor placeholder. An element in $E_{G}$ is a tensor. $\psi_{G}$ is called an incidence function which maps an edge into a pair of nodes (i.e., a mapping from $E(G)\rightarrow V(G)\times V(G)$), denoting the structure of the graph.

A constraint $C$ is a limitation placed on the values of variables. Consider a finite sequence of variables $S:=\{x_{1},x_{2},...,x_{k}\}$, with respective domains $D(x_{1})$, . . ., $D(x_{k})$ associated with them. So each variable $x_{i}$ ranges over the domain $D(x_{i})$. By a constraint $C$ on $S$ we mean a subset of $D(x_{1})\times D(x_{2})...\times D(x_{k})$.

An instantiation $Q$ is defined as a set of tuples, written as $\left\langle x_{1}=v_{1},x_{2}=v_{2},...,x_{m}=v_{m}\right\rangle$, denoting that a specific value $v_{i}$ that has been assigned to the variable $x_{i}$.

A constraint satisfaction problem (CSP) $P:(V,D,C)$, where $V$ is a set of variables, $D$ is the set of domains of values for each variable, $C$ is a set of constraints. A solution to a problem $P$ is an instantiation $Q$, containing the assignment of all variables in $V$, which satisfies all of constraints in $SC$. Namely, an instantiation $Q$ is a solution of $P:(V,D,C)$ only if it satisfies with all of constraints in $C$.

Let $X=(X_{1},X_{2},...,X_{n})$ be a set of variables in a CSP, and let $X^{{}^{\prime}}=(X^{{}^{\prime}}_{1},X^{{}^{\prime}}_{2},...,X^{{}^{\prime}}_{m})$ be a subset of variables from $X$. A partial instantiation of variables $\left\langle X^{{}^{\prime}}_{1}=x_{1},X^{{}^{\prime}}_{2}=x_{2},...,X^{{}^{\prime}}_{m}=x_{m}\right\rangle$ is locally consistent if it satisfies all the constraints in $X^{{}^{\prime}}$. A globally consistent CSP is one in which any locally consistent partial instantiation of variables can be extended to a consistent full instantiation. Globally consistent CSPs have the property that a solution can be found without backtracking  [dechter1992local].

Taking each operation as a variable (a set variable $V_{x}$, containing $Op_{x}$, $Input_{x}$, $Attr_{x}$), constraints of the computation graph could be rewritten as a binary CSP, consisting of two kinds of constraints: first are unary constraints on each variable, and second are binary constraints between two variables (i.e., the output of an operation equals to the input of another operation). According to the definition, an instantiation $Q$ is locally consistent on $V_{x}$ if $Q$ satisfies all the constraints in $V_{x}$.

Because our instantiation follows the topological order of a computation graph, with only instantiating edges which are from previous nodes (variables that are ahead of $V_{x}$ in the order) to current variable $V_{x}$, the instantiation on $V_{x}$ will not affect local consistency of previous variables (based on the property of topological order). Thus, for each $x$, as long as we are able to instantiate $Q$ with its local consistency on $V_{x}$ every time, then we could include $V_{x}$ in the end of topological order, and instantiation is still consistent. Also, because we instantiate edges with the direction followed by the topological order, the overall graph is loop-free. Thus, following with the topological order, ensuring local consistency on each operation leads to bracktrack-free instantiation on the graph level.

For an operation $x$, our order contains several groups, arranged as follows: $G_{1},G_{2},G_{3},...,G_{|Indegree_{x}|+2}$. First group consists of one variable: $G_{1}=\{Indegree_{x}\}$. Second group is the variables related to the first tensor in the input (first incoming edge of this operation), i.e., $G_{2}=Str_{in_{1}}(in_{1}\in Input_{x}$). Third group is the attributes of operations (except for $Indegree_{x}$), i.e., $G_{3}=Attr_{x}\setminus\{Indegree_{x}\}$. For the rest, each group is variables related to the next tensor in the input (next incoming edge of this operation), i.e., $G_{i+2}=Str_{in_{i}}(in_{i}\in Input_{x})$. In the groups related to each tensor (assume the tensor is $t$), the variable that denotes the dimension size of the tensor is ahead of the variables that denote the length of each dimension of the tensor, i.e., $d_{t}$ (denotes $dim_{t}$) is ahead of $t_{i}$ (denotes $t[i]$).

Specifically, there are two forms which cause the existing constraint solving or sampling approaches [DBLP:conf/tacas/MouraB08, DBLP:conf/iccad/DutraBS18] hard to handle. First is the quantifier in the constraints, which hold the forms as $\forall i\in f(x),C(i)$, where $f$ is a function returns a set, $x$ is a variable, $C(i)$ is a constraint whose form is dependent on the value of $i$. Second is the unknown function. Constraints may contain terms such as $t_{f(x)}$, where $f(x)$ is a function that returns an integer number and $t_{f(x)}$ is the variable that denotes the $t[f(x)]$ (f(x)-st dimension’s length of tensor $t$).

Our instantiation could eliminate the quantifiers and unknown functions in constraints with the following reason. As quantifiers in form of $\forall i\in f(x),C(i)$, for all of variable $v$ whose existence in $C(i)$ depends on the domain of $f(x)$, we call that $v$ depend on $x$. As constraints with unknown function such as $t_{f(x)}$, we call $t_{i}$ depends on $x$. For constraints on deep learning models, the above dependencies among constraints are loop-free. Our instantiation order is actually a topological order satisfying those dependencies, i.e., ensuring that for any dependencies that $x$ depends on $y$, $y$ is ahead of $x$ in the order. Thus, followed by the instantiation order, with satisfying the precondition of eliminating quantifiers and unknown functions by instantiation, we could simplify the constraints to a decidable propositional logic for constraint propagation.

The reason why we put the variables related to the same tensor in a group, i.e., instantiate the tensor(s) one by one, is due to the consideration of instantiating $\psi_{G}$.

We design an on-demand policy for instantiating the tensor, with consideration of the instantiation for $\psi_{G}$ in the meanwhile. For each tensor $t$ in the input of $x$ ($t\in Input_{x}$), our on-demand policy instantiates $Str_{t}$ with two choices: (1) reusing the structure $Str_{s}$ of an existing tensor $s$ as long as they are consistent with the instantiation, in other words, we set $t$’s structure the same as an instantiated tensor $s$, which is from the output of an instantiated node $ex$, i.e., instantiating $t=s$ with $\psi_{G}(t)=(ex,x)$ (if there are more than one satisfied tensor, we will randomly pick one of them; if no such tensor, we choose the second way); (2) creating a new tensor placeholder as a node $n$, and set its output as $t$, in other words, instantiating a tensor $t$ with $t\in Output_{n}$ as well as $\psi_{G}(t)=(n,x)$.

We select the choice of instantiating tensors according to a Bernoulli distribution, as a common way to produce random boolean decisions. Any other distributions are also allowed. The distribution is controlled by a parameter $picking\ rate$. The higher $picking\ rate$ is, the higher chance that our approach would select the first choice (i.e., reusing an existing tensor). To favor generating more complicated computation graphs, we set $picking\ rate$ relatively high in practice. We will further explain the effect of this parameter in Section IV.

We illustrate that our propagation-based instantiation will not lead to inconsistence due to the property we called operation-level global consistency. For the constraints related to each single operation such as $x$, after determining the type ($OP_{x}$) and the number of tensors in the input ($Indegree_{x}$), we could take attributes as a variable and each tensor in the input of the operation as a variable. With good properties of specification on deep learning operations, this CSP is globally consistent [dechter1992local]. Thus, any order for instantiation, including our delicately-designed instantiation order in our approach, will not lead to inconsistence.

Declarative-style generation constructs deep learning models only based on the syntax grammar, in short as DeclGen. When determining the shape of tensors, it just randomly generates from all choices. After the construction of the input, i.e., a whole computation graph, this approach directly feeds input into the compiler under test, and relies on the compiler’s running to check whether the model is satisfied with its semantic specifications.

Inspired by feedback-directed random test generation [pacheco2007feedback], this approach conducts random generation for operation construction, i.e., randomly constructs a new operation to append it into the model, and checks whether the model satisfies the semantic specifications or not. This generation way can avoid generating invalid models at early stages, leading to the improvement of overall effectiveness, while the generation for a single operation to satisfy its semantic specifications is still ineffective.

Muffin [DBLP:conf/icse/GuLZ022] is a state-of-the-art generation-based testing approach, proposed originally to test deep learning libraries such as Keras [keras], generating models based on two model structure templates (chain structure with skips and cell-based structure) with deep learning library APIs. To satisfy with tensor structural constraints, Muffin hardcodes additional Reshaping layers to reshape the input/output tensors for the connection between layers. Though Muffin is not designed for testing deep learning compilers, we can retrofit it to barely achieve the goal by converting the models constructed by high-level APIs into computation graphs with existing tools [tf2onnx].

TVMFuzz [DBLP:conf/sigsoft/ShenM0TCC21] is a fuzzer which specifically targets testing TVM [DBLP:conf/osdi/ChenMJZYSCWHCGK18]. It randomly generates and mutates Tensor-level IR(TIR) expressions (the intermediary language of TVM) for fuzzing test, mainly towards the type-related bug detection.

NNSmith [NNSmith] is a generation-based approach for testing deep learning compilers, as a parallel research work with ours. NNSmith constructs the computation graphs based on the specifications of deep learning models: it tries possible choices for types, attributes, and input/output of operations by iteratively adding constraints from specifications and leveraging existing constraint solver Z3 [DBLP:conf/tacas/MouraB08] to check the satisfaction; if constraints are not satisfied, it will backtrack and try different choices to pick.

Graph-level metrics are designed for measuring various aspects of a single generated model. Let a test set be the set of models generated by an approach. Given a test set $I$, which contains $n_{I}$ graphs, the graph-level metrics are defined as follows.

Number of Operations (NOO) of a graph $g$ is defined as the total number of operations in $g$. Number of Operation Types (NOT) of a graph $g$ is defined as the number of different types of operations in $g$. Number of Operation Pairs (NOP) of a graph $g$ is defined as the number of different edges in $g$ that connect two operations together. Number of Operation Triples (NTR) of a graph $g$ is defined as the number of different pairs of adjacent edges that connect three operations together in $g$. Number of Shapes and Attributes (NSA) of a graph $g$ is defined as the total number of different shapes of input tensors and attributes (except for its input dgrees) for each operation in graph $g$. These graph-level metrics for test set $I$ are defined as the average of each of them among all the graphs in $I$: $GLM(I)=\frac{\Sigma_{g}{GLM_{g}(g)}}{n_{I}}$, where $GLM\in\{NOO,NOT,NOP,NTR,NSA\}$.

Operation-level metrics are designed for measuring various aspects of operations among the whole test set. An operation corpus is a set of operations with their attributes including the operation name and the possible number of different input degrees. Given an operation corpus $C$ containing $n_{C}$ different operations and a test set $I$, we first calculate the metric on each type of operator $o$ in $I$, denoted as $XXC_{op}(o)$, then we have the operation-level metric of $I$ as the average of the operation-level metric on different operators, i.e., $XXC(I)=\frac{\Sigma_{o}{XXC_{op}(o)}}{n_{C}}$, where $XXC\in\{OTC,IDC,ODC,SEC,DEC,SAC\}$. We simply explain the meanings of these six metrics as below, and detailed definitions of these operation-level metrics are shown in our project website [israproject].

Operation Type Coverage (OTC), Input Degree Coverage (IDC), Output Degree Coverage (ODC) show the diversity of operations types, and the diversity of the input and output degrees of them in the test set $I$ respectively. Single Edge Coverage (SEC) shows the diversity of edges between the operations in $I$. Double Edge Coverage (DEC) shows the diversity of pairs of edges that are adjacent, which is actually the coverage of different triples of operations that are connected in a graph in the test set. Shapes and Attributes Coverage (SAC) indicates the diversity of attributes of the operations (except for input degrees) and their input tensor shapes in the test set.

The result of experiment on coverage measurement is shown in Table I. Firstly, with alignment on the number of generated inputs, we can find that Isra outperforms the baselines greatly with respect to the amount of time, showing the efficiency of our approach.

For operation-level metrics, we find that Isra is able to cover all kinds of operations that we have chosen and all kinds of input degrees of each type of operation. Compared with the two baselines, Isra has higher coverage on all of operation-level metrics, especially for $SEC$, $DEC$, and $SAC$.

We find that the $NOO$ (Number of Operations) of our approach and Randoop-Gen are closer to the average of the lower bound and upper bound of the operation numbers that we set (consistent with our uniform sampling for the number of operations), while DeclGen’s $NOO$ remains at a significantly lower level. The reason is that DeclGen holds less probability to satisfy the semantic specifications, which leads to generating rather simple models and bad performance on the graph-level metrics. Randoop-Gen’s $NOP$ and $NTR$ are comparable with our approach, however, the operation types ($NOT$) of Isra are more diverse, making it outperform Randoop-Gen at coverage of operation pairs ($SEC$) and triples ($DEC$). The results of graph-level metrics indicate that Isra are capable of generating diverse, large and complex models.

As shown in Figure 4, Figure 6, and Figure 6, Isra is able to generate different operations in a relatively uniform distribution, which is consistent with our uniform sampling for picking the type of operation. As a contrast, all of baselines fail to generate a sufficient number of operations with relatively complicated semantic specifications such as Conv and Gemm. It shows that all of baselines have a limitation that the diversity of models generated by them is weak. This is because the constraints of some operations are relatively complicated and less possible to satisfy. Those complex operations are less possible to be chosen in the valid output by the filter of the iterative checking process. Besides, among models generated by Muffin, reshape operation appears most frequently because Muffin forces the insertions of reshape operation before many operations to ensure semantic specifications.

To evaluate the effect of $picking\ rate$ parameter, we also compare the results of Isra with the setting of different $picking\ rates$. The settings are the same as the experiment on coverage measurement, except that we set the operation number in the graphs as a fixed number 100. The result is shown in Table II. If the $picking\ rate$ is relatively high, the operations are more likely to be matched with existing tensors, leading to $NOP$, $NTR$ going high. In the meanwhile, the shape of newly created tensors is more likely to be equal to the shape of previous tensors, leading to the result that $NSA$ goes down as the $picking\ rate$ increases. We finally choose its value as 0.97, as a trade-off.

Among all of unique bugs detected by  Isra, we categorize them into two types based on the test oracles detecting them: (1) error bug (29 of 33) : the given input triggers an error, crash or unexpected exception during compilation; (2) inconsistency bug (4 of 33): the compiler executes the given input and terminates normally but the compiled model produces different outputs according to differential testing.

After we report found bugs to the corresponding community, compiler developers give responses for most of them, all with positive feedback. Among all of bugs found by Isra, there are 24 previously unknown bugs. Until now, a majority of our detected bugs (27 of 33) have already been fixed by developers, with 16 bugs directly owing to our bug reporting/pull requests, benefiting all the compiler users and their applications. One of TVM core developers replies with the following message for bugs reported by us⁵⁵5https://github.com/apache/tvm/pull/7208#issuecomment-754406762: “These two errors that you generated were excellent real bugs with the importer and were very easy to understand and replicate with your post. If they’re being auto-generated they look excellent!” The feedback from real-world developers is also strong evidence showing that Isra is practical for testing real-world deep learning compilers and able to detect critical bugs in practice.

We list 24 previously unknown bugs (as well as bug reports) detected by Isra in Table IV, including the stage of root causes, the time it takes to have the bug confirmed and fixed, and the GitHub issue ID ⁶⁶6For reference, the URLs of TVM’s and Glow’s bug reports are https://github.com/apache/tvm/issues/#IssueID, and https://github.com/pytorch/glow/issues/#IssueID. The URLs for SophGo’s bug reports are internal and not publicly accessible. for reference. The details of confirmed/fixed bugs are as follows.

TVM-1 is a bug in the compiler backend, caused by a pass named DynamicToStatic which should not be defined at optimization level 3. It will lead the internal error when the deep learning model contains operations such as MatMul, Dropout. After our reporting, developers reordered passes in the backend and lowered DynamicToStatic optimization level to fix it ⁷⁷7https://github.com/apache/tvm/pull/7213.

TVM-2 is a bug in the compiler frontend. The TVM developer has explained the cause of the bug and fixed it⁸⁸8https://github.com/apache/tvm/issues/7202#issuecomment-754372403: “It’s due to a bad assumption made in PRelu conversion about the input layout……Our current PRelu converter assumes that incoming data is in NCHW format and that the slope will have C total elements. Neither of these are actual requirements for ONNX PReLu.”

TVM-3 and TVM-4 are bugs in the compiler frontend. Some of parameters in LpPool and LeakyRelu operation in ONNX standard allow default value but it was not supported in TVM.

TVM-5 is a bug in the compiler backend, which catches an edge case of the compiler’s type checker as explained by a TVM developer⁹⁹9https://github.com/apache/tvm/issues/7262#issuecomment-911968074.

TVM-6 and TVM-7 are bugs in the compiler frontend. The former is due to that one of input tensors in Gemm operation can be optional by the standard but the TVM doesn’t allow that behavior. The latter is due to the fact that “Split operation is not dynamic inputs” as explained by the compiler developer.

TVM-8 is a bug in the compiler backend due to inconsistent specifications between different versions on Squeeze operation, causing erroneous implementation in the compiler.

TVM-9 is a bug in the compiler backend. The erroneous backend implementation causes the inconsistent outputs on a model containing Flatten and ReduceL1 operation. Developers have not confirmed this bug, but it has been fixed in the next released version of the compiler.

Glow-1 is a bug in the compiler backend due to that ReduceSum operation in the input model contains multi axis inputs and attributes.

SophGo-1 is a bug in the compiler frontend. The compiler does not support that the weight tensor of Conv operation is an input tensor. Developers do not fix this bug due to the reason that they suppose users take this parameter as a constant because this parameter usually does not change after deployment.

SophGo-2 is a bug in the compiler backend. If the inputs of Mean operation are the same tensor, then the calculation of mean operation will throw exception due to the naming error.

SophGo-3 is a bug in the compiler backend. ReduceProd operation will register a buffer, but buffer size has not been assigned which leads to the incorrect parameters in calculation and further causes the final result wrong.

SophGo-4 is a bug in the compiler frontend due to erroneous parsing for Pooling operation.

SophGo-5 is a bug in the compiler backend due to incorrect implementation on Split operation.

SophGo-6 is a bug in the compiler backend. The compiler assumes the second input of PRelu holds a specific shape which is not consistent with the specification.

SophGo-7 is a bug in the compiler backend. The compiler backend incorrectly covers the input data for the calculation on Cos operation, causing the wrong results of model’s output.

SophGo-8, SophGo-9, and SophGo-10 are bugs in the compiler frontend due to erroneous parsing for Unsqueeze operation, Split operation and Gemm operation. ONNX standard of some operations has changed after version 13. The compiler only implements old version and is not compatible with latest standard. Developers do not fix SophGo-10 due to the same reason as SophGo-1.

SophGo-11 is a bug in the compiler backend due to incorrect implementation on Resize operation.

Though our test generation approach is sound (i.e., the models generated by our approach ensures the validity), false positives may be introduced by floating point errors [7194603, DBLP:journals/pomacs/XiaoLYPW22]. For differential testing, one of test oracles we used, when it comes to checking output equivalence, false alarms may be produced due to floating point errors/inaccuracies. To reduce false alarms, we use a high error tolerance in comparison of models’ outputs (the relative error is set to 10% as mentioned in Section IV-B), which is similar to a parallel work [NNSmith]. In our evaluation, Isra did not find false positives caused by the floating-point errors.