# Formal Verification of Long Short-Term Memory based Audio Classifiers: A
Star based Approach

Neelanjana Pal Institute for Software Integrated Systems
Vanderbilt University
Nashville, USA<EMAIL_ADDRESS>Institute for Software Integrated
Systems
Vanderbilt University
Nashville, USA Taylor T Johnson Institute for Software Integrated Systems
Vanderbilt University
Nashville, USA<EMAIL_ADDRESS>
###### Abstract

Formally verifying audio classification systems is essential to ensure
accurate signal classification across real-world applications like
surveillance, automotive voice commands, and multimedia content management,
preventing potential errors with serious consequences. Drawing from recent
research, this study advances the utilization of star-set-based formal
verification, extended through reachability analysis, tailored explicitly for
Long Short-Term Memory architectures and their Convolutional variations within
the audio classification domain. By conceptualizing the classification process
as a sequence of set operations, the star set-based reachability approach
streamlines the exploration of potential operational states attainable by the
system. The paper serves as an encompassing case study, validating and
verifying sequence audio classification analytics within real-world contexts.
It accentuates the necessity for robustness verification to ensure precise and
dependable predictions, particularly in light of the impact of noise on the
accuracy of output classifications.

##  1 Introduction

Deep Neural Networks (DNNs) have demonstrated remarkable capabilities in
addressing intricate tasks like image classification, object detection, speech
recognition, natural language processing, and document analysis, at times even
surpassing human performance [24, 22, 25]. This success has ignited a surge in
exploring the viability of DNNs across diverse real-world domains, including
biometric authentication, mobile facial recognition for security, and malware
detection. However, given the sensitive nature of the data in these critical
applications, incorporating safety, security, and robust verification into
their design has become paramount.

However, studies have revealed that even slight modifications in input data
can effectively mislead cutting-edge, well-trained networks, causing
inaccuracies in their predictions [33, 41, 13]. The arena of network
verification has primarily concentrated on image inputs, particularly
emphasizing the assurance of safety and robustness in various classification
neural networks [44, 3, 8, 20, 32, 45]. Previous investigations have
scrutinized a range of network architectures, encompassing feed-forward neural
networks (FFNNs [43]), convolutional neural networks (CNNs [45]), semantic
segmentation networks (SSNs [44]), and a few using Recurrent Neural Networks
(RNNs [42]) employing diverse set-based reachability tools such as Neural
Network Verification (NNV [46, 27]) and JuliaReach [7], among others.

Models utilizing NNs for audio classification have found application in
diverse tasks, ranging from Music Genre Classification [11, 9, 12] and
Environmental Sound Classification [14, 5, 10] to Audio Generation [34, 37].
Therefore, formal verification of audio classification systems holds paramount
importance in ensuring their reliability and safety, particularly in safety-
critical applications such as autonomous vehicles [47, 36], medical diagnosis
[16, 31], and industrial monitoring [48].

This study introduces an extension, building upon the foundations laid by two
recent studies [42, 35] in the domain of formal verification. The objective is
to leverage set-based reachability techniques to verify audio classification
models based on the Long Short Term Memory (LSTM) and CNN-LSTM architectures.
Drawing inspiration from [42], which highlights the star-based verification of
basic vanilla RNNs, and from [35], which demonstrates the formal verification
of convolutional neural networks operating on time series data, work shown in
this paper amalgamates both concepts. Specifically, it employs two LSTM models
and one CNN-LSTM model for these classifications, following the ones depicted
in [28, 29, 30].

##### Contributions.

  1. 1.

This paper presents a thorough case study on the formal verification of audio
classification models using the LSTM and CNN-LSTM architectures with two
different datasets. Our focus is to rigorously assess the robustness
verification of these models within a formal verification framework, analyzing
their behavior and performance against input noises. We develop our work as an
extension of the NNV tool111The code for this paper is available at
https://github.com/verivital/nnv/tree/master/code/nnv/examples/Submission/FMAS2023
to formally analyze and explore CNN-LSTM architecture verification for audio
data using sound and deterministic reachability methods.

  2. 2.

Building on insights from existing research [42, 35], this paper extends
formal verification to more complex RNN architectures. This involves
addressing the challenges of the complex structure of the LSTM layers,
comprehensively evaluating their behavior, and ensuring robustness compliance
through formal verification. This study pushes formal verification’s
boundaries, embracing design complexities for heightened assurance and
reliability.

  3. 3.

In this assessment, we conduct a thorough and comprehensive evaluation of
three distinct network architectures across diverse audio classification
scenarios.

  4. 4.

Finally, we develop insights on evaluating the reachability analysis on those
networks and possible future direction.

##### Outline.

The paper is organized as follows: Section 2 mentions the works already done
in the literature and the inspiration works for this paper; Section 3 provides
the necessary context for the background, and defines the verification
properties for this work; Section 4 explains the reachability calculations for
the LSTM layer; and Section 5 describes the methodology, including dataset,
network models, and input perturbations. Section 6 presents the experimental
results, evaluation metrics, and their implications. Finally, Section 7
summarizes the main findings and suggests future research directions.

##  2 Related Work

In recent times, an upsurge of methodologies and tools have arisen to confront
the verification complexities inherent in intricate systems like Deep Neural
Networks (DNNs), as evident from the literature [15, 18, 26, 45].
Correspondingly, tools have emerged to tackle the robustness challenges of
Convolutional Neural Networks (CNNs) [3, 20, 21, 38, 39, 40]. Earlier
undertakings in the verification of Recurrent Neural Networks (RNNs) are
showcased through projects like RnnVerify [19] and RNSVerify [2]. RNSVerify
employs an unrolling technique to translate RNNs into extensive Feedforward
Neural Networks (FFNNs), simplifying verification through Mixed-Integer Linear
Program (MILP) approaches [2]. However, this unrolling method faces
scalability constraints, particularly with bounded n-step RNNs, as the
verification complexity scales dramatically. Conversely, RnnVerify [19]
employs invariant inference for RNN verification, bypassing unrolling. Their
strategy involves crafting an FFNN with matching dimensions to over-
approximate the RNN, followed by verifying RNN properties over this
approximation using SMT-based methodologies. Our work gets inspiration from
[42], where authors introduce a pioneering approach founded on star
reachability for RNN verification, aiming to amplify the dependability and
safety of RNNs and show the results based on some vanilla RNN models.

##### Distinction from the previous works [42, 35].

While both papers share the common goal of validating the robustness of RNNs,
the preceding study can be perceived as an initial step in that research
trajectory. In contrast, this paper represents a more comprehensive evolution
of the concepts initially introduced.

  1. 1.

The work in [42] focused on the Vanilla RNN, while this paper delves into
models of significantly greater intricacy, such as the LSTM and CNN-LSTM
architectures. Vanilla RNNs and LSTMs are both types of recurrent neural
networks. However, Vanilla RNNs are simpler in terms of architecture and have
fewer parameters, whereas LSTMs are more complex due to their gated units and
larger parameters.

    1. (a)

Vanilla RNNs handle input sequences in a sequential manner, updating a hidden
state at each step. In contrast, LSTMs also maintain a hidden state, but their
structure is more complex, featuring multiple gates (input, forget, and output
gates) that regulate the information flow.

    2. (b)

Vanilla RNNs face challenges capturing long-term dependencies within sequences
due to the vanishing gradient problem. This problem limits their ability to
learn connections between distant time steps. LSTMs, on the other hand, were
specifically designed to tackle the vanishing gradient problem and excel at
capturing long-term dependencies, rendering them better suited for tasks
involving intricate temporal relationships.

    3. (c)

Vanilla RNNs possess a constrained memory capacity, often rapidly discarding
information from earlier time steps. This limitation can hinder their
performance in tasks with extended sequences. In contrast, LSTMs feature an
improved memory mechanism that allows them to retain or discard information
from prior time steps selectively. This capability equips them to handle
longer sequences and capture complex patterns effectively.

  2. 2.

The study conducted in [35] focused on examining time-series regression models
in the Prognostics and Health Management domain. Drawing inspiration from this
work, our study extends the investigation to encompass the time domain’s
influence, specifically concerning sequential audio noise and Japanese vowel
audio samples. This basic experiment provides a foundation for understanding
the robustness and reliability of audio classification systems. They offer
insights that can be directly applied to real-world scenarios, making them
valuable for a broad audience in the field of audio classification.

    1. (a)

Utilizing real-world datasets, this experiment can yield practical insights
into audio classification system performance, benefiting fields such as speech
recognition, audio surveillance, and multimedia content management by offering
real-world applicability.

    2. (b)

This experiment can provide valuable insights into the robustness of audio
classifiers when exposed to different noise levels and perturbations, offering
crucial implications for applications where audio data is frequently affected
by a noise like voice commands in automobiles or audio analysis in noisy
settings.

    3. (c)

While this work concentrates on two particular datasets, the verification
methodologies showcased can be extended to diverse audio classification
endeavors, allowing readers engaged in various audio classification challenges
to customize and apply the methodologies to their specific contexts.

    4. (d)

The metrics used in this paper can be potential for real-world applications to
evaluate and enhance the reliability and efficiency of audio classification
systems.

##  3 Preliminaries

This section introduces some basic definitions and descriptions necessary to
understand the progression of this paper and the necessary evaluations on
audio classification models.

###  3.1 Neural Network Verification Tool and Star Sets

The Neural Network Verification (NNV) tool constitutes a framework designed to
verify the safety and robustness of neural networks [46, 27]. This tool
meticulously scrutinizes neural network behavior across diverse input
conditions, warranting secure and accurate functionality across all scenarios.
NNV employs reachability algorithms, including the exact and over-approximate
star set methodologies [45, 43], to compute reachable sets for each neural
network layer. These sets encapsulate all feasible network states for a given
input, thereby facilitating the verification of specific safety properties.

NNV holds particular significance in safety-critical domains like autonomous
vehicles and medical devices, where the trustworthiness and reliability of
neural networks are paramount. NNV bolsters public confidence in these
applications by ensuring consistent performance across all conditions. In this
paper, we extend the capabilities of the NNV tool to implement our work,
utilizing the star-based reachability analysis to ascertain the reachable sets
of neural networks at their outputs.

Figure 1: Star for a sequence input data with four Feature Values (rows) with
four time-steps (columns)

###### Definition 3.1

_A generalized star set_ (or simply star) $\Theta$ is a tuple $\langle
c,V,P\rangle$ where $c\in\mathbb{R}^{n}$ is the center,
$V=\\{v_{1},v_{2},\cdots,v_{m}\\}$ is a set of m vectors in $\mathbb{R}^{n}$
called basis vectors, and $P:\mathbb{R}^{m}\to\\{\top,\bot\\}$ is a predicate.
The basis vectors are arranged to form the star’s $n\times m$ basis matrix.
The set of states represented by the star is given as:

$\llbracket\Theta\rrbracket=\\{x~{}|~{}x=c+\Sigma_{i=1}^{m}(\alpha_{i}v_{i})~{}\text{and}~{}P(\alpha_{1},\cdots,\alpha_{m})=\top\\}.$
(1)

In this work, we restrict the predicates to be a conjunction of linear
constraints, $P(\alpha)\triangleq C\alpha\leq d$ where, for $p$ linear
constraints, $C\in\mathbb{R}^{p\times m}$, $\alpha$ is the vector of
$m$-variables, i.e., $\alpha=[\alpha_{1},\cdots,\alpha_{m}]^{T}$, and
$d\in\mathbb{R}^{p\times 1}$.

###  3.2 Network Architecture Specifics

####  3.2.1 Long Short Term Memory (LSTM) Layer

An LSTM layer, a subtype of the Recurrent Neural Network (RNN) layer, excels
at capturing long-term dependencies in time series and sequential data [17].
It comprises two critical elements: the hidden state ($h_{t}$, also called the
output state) and the cell state ($c_{t}$). At each time step ‘t,’ the hidden
state captures the layer’s output for that instance, while the cell state
accumulates insights from preceding time steps.

Figure 2: The flow of data at time step t in an LSTM layer

$\begin{split}c_{t}&=f_{t}\odot c_{t-1}+i_{t}\odot g_{t}\\\
h_{t}&=o_{t}\odot\sigma_{c}(c_{t})\end{split}$ (2)

During each time step, the layer refines the cell state by incorporating or
omitting information. This process is steered by distinct gates that control
these adjustments, as shown in Fig. 2.

$\begin{split}i_{t}=\sigma_{g}(W_{i}x_{t}+R_{i}h_{t-1}+b_{i})\\\
f_{t}=\sigma_{g}(W_{f}x_{t}+R_{f}h_{t-1}+b_{f})\\\
g_{t}=\sigma_{c}(W_{g}x_{t}+R_{g}h_{t-1}+b_{g})\\\
o_{t}=\sigma_{g}(W_{o}x_{t}+R_{o}h_{t-1}+b_{o})\end{split}$ (3)

In these equations, $\odot$ represents the Hadamard product (element-wise
multiplication), $\sigma_{c}$ denotes the activation function applied element-
wise to the cell state $c_{t}$ and to the cell state gate $g_{t}$;
$\sigma_{g}$ denotes the activation function applied element-wise to the
hidden state gates. Here, $W$, $R$, and $b$ are, respectively, hidden state
weights, recurrent weights, and biases for each of the gates.

####  3.2.2 Convolutional Neural Network + Long Short Term Memory (CNN+LSTM)
Architecture

When processing sequences, a CNN uses sliding convolutional filters over the
input, extracting information from spatial and temporal dimensions.
Conversely, an LSTM network progresses through time steps, capturing lasting
connections between them. The synergy of CNN and LSTM layers, as seen in
CNN+LSTM architectures [50], harnesses the strengths of both convolutional and
LSTM units for insightful data analysis.

The convolutional component forms the foundation for acquiring local feature
modules that grasp both local and hierarchical correlations. This fusion
enables the identification of intricate data relationships. Additionally, the
inclusion of an LSTM layer enhances the network’s capacity to capture
prolonged dependencies by leveraging information from these localized
features.

Figure 3: Layers of a demo CNN+LSTM Architecture model

###  3.3 Reachability Analysis Computation

This section describes how the reachability of an NN layer and the NN as a
whole is computed for this study.

In this context, we adopt an alternative technique for defining a Star set.
This method involves utilizing the input’s upper and lower bounds with noise,
subsequently aligning them around the original input. We establish a
comprehensive array of constraints by incorporating these bounds for each
input parameter alongside predicates. These constraints are then presented to
the optimizer for a solution, ultimately yielding the initial set of states.

###### Definition 3.2

A layer $L$ of a NN is a function $h:~{}u\in\mathbb{R}^{j}\rightarrow
v\in{\mathbb{R}}^{p},$ defined as follows

$v=h(u)$ (4)

where the function $h$ is determined by parameters $\theta$, typically defined
as a tuple $\theta=\langle\sigma,W,b\rangle$ for fully-connected and
convolutional layers, where $W$ is the weight matrix, $b$ is the bias vector,
and activation function is $\sigma$. For CNN layers, $\theta$ may include
parameters like the filter size, padding, or dilation factor.

###### Definition 3.3

Let $h:~{}u\in\mathbb{R}^{j}\rightarrow v\in{\mathbb{R}}^{p}$, be an NN layer
as described in Eq. 4. The reachable set ${\mathcal{R}_{h}}$, with input,
$\mathcal{I}\in\mathbb{R}^{n}$ is defined as

$\mathcal{R}_{h}\triangleq\\{v~{}|~{}v=h(u),~{}u\in\mathcal{I}\\}$ (5)

Reachability analysis (or, shortly, reach) of an NN $f$ on Star input set
$\mathcal{I}$ is similar to the reachable set calculations for CNN[45] or
FFNN[43].

$\begin{split}Reach(f,\mathcal{I}):~{}&\mathcal{I}\rightarrow\mathcal{R}_{ts}\end{split}$
(6)

We call $\mathcal{R}_{ts}(I)$ the _output reachable set_ of the NN
corresponding to the input set $\mathcal{I}$.

For an NN, the output reachable set can be calculated as a step-by-step
process of constructing the reachable sets for each network layer.

$\begin{split}\mathcal{R}_{L_{1}}&\triangleq\\{v_{1}~{}|~{}v_{1}=h_{1}(x),~{}x\in\mathcal{I}\\},\\\
\mathcal{R}_{L_{2}}&\triangleq\\{v_{2}~{}|~{}v_{2}=h_{2}(v_{1}),~{}v_{1}\in\mathcal{R}_{L_{1}}\\},\\\
&\vdots\\\
\mathcal{R}_{ts}=\mathcal{R}_{L_{k}}&\triangleq\\{v_{k}~{}|~{}v_{k}=h_{k}(v_{k-1}),~{}v_{k-1}\in\mathcal{R}_{L_{k-1}}\\},\\\
\end{split}$ (7)

where $h_{k}$ is the function represented by the $k^{th}$ layer $L_{k}$. The
reachable set $\mathcal{R}_{L_{k}}$ contains all outputs of the neural network
corresponding to all input vectors $x$ in the input set $\mathcal{I}$.

###  3.4 Adversarial Perturbation

An audio classification system may face real-world scenarios involving
elements like background noise, interference, or distortions. While
potentially perceptible, these factors remain within the scope of challenges
that practical systems are designed to address. However, this paper
exclusively used l-infinity perturbations, focusing on assessing how audio
classification models respond to variations within specific constraints.

Considering an input sequence characterized by $t_{s}$ time instances and
$n_{f}$ features, various perturbation types ($l_{\infty}$ norm) [35] arise
based on their distribution across the sequence. These adversarial
perturbation categories can be delineated as follows:

  1. 1.

Single Feature Single-instance (SFSI): This entails perturbing the value of a
specific feature solely at a particular instance ($t$), deviating by a certain
percentage from the actual value:

$s^{perturb}=g_{\epsilon,s^{perturb}}(s)=s+\epsilon_{t}\cdot s_{t}^{perturb}$
(8)

  2. 2.

Single Feature All-instances (SFAI): In this scenario, a particular feature
across all time instances undergoes perturbation by a certain percentage
relative to its original values:

$s^{perturb}=g_{\epsilon,s^{perturb}}(s)=s+\sum_{i=1}^{n}\epsilon_{i}\cdot
s_{i}^{perturb}$ (9)

  3. 3.

Multifeature Single-instance (MFSI): All feature values experience
perturbation, but solely at a specific instance (t), following the principle
outlined in Eq. 8 for each feature.

  4. 4.

Multifeature All-instance (MFAI): Perturbation affects all feature values
across all instances, aligning with the approach delineated in Eq. 9 for every
feature.

###  3.5 Robustness Verification Properties

##### Robustness.

Robustness pertains to the capacity of a system or model to sustain its
performance and functionality amid diverse challenging conditions,
uncertainties, or perturbations. This highly desirable trait ensures the
system’s dependability, resilience, and adaptability in the presence of
altering or unfavorable circumstances. To formally articulate the concept of
robustness for quantifying the desired classification task, the following
formulation can be employed:

$||x^{\prime}-x||{\infty}<\delta\implies f(x^{\prime})==f(x)$ (10)

Here, $x$ signifies the original input from the input space $R^{n_{f}\times
t_{s}}$, $x^{\prime}$ represents the perturbed input, $f(x^{\prime})$ and
$f(x)$ correspond to the classifiers’ outputs for $x^{\prime}$ and $x$,
respectively. $\delta$ stands for the maximum magnitude of the introduced
perturbation ($\delta\in\textbf{R}>0$). By disregarding the softmax and
classification layers within the models and focusing on the output of the
layer immediately preceding the softmax, the formulation for robustness
simplifies as follows:

$||x^{\prime}-x||_{\infty}<\delta\implies\text{maxID}(g(x^{\prime}))==\text{maxID}(g(x))$
(11)

In this context, the function $g$ symbolizes the operation performed by the
neural network classifier model until the softmax layer, and maxID denotes the
function responsible for identifying the class with the highest value in the
output.

##### Verification Properties.

Verification properties can be broadly classified into two distinct
categories: local and global. A local property must be valid for specific
predefined inputs, while a global property [49] is established across the
entire input space $R^{n_{f}\times t_{s}}$ of the network model, holding true
for all inputs without exceptions.

##### Local Robustness.

Given a sequence classifier $f$ and an input sequence $S$, the network is
called locally robust to any perturbation $\mathcal{A}$ if and only if:
reachable bounds of the desired class will be max compared to the bounds of
the other classes, even in the presence of any perturbation.

Robustness Value (RV) of a sequence $S$ is a binary variable, which indicates
the local robustness of the system. RV is $1$ when the reachable output range
of the desired class is greater than the reachable bounds of other classes,
making it locally robust; otherwise, RV is 0.

$RV=1\iff{LB_{desired}}\geq{UB_{other}}$ else, RV = 0

where ${LB_{desired}}$ and ${UB_{other}}$ are the lower reachable bound of the
desired class and ${UB_{other}}$ are the upper bounds of all other classes.

##### Percentage Robustness (PR).

We apply the concept of Percentage Robustness (PR), previously utilized in
image-based classification or segmentation neural networks [44], to the
context of sequence audio inputs. The PR for a sequence classifier,
corresponding to any adversarial perturbation, is defined as:

$PR=\frac{N_{robust}}{N_{total}}\times 100$ (12)

where $N_{robust}$ represents the total number of robust sequences, and
$N_{total}$ is the overall count of sequences in the test dataset. Percentage
robustness can be used as an indicator of global robustness [49] with respect
to various types of perturbations.

##  4 Reachability of a Long Short Term Memory Layer

To compute the reachability of an LSTM layer in relation to a star input set
$S_{t}$, a series of stepwise reachability computations are necessary to
ultimately determine the reachable set of the LSTM layer’s output, as depicted
in Eq. 2-3. Ensuring accurate results relies on verifying the validity of
specific conditions, which are crucial for this process to be sound and
accurate:

  1. 1.

Affine Mapping Validity. The transformation of a star set through an affine
mapping using a given weight and bias must result in another valid star set
[43].

  2. 2.

Star Set Summation. Combining two star sets through Minkowski summation should
lead to the formation of yet another valid star set [6].

  3. 3.

Activation Function Application. Upon applying the activation function to a
star set, the output should also result in a star set(s). The outcome could
manifest as a single star set or a composition of multiple star sets,
contingent on factors such as the activation functions employed and the
specific reachability technique utilized [43, 46, 44, 45].

  4. 4.

Hadamard Product Validity. The Hadamard Product of two star sets should yield
another valid star set.

While the validity of the first three conditions for star sets has been
established in prior research, this current study aims to extend that
validation to include the fourth condition as well.

######  Definition 4.1 (Hadamard product of two star sets)

Given two star-sets $\Theta_{1}=\langle c_{1},V_{1},P_{1}\rangle$ and
$\Theta_{2}=\langle c_{2},V_{2},P_{2}\rangle$, the Hadamard product of them
$\bar{\Theta}=\Theta_{1}\odot\Theta_{2}=\\{y~{}|~{}y=x_{1}\odot
x_{2},~{}x_{1}\in\Theta_{1},~{}x_{2}\in\Theta_{2}\\}$ is another star with the
following characteristics.

$\bar{\Theta}=\langle\bar{c},\bar{V},\bar{P}\rangle,~{}\bar{c}=c_{1}\odot
c_{2},~{}\bar{V}=\begin{bmatrix}V_{1}&0\\\
0&V_{2}\end{bmatrix},~{}\bar{P}\equiv\begin{bmatrix}P_{1}&0\\\
0&P_{2}\end{bmatrix}$

Therefore we can conclude that for a given input set $S_{t}$ and an LSTM
layer, the output is also a star set.

##  5 Experimental Setup

###  5.1 Hardware Used:

The actual experimental results shown in this paper are conducted in a
Windows-10 computer with the 64-bit operating system, Intel(R) Core(TM)
i7-8850H processor, and 16 GB RAM.

###  5.2 Dataset Description

For evaluation, we consider two different audio datasets for noise
classification and Japanese vowel classification.

#####  Audio Noise Data:

To curate this dataset, we generated a collection of 1000 white noise signals,
1000 brown noise signals, and 1000 pink noise signals using MATLAB. Each
signal corresponds to a 0.5-second duration and adheres to a 44.1 kHz sample
rate. From this pool of 1000 signals, a training set is fashioned, comprising
800 white noise signals, 800 brown noise signals, and 800 pink noise signals.
Given the multidimensionality inherent in audio data, often containing
redundant information, a dimensionality reduction strategy is employed. We
begin by extracting features and subsequently training the model using only
two extracted features. These features are generated from the centroid and
slope of the mel spectrum over time.

#####  Japanese Vowel [4, 23]:

This dataset is collected from [4] from the University of Irvine Machine
Learning Repository. Two Japanese vowels were sequentially pronounced by nine
male speakers. A 12-degree linear prediction analysis was subjected to each
instance of utterances. Each speaker’s utterance constitutes a time series
ranging from 7 to 29 points in length, with each point featuring 12
coefficients. For 9 classes (i.e., vowels), the dataset has a total of 640
time series. Among these, 270 time series were designated for training
purposes, while the remaining 370 were allocated for testing.

###  5.3 Network Description

#####  Audio Noise Data:

The network architecture used for training the audio noise dataset, partially
adopted from [28], is an LSTM network. The network has two input features
which correspond to one noise type at the output. Following 11, the network
for this dataset can be represented as:

$\displaystyle\begin{split}f:~{}x\in\mathbb{R}^{2\times l_{s}}\rightarrow
y\in{\mathbb{R}^{3}}\\\ \hat{noiseClass}=maxID(g(x))\end{split}$ (13)

#####  Japanese Vowel:

Here we have trained two different classifiers for the Japanese Vowel dataset.
The LSTM architecture is partially adopted from [29] and the CNN+LSTM is
partially adopted from [30]. Both the networks have twelve input features
which correspond to one vowel at the output. Therefore, the networks for this
dataset can be represented as:

$\displaystyle\begin{split}f:~{}x\in\mathbb{R}^{12\times l_{s}}\rightarrow
y\in{\mathbb{R}^{9}}\\\ \hat{vowelClass}=maxID(g(x))\end{split}$ (14)

Here $l_{s}$ is the audio sequence length and the function $maxID$ provides
the class with the maximum value.

Table 1: Performances of different networks used in this paper $Networks$ | $Accuracy(\%)$
---|---
$audio\\_noise\\_lstm$ | 100
$japanese\\_vowel\\_lstm$ | 93.51
$japanese\\_vowel\\_cnnlstm$ | 96.49

##  6 Evaluation

###  6.1 Robustness Verification of Audio Noise Classifier

To conduct robustness verification on the audio noise dataset, we encompass
all four categories of perturbations, following [35]. First, we curate 100
sequences each of white, brown, and pink noise as test datasets. Then, we
generate adversarial sequences centered around the original ones by applying
$l_{\infty}$ norms. This involves utilizing 5 distinct percentage values for
perturbation ($\epsilon$), specifically 50$\%$, 60$\%$, 70$\%$, 80$\%$, and
90$\%$ of the mean ($\mu$) value. These newly created adversarial inputs are
subjected to assessment through the exact-star reachability analysis [Sec. 4]
to determine their robustness. Notably, in the case of Single Feature Single-
instance Noise (SFSI) and Single Feature All-instances Noise (SFAI), we opt
for random selection of feature 1 for input perturbation.

Table 2: Global Robustness: percentage robustness (PR) and total verification runtime (sumRT in seconds) for 100 test audio noise sequences $noise$ | $PR_{SFSI}$ | $PR_{SFAI}$ | $PR_{MFSI}$ | $PR_{MFAI}$ | $sumRT_{SFSI}$ | $sumRT_{SFAI}$ | $sumRT_{MFSI}$ | $sumRT_{MFAI}$
---|---|---|---|---|---|---|---|---
50 | 98 | 80.33 | 98 | 80.33 | 0.3071 | 0.2626 | 0.3018 | 0.2625
60 | 96 | 71.67 | 96 | 71.67 | 0.3034 | 0.2571 | 0.3018 | 0.2578
70 | 94 | 25.67 | 94 | 25.67 | 0.3039 | 0.2637 | 0.3070 | 0.2663
80 | 85.33 | 12.33 | 85.33 | 12.33 | 0.3073 | 0.2559 | 0.3111 | 0.2556
90 | 63.33 | 8.33 | 63.33 | 8.33 | 0.3060 | 0.2504 | 0.3093 | 0.2537
Figure 4: Percentage Robustness and Runtime plots w.r.t increasing
perturbations

##### Observations and Analysis.

Table 2 and Fig. 4 present the network’s overall performance, i.e., the
percentage robustness measures, PR [Sec. 3.5], and total verification runtime
(sumRT) in seconds, with respect to each adversarial perturbation. The
observations derived from both the table and the figure provide the following
insights:

  1. 1.

Trend of Percentage Robustness ($PR$). As the adversary level increases from
50 to 90, we observe a consistent decrease in PR values for all perturbation
scenarios (SFSI, SFAI, MFSI, MFAI), which aligns with the concept of the
robustness verification property. This decrease in PR signifies a reduction in
the system’s ability to maintain its classification accuracy in the presence
of higher adversary levels.

  2. 2.

Comparative Analysis of Perturbation Scenarios. Within each noise level,
comparing PR values across different perturbation scenarios (SFSI, SFAI, MFSI,
MFAI), it’s evident that PR values for SFSI and MFSI are generally higher than
those for SFAI and MFAI. This finding indicates that perturbing features at a
single instance or all features at a single instance generally leads to better
robustness against varying noise levels.

  3. 3.

Similar PR Values for Different Perturbation Scenarios. Another notable
observation is the similarity in robustness matrices between SFSI and MFSI
scenarios, accompanied by closely comparable computation times for their
respective verification processes. This parallelism is also evident for SFAI
and MFAI perturbations as well. This pattern could be ascribed to the
dataset’s limited feature set of only two dimensions, where the foremost
feature likely holds paramount importance in influencing the class
determination in the presence of noise. Consequently, when single-instance
perturbations target the first feature, perturbing both features results in an
effect akin to perturbing the first feature alone. This interpretation is
applicable to both MFAI and SFAI scenarios as well.

###  6.2 Robustness Verification of Japanese Vowel Classifiers

To verify the robustness of both the LSTM and the CNN+LSTM models in the
context of the Japanese vowel classifier, we extend the evaluation to
encompass all four perturbation categories, mirroring the approach undertaken
for the audio noise classifier. During this procedure, we focus on the
complete set of correctly classified test sequences. Subsequently, we create
adversarial inputs centered around the original sequences by applying
$l_{\infty}$ norms to evaluate their robustness. This perturbation process
involves applying 5 distinct percentage values ($\epsilon$) for perturbation:
specifically, 50$\%$, 60$\%$, 70$\%$, 80$\%$, and 90$\%$ of the mean ($\mu$)
value. The resulting set of adversarial inputs is then assessed using the
exact-star reachability analysis for both the classifiers to ascertain their
robustness. Like the earlier scenario, for SFSI and SFAI, feature 1 is chosen
for perturbation.

Table 3: Global Robustness: percentage robustness (PR) and total verification runtime (sumRT in seconds) for all test Japanese Vowel audio sequences $noise$ | $PR_{SFSI}$ | $PR_{SFAI}$ | $PR_{MFSI}$ | $PR_{MFAI}$ | $sumRT_{SFSI}$ | $sumRT_{SFAI}$ | $sumRT_{MFSI}$ | $sumRT_{MFAI}$
---|---|---|---|---|---|---|---|---
50 | 100 | 68.21 | 100 | 74.86 | 1.1502 | 1.0398 | 1.0392 | 1.0442
60 | 100 | 60.40 | 100 | 50.29 | 0.9989 | 0.9992 | 0.9970 | 0.9966
70 | 100 | 50.29 | 100 | 27.17 | 0.9981 | 0.9968 | 0.9965 | 0.9952
80 | 100 | 43.93 | 100 | 13.01 | 0.9920 | 0.9930 | 0.9978 | 0.9882
90 | 100 | 39.02 | 100 | 8.38 | 1.0044 | 1.0083 | 1.004 | 0.9985
Figure 5: Percentage Robustness and Runtime plots w.r.t increasing
perturbations, for LSTM architecture

##### Observations and Analysis: LSTM Model

Table 3 and Fig. 5 present the LSTM network’s overall performance, i.e., the
percentage robustness measures, PR [Sec. 3.5], and total verification runtime
(sumRT), with respect to each adversarial perturbation. The notable findings
are outlined as follows

  1. 1.

Trend of Percentage Robustness ($PR$). Similar to the audio noise classifier,
the trends in $PR$ values here also suggest that as noise levels increase, the
percentage robustness tends to decrease across all scenarios. This aligns with
the intuitive expectation that higher adversary levels lead to increased
challenges in maintaining robustness.

The $PR_{SFSI}$ and $PR_{MFSI}$ values remain consistently at 100$\%$ across
all noise levels, indicating that perturbing either a single feature or all
features at a specific instance does not significantly affect the robustness
of the audio sequences. On the other hand, $PR_{SFAI}$ and $PR_{MFAI}$ show
distinct trends. As adversary levels increase, $PR_{SFAI}$ gradually
decreases, suggesting that perturbing all instances but only a single feature
starts impacting the robustness. Similarly, $PR_{MFAI}$ also experiences a
decline with increasing noise levels, reflecting that perturbing all instances
and features has an impact on the sequences’ robustness.

  2. 2.

Comparative Analysis of Perturbation Scenarios. The comparison between single-
instance perturbation scenarios ($SFSI$ and $SFAI$) and multifeature
perturbation scenarios ($MFSI$ and $MFAI$) reveals a pattern. The former
scenarios (single-instance) generally maintain higher robustness compared to
the latter (multifeature) scenarios. This suggests that perturbing all
features has a larger impact on robustness than perturbing just a single
feature.

The interrelation between $PR_{SFSI}$ and $PR_{MFSI}$ is also notable. Both
scenarios exhibit identical trends, regardless of the noise level. Similarly,
$PR_{SFAI}$ and $PR_{MFAI}$ also demonstrate similar behaviors, with both
scenarios showing a decline in robustness as noise increases.

##### Observations and Analysis: CNN+LSTM Model

Table 4 and Fig. 6 present the CNN+LSTM network’s overall performance.

Table 4: Global Robustness: percentage robustness (PR) and total verification runtime (sumRT in seconds) for all correctly-classified test Japanese Vowel audio sequences $noise$ | $PR_{SFSI}$ | $PR_{SFAI}$ | $PR_{MFSI}$ | $PR_{MFAI}$ | $sumRT_{SFSI}$ | $sumRT_{SFAI}$ | $sumRT_{MFSI}$ | $sumRT_{MFAI}$
---|---|---|---|---|---|---|---|---
50 | 96.82 | 49.13 | 97.39 | 65.89 | 5.5019 | 4.2007 | 4.2197 | 4.1148
60 | 96.82 | 40.75 | 97.39 | 43.64 | 4.5148 | 3.9238 | 3.9123 | 3.9200
70 | 96.82 | 34.68 | 97.10 | 18.78 | 4.6223 | 4.0966 | 4.0778 | 4.0626
80 | 96.82 | 30.63 | 97.10 | 3.17 | 4.5658 | 4.0998 | 4.0550 | 4.0714
90 | 96.82 | 26.58 | 97.10 | 0 | 4.5773 | 4.0785 | 4.0715 | 4.0605
Figure 6: Percentage Robustness and Runtime plots w.r.t increasing
perturbations, for LSTM architecture

Key insights gleaned from both the table and the plot include:

  1. 1.

Trend of Percentage Robustness ($PR$). Across all perturbation levels, the
$PR_{SFSI}$ remain consistently at around 96$\%$ and the $PR_{MFSI}$ at around
97$\%$, indicating that the perturbations applied in these scenarios do not
significantly affect the robustness of the audio sequences. For SFAI and MFAI
perturbations, PR also decreases with rising noise levels, although the
decline is more pronounced. PR values for SFSI and MFSI perturbations are
significantly higher compared to SFAI and MFAI perturbations at all noise
levels, indicating that sequences with perturbations at a single instance are
more robust to noise.

  2. 2.

Trend of Verification Runtimes ($sumRT$). Verification runtimes tend to rise
with elevated noise levels across all perturbation scenarios. However, in the
case of the Japanese Vowel dataset, an initial decrease is observed in the
runtime trend, followed by an increase at perturbation level 70$\%$ and then
again decreases at 80$\%$, followed by another increase at 90$\%$. It’s also
worth noting that contrary to the expected trend, $sumRT_{SFSI}$ exhibits a
higher runtime value in comparison to $sumRT_{SFAI}$ and $sumRT_{MFAI}$.

Overall, the above tables demonstrate how different perturbation scenarios and
adversary levels impact the percentage robustness of the audio noise and
Japanese Vowel audio classifiers. The trends and interrelations provide
insights into the varying effects of perturbations on different scenarios and
noise levels, helping to understand the robustness behavior of the neural
network models under different conditions.

##  7 Conclusion and Future Directions

This study delves into formal method-based reachability analysis for various
LSTM-based neural networks (NNs) using exact and approximate Star methods,
specifically in the context of audio sequence classification – a critical
aspect for safety-critical applications. The investigation encompasses four
distinct adversarial perturbation types, as introduced in the existing
literature. The evaluation occurs across two audio sequence datasets: audio
noise sequences and Japanese vowel audio sequences. The unified reachability
analysis accommodates shifting features within time sequences while
scrutinizing the output against the desired audio class. Robustness properties
are verified for both datasets. Although real-world datasets are employed,
further research is essential to strengthen the connection between practical
issues and performance metrics. The evaluation can also be conducted with
multiple repetitions to ensure that the reported results are not dependent on
specific instances or random fluctuations, thus enhancing the overall validity
and reliability of the findings. Exploring real-world scenarios encompassing a
wider array of perturbation types and magnitudes will also be fascinating,
potentially yielding diverse effects on system behavior. The study paves the
way for exploring the impact of perturbations on the output and expanding
reachability analysis to three-dimensional sequence data like videos. An
intriguing direction for exploration can involve analyzing the peculiar
runtime patterns observed in the plots for the Japanese Vowel audio dataset.
Potential future applications can also encompass medical video analysis.
Notably, this work concentrates on offline data analysis, omitting
considerations for real-time stream processing and memory limitations, which
offers intriguing prospects for future investigation.

##### Acknowledgements.

The material presented in this paper is based upon work supported by the
National Science Foundation (NSF) through grant numbers 1910017, 2028001,
2220426, and 2220401, and the Defense Advanced Research Projects Agency
(DARPA) under contract number FA8750-18-C-0089 and FA8750-23-C-0518, and the
Air Force Office of Scientific Research (AFOSR) under contract number
FA9550-22-1-0019 and FA9550-23-1-0135. Any opinions, findings, conclusions, or
recommendations expressed in this paper are those of the authors and do not
necessarily reflect the views of AFOSR, DARPA, or NSF.

## References

  * [1]
  * [2] Michael E Akintunde, Andreea Kevorchian, Alessio Lomuscio & Edoardo Pirovano (2019): _Verification of RNN-Based Neural Agent-Environment Systems_.  In: Proceedings of the AAAI Conference on Artificial Intelligence, 33, pp. 6006–6013, 10.1609/aaai.v33i01.33016006.
  * [3] Greg Anderson, Shankara Pailoor, Isil Dillig & Swarat Chaudhuri (2019): _Optimization and abstraction: a synergistic approach for analyzing neural network robustness_.  In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731–744, 10.1145/3314221.3314614.
  * [4] Arthur Asuncion & David Newman (2007): _UCI machine learning repository_.
  * [5] Yusuf Aytar, Carl Vondrick & Antonio Torralba (2016): _Soundnet: Learning sound representations from unlabeled video_.  Advances in Neural Information Processing Systems 29: December 5-10, 2016, Barcelona, Spain.
  * [6] Stanley Bak & Parasara Sridhar Duggirala (2017): _Simulation-equivalent reachability of large linear systems with inputs_.  In: International Conference on Computer Aided Verification, Springer, pp. 401–420, 10.1007/978-3-319-63387-9_20.
  * [7] Sergiy Bogomolov, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin & Christian Schilling (2019): _JuliaReach: a toolbox for set-based reachability_.  In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 39–44, 10.1145/3302504.3311804.
  * [8] Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio & Ruth Misener (2020): _Efficient verification of relu-based neural networks via dependency analysis_.  In: Proceedings of the AAAI Conference on Artificial Intelligence, 34, pp. 3291–3299, 10.1609/aaai.v34i04.5729.
  * [9] Keunwoo Choi, György Fazekas, Mark Sandler & Kyunghyun Cho (2017): _Convolutional recurrent neural networks for music classification_.  In: 2017 IEEE International conference on acoustics, speech and signal processing (ICASSP), IEEE, pp. 2392–2396, 10.1109/ICASSP.2017.7952585.
  * [10] Fatih Demir, Daban Abdulsalam Abdullah & Abdulkadir Sengur (2020): _A new deep CNN model for environmental sound classification_.  IEEE Access 8, pp. 66529–66537, 10.1109/ACCESS.2020.2984903.
  * [11] Mingwen Dong (2018): _Convolutional neural network achieves human-level accuracy in music genre classification_.  arXiv preprint arXiv:1802.09697.
  * [12] Peace Busola Falola, Emmanuel Oluwadunsin Alabi, Folashade Titilope Ogunajo & Oluwakemi Dunsin Fasae (2022): _Music genre classification using machine and deep learning techniques: a review_.  ResearchJet J Anal Invent 3(03), pp. 35–50.
  * [13] Ian J Goodfellow, Jonathon Shlens & Christian Szegedy (2015): _Explaining and harnessing adversarial examples_.  3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings.
  * [14] Andrey Guzhov, Federico Raue, Jörn Hees & Andreas Dengel (2021): _Esresnet: Environmental sound classification based on visual domain models_.  In: 2020 25th International Conference on Pattern Recognition (ICPR), IEEE, pp. 4933–4940, 10.1109/ICPR48806.2021.9413035.
  * [15] Navid Hashemi, Bardh Hoxha, Tomoya Yamaguchi, Danil Prokhorov, Georgios Fainekos & Jyotirmoy Deshmukh (2023): _A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning-enabled Control Systems_.  In: Proceedings of the ACM/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), pp. 98–109, 10.1145/3576841.3585928.
  * [16] Ezz El-Din Hemdan, Walid El-Shafai & Amged Sayed (2023): _CR19: A framework for preliminary detection of COVID-19 in cough audio signals using machine learning algorithms for automated medical diagnosis applications_.  Journal of Ambient Intelligence and Humanized Computing 14(9), pp. 11715–11727, 10.1007/s12652-022-03732-0.
  * [17] Sepp Hochreiter & Jürgen Schmidhuber (1997): _Long short-term memory_.  Neural computation 9(8), pp. 1735–1780, 10.1162/neco.1997.9.8.1735.
  * [18] Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu & Xinping Yi (2020): _A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability_.  Computer Science Review 37, p. 100270, 10.1016/j.cosrev.2020.100270.
  * [19] Yuval Jacoby, Clark Barrett & Guy Katz (2020): _Verifying recurrent neural networks using invariant inference_.  In: Automated Technology for Verification and Analysis: 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19–23, 2020, Proceedings 18, Springer, pp. 57–74, 10.1007/978-3-030-59152-6_3.
  * [20] Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić et al. (2019): _The marabou framework for verification and analysis of deep neural networks_.  In: International Conference on Computer Aided Verification, Springer, pp. 443–452, 10.1007/978-3-030-25540-4_26.
  * [21] Panagiotis Kouvaros & Alessio Lomuscio (2018): _Formal verification of cnn-based perception systems_.  arXiv preprint arXiv:1811.11373.
  * [22] Alex Krizhevsky, Ilya Sutskever & Geoffrey E Hinton (2012): _Imagenet classification with deep convolutional neural networks_.  Advances in Neural Information Processing Systems 25: December 3-6, 2012, Lake Tahoe, Nevada, United States, pp. 1106–1114.
  * [23] Mineichi Kudo, Jun Toyama & Masaru Shimbo (1999): _Multidimensional curve classification using passing-through regions_.  Pattern Recognition Letters 20(11-13), pp. 1103–1111, 10.1016/S0167-8655(99)00077-X.
  * [24] Steve Lawrence, C Lee Giles, Ah Chung Tsoi & Andrew D Back (1997): _Face recognition: A convolutional neural-network approach_.  IEEE transactions on neural networks 8(1), pp. 98–113, 10.1109/72.554195.
  * [25] Yann LeCun, Léon Bottou, Yoshua Bengio & Patrick Haffner (1998): _Gradient-based learning applied to document recognition_.  Proceedings of the IEEE 86(11), pp. 2278–2324, 10.1109/5.726791.
  * [26] Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J Kochenderfer et al. (2021): _Algorithms for verifying deep neural networks_.  Foundations and Trends® in Optimization 4(3-4), pp. 244–404, 10.1561/2400000035.
  * [27] Diego Manzanas Lopez, Sung Woo Choi, Hoang-Dung Tran & Taylor T Johnson (2023): _NNV 2.0: the neural network verification tool_.  In: International Conference on Computer Aided Verification, Springer, pp. 397–412, 10.1007/978-3-031-37703-7_19.
  * [28] _Classify Sound Using Deep Learning - MATLAB & Simulink — mathworks.com_.  https://www.mathworks.com/help/audio/gs/classify-sound-using-deep-learning.html.
  * [29] _Sequence Classification Using Deep Learning - MATLAB &; Simulink — mathworks.com_.  https://www.mathworks.com/help/deeplearning/ug/classify-sequence-data-using-lstm-networks.html.
  * [30] _Sequence Classification Using 1-D Convolutions \- MATLAB &; Simulink — mathworks.com_.  https://www.mathworks.com/help/deeplearning/ug/sequence-classification-using-1-d-convolutions.html.
  * [31] Toshio Modegi & Shun-ichi Iisaku (1997): _Application of MIDI technique for medical audio signal coding_.  In: Proceedings of the 19th Annual International Conference of the IEEE Engineering in Medicine and Biology Society.’Magnificent Milestones and Emerging Opportunities in Medical Engineering’(Cat. No. 97CH36136), 4, IEEE, pp. 1417–1420, 10.1109/IEMBS.1997.756970.
  * [32] Jeet Mohapatra, Tsui-Wei Weng, Pin-Yu Chen, Sijia Liu & Luca Daniel (2020): _Towards verifying robustness of neural networks against a family of semantic perturbations_.  In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, pp. 244–252, 10.1109/CVPR42600.2020.00032.
  * [33] Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi & Pascal Frossard (2016): _Deepfool: a simple and accurate method to fool deep neural networks_.  In: Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 2574–2582, 10.1109/CVPR.2016.282.
  * [34] Aaron van den Oord, Sander Dieleman, Heiga Zen, Karen Simonyan, Oriol Vinyals, Alex Graves, Nal Kalchbrenner, Andrew Senior & Koray Kavukcuoglu (2016): _Wavenet: A generative model for raw audio_.  The 9th ISCA Speech Synthesis Workshop, Sunnyvale, CA, USA, 13-15 September 2016, p. 125.
  * [35] Neelanjana Pal, Diego Manzanas Lopez & Taylor T Johnson (2023): _Robustness verification of deep neural networks using star-based reachability analysis with variable-length time series input_.  In: International Conference on Formal Methods for Industrial Critical Systems, Springer, pp. 170–188, 10.1007/978-3-031-43681-9_10.
  * [36] Gunasekaran Raja, Senbagapriya Senthilkumar, Sivaseelan Ganesan, Rithika Edhayachandran, Geetha Vijayaraghavan & Ali Kashif Bashir (2021): _AV-CPS: audio visual cognitive processing system for critical intervention in autonomous vehicles_.  In: 2021 IEEE International Conference on Communications Workshops (ICC Workshops), IEEE, pp. 1–6, 10.1109/ICCWorkshops50388.2021.9473647.
  * [37] Adam Roberts, Jesse Engel, Colin Raffel, Curtis Hawthorne & Douglas Eck (2018): _A hierarchical latent vector model for learning long-term structure in music_.  In: International conference on machine learning, PMLR, pp. 4364–4373.
  * [38] Wenjie Ruan, Min Wu, Youcheng Sun, Xiaowei Huang, Daniel Kroening & Marta Kwiatkowska (2019): _Global Robustness Evaluation of Deep Neural Networks with Provable Guarantees for the $L\\_0$ Norm_.  Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pp. 5944–5952, 10.24963/ijcai.2019/824.
  * [39] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel & Martin Vechev (2018): _Fast and effective robustness certification_.  In: Advances in Neural Information Processing Systems, pp. 10825–10836.
  * [40] Gagandeep Singh, Timon Gehr, Markus Püschel & Martin Vechev (2019): _An abstract domain for certifying neural networks_.  Proceedings of the ACM on Programming Languages 3(POPL), p. 41, 10.1145/3291645.
  * [41] Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow & Rob Fergus (2014): _Intriguing properties of neural networks_.  In: 2nd International Conference on Learning Representations, ICLR 2014.
  * [42] Hoang Dung Tran, Sung Woo Choi, Xiaodong Yang, Tomoya Yamaguchi, Bardh Hoxha & Danil Prokhorov (2023): _Verification of Recurrent Neural Networks with Star Reachability_.  In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1–13, 10.1145/3575870.3587128.
  * [43] Hoang-Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang & Taylor T Johnson (2019): _Star-based reachability analysis of deep neural networks_.  In: International Symposium on Formal Methods, Springer, pp. 670–686, 10.1007/978-3-030-30942-8_39.
  * [44] Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Diego Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang, Stanley Bak & Taylor T Johnson (2021): _Robustness verification of semantic segmentation neural networks using relaxed reachability_.  In: International Conference on Computer Aided Verification, Springer, pp. 263–286, 10.1007/978-3-030-81685-8_12.
  * [45] Hoang-Dung Tran, Weiming Xiang & Taylor T Johnson (2020): _Verification approaches for learning-enabled autonomous cyber–physical systems_.  IEEE Design & Test 39(1), pp. 24–34, 10.1109/MDAT.2020.3015712.
  * [46] Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak & Taylor T Johnson (2020): _NNV: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems_.  In: International Conference on Computer Aided Verification, Springer, pp. 3–17, 10.1007/978-3-030-53288-8_1.
  * [47] Finley Walden, Sagar Dasgupta, Mizanur Rahman & Mhafuzul Islam (2022): _Improving the Environmental Perception of Autonomous Vehicles using Deep Learning-based Audio Classification_.  CoRR abs/2209.04075, 10.48550/arXiv.2209.04075.
  * [48] Avery Wang et al. (2003): _An industrial strength audio search algorithm._ In: ISMIR 2003, 4th International Conference on Music Information Retrieval, Baltimore, Maryland, USA, October 27-30, 2003, Proceedings, Washington, DC, pp. 7–13.
  * [49] Zhilu Wang, Yixuan Wang, Feisi Fu, Ruochen Jiao, Chao Huang, Wenchao Li & Qi Zhu (2022): _A Tool for Neural Network Global Robustness Certification and Training_.  CoRR abs/2208.07289, 10.48550/arXiv.2208.07289.
  * [50] Jianfeng Zhao, Xia Mao & Lijiang Chen (2019): _Speech emotion recognition using deep 1D & 2D CNN LSTM networks_.  Biomedical signal processing and control 47, pp. 312–323, 10.1016/j.bspc.2018.08.035.


# Electric field tunable non-linear Hall terahertz detector in Dual quantum
spin Hall insulator $\text{TaIrTe}_{4}$

Junwen Lai  School of Materials Science and Engineering, University of Science
and Technology of China, Shenyang 110016, China.  Shenyang National Laboratory
for Materials Science, Institute of Metal Research,Chinese Academy of
Sciences, Shenyang 110016, China.  Jie Zhan  School of Materials Science and
Engineering, University of Science and Technology of China, Shenyang 110016,
China.  Shenyang National Laboratory for Materials Science, Institute of Metal
Research,Chinese Academy of Sciences, Shenyang 110016, China.  Peitao Liu
School of Materials Science and Engineering, University of Science and
Technology of China, Shenyang 110016, China.  Shenyang National Laboratory for
Materials Science, Institute of Metal Research,Chinese Academy of Sciences,
Shenyang 110016, China.  Xing-Qiu Chen<EMAIL_ADDRESS>School of
Materials Science and Engineering, University of Science and Technology of
China, Shenyang 110016, China.  Shenyang National Laboratory for Materials
Science, Institute of Metal Research,Chinese Academy of Sciences, Shenyang
110016, China.  Yan Sun<EMAIL_ADDRESS>School of Materials Science and
Engineering, University of Science and Technology of China, Shenyang 110016,
China.  Shenyang National Laboratory for Materials Science, Institute of Metal
Research,Chinese Academy of Sciences, Shenyang 110016, China.

###### Abstract

Nonlinear Hall effect (NHE) can be generated via Berry curvature dipole (BCD)
on nonequilibrium Fermi surface in a non-magnetic system without inversion
symmetry. To achieve a large BCD, strong local Berry curvatures and their
variation with respect to momentum are necessary and hence topological
materials with strong inter-band coupling emerge as promising candidates. In
this study, we propose a switchable and robust BCD in the newly discovered
dual quantum spin Hall insulator (QSHI) $\text{TaIrTe}_{4}$ by applying out-
of-plane electric fields. Switchable BCD could be found along with topological
phase transitions or insulator-metal transition in the primitive cell and CDW
phases of $\text{TaIrTe}_{4}$ monolayer. This work presents an instructive
strategy for achieving a switchable and robust BCD within dual QSHIs, which
should be helpful for designing the NHE-based THz radiations detector.

##  I Introduction

In nonlinear second-order quantum responses, the Berry curvature dipole (BCD)
has recently attracted much attention as it could widely occur in non-magnetic
systems with breaking inversion symmetry at both zero and twice driving
frequency[1, 2]. Unlike the well-known anomalous Hall effect (AHE) which
serves as a summation of Berry curvature, BCD manifests as a spatially varying
distribution of Berry curvature in momentum space and does not require time
reversal symmetry broken. In the last decades, BCD has provided inspirations
in many physical properties and applications including spintronics, energy
harvesting and microwave detection [3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
15]. Very recently, the utilization of BCD as a rectifier of terahertz (THz)
wave provides a new strategy for the THz radiation detection based on
intrinsic electronic band structures in materials[10], see Fig. 1. The THz
technology is making groundbreaking advancement and has already been proposed
as a next-generation technology in many fields including spectroscopy,
sensing, information and communication[16, 17]. Despite these wide potentials,
its practical application as THz detection still faces challenges in obtaining
a sensitive, switchable, and significant signal, as well as the compatibility
to integral into currently using electronic devices. Therefore, new design of
the devices and materials candidates are desired.

Materials with high BCD have been studied in various systems including
topological insulators (TIs), Weyl semimetals (WSMs), transition metal
dichalcogenides, anti-ferromagnetic metals, etc., both theoretically and
experimentally [4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]. Topological
materials are naturally with great potential to have large BCD due to their
large local Berry curvature originating from the band inversion. The electric
field serves as an effective method to tune the electronic structures and
induce phase transition in two-dimensional (2D) topological materials[18, 19,
7, 13, 15]. Therefore, tunable NHE in 2D topological materials is expected in
the condition with gating fields. The experimental studies about BCD in 2D TIs
are rare due to the lack of promising material candidates. Most studies focus
on transition metal dichalcogenides $\text{WTe}_{2}\text{/MoTe}_{2}$ and the
moiré superlattice[4, 6, 7, 13].

Very recently, a new topological phase of dual quantum spin Hall insulator
(QSHI) was discovered in $\text{TaIrTe}_{4}$[20] monolayer. In addition to the
nontrivial band gap at the charge neutrality points[21, 22], a new $Z_{2}$ gap
can be generated when the chemical potential shifts to the van Hove
singularity (VHS) point, which reveals strong inter-band coupling in a large
energy window. In this work, the electronic structure and topological phase
transition of this new phase are studied in detail. Based on the electronic
structure evolution, we calculated its switchable non-linear Hall performance
under a varying electric field. Taking advantage of the switchable NHE and
large current responsivity in monolayer $\text{TaIrTe}_{4}$, a BCD based Hall
rectifier could be designed and utilized in the AC electrical fields and THz
radiation detection.

Figure 1:  Schematic view of terahertz (THz) photodetection based on the Berry
curvature dipole (BCD) of the quantum spin Hall insulator (QSHI)
$\text{TaIrTe}_{4}$. $\varepsilon_{y}$ is the amplitude of the THz polarized
light along $y$ direction, $j_{x}$ is the non-linear DC along $x$ direction,
$E$ is the electric field perpendicular to the monolayer $\text{TaIrTe}_{4}$.
The strength of this mechanism could be described by the nonlinear
conductivity $\chi_{xyy}$.

##  II Method

###  II.1 Non-linear Hall effect

Consider two linear polarized THz radiations or AC electric fields defined by
$\bm{\varepsilon}_{b}(t)=\varepsilon_{b}e^{i\omega t}$ and
$\bm{\varepsilon}_{c}(t)=\varepsilon_{c}e^{i\omega t}$, where $b$ and $c$ are
the polarized direction and $\omega$ is the wave frequency. The non-linear
Hall rectify current along $a$ direction is given by[1]

$\aligned j_{a}=\chi_{abc}\varepsilon_{b}\varepsilon_{c}^{*}$ (1)

By considering the symmetry of this second-order tensor and ignoring the
conductivity coefficient, it’s convenient to reform $\chi_{abc}$ into a two-
indices quantity $D_{bd}$. Besides, only $z$ component of Berry curvature
exists for 2D material. Thus, only components with $d=z$ and $a,c=x,y$ can
exist, which reads

$\aligned\chi_{xby}=-\chi_{ybx}=\frac{e^{3}\tau}{2\hbar^{2}(1+i\omega\tau)}D_{bz}$
(2)

$\aligned
D_{bz}=\int[d\mathbf{k}]\sum_{n}f_{n\mathbf{k}}\frac{\partial\Omega_{z\mathbf{k}}^{n}}{\partial
k_{b}}$ (3)

where $\tau$ is the electron relaxation time, and
$f_{n\mathbf{k}}=1/(e^{(E_{\mathbf{k}}-E_{f}-\mu)/\epsilon}+1)$ is the Fermi-
Dirac distribution under the equilibrium state. $\Omega_{z\mathbf{k}}^{n}$ is
the Berry curvature of the $n$-th band at momenta $\mathbf{k}$, which reads

$\aligned\Omega_{z\mathbf{k}}^{n}=2i\hbar^{2}\sum_{m\neq
n}\frac{\braket{u_{n\mathbf{k}}}{\hat{v}_{x}}{u_{m\mathbf{k}}}\braket{u_{m\mathbf{k}}}{\hat{v}_{y}}{u_{n\mathbf{k}}}}{\left(E_{n\mathbf{k}}-E_{m\mathbf{k}}\right)^{2}}$
(4)

where $\hat{v}_{a}=\frac{1}{\hbar}\frac{\partial\hat{H}}{\partial k_{a}}$ is
the velocity operator along $a$ direction, $\hat{H}$ is the Hamiltonian in
Wannier basis, $\ket{u_{n\mathbf{k}}}$ is the eigenstate of Hamiltonian with
the eigenvalue of $E_{n\mathbf{k}}$. Note that the BCD is unit-free in three-
dimension and with a unit of Angstrom in 2D.

Considering the scattering rate of electrons is in the order of tens of THz,
the NHE in materials can be utilized in rectifying incident THz radiations
with the output of direct electrical current. Corresponding performance of the
THz detector device can be characterized by the strength of the electric
output per optical input, which is known as the current repsonsivity[10]. To
obtain it, the power of the Hall rectifier $P$ should also be taken into
consideration other than the BCD, which reads

$\aligned
P=\frac{e\tau}{\hbar(1+i\omega\tau)}\sigma_{ab}\varepsilon_{a}\varepsilon_{b}LW$
(5)

where $L$ and $W$ are the length and width of the Hall rectifier.
$\sigma_{ab}$ is the Drude weight, which is given by

$\aligned\sigma_{ab}=&\frac{e}{\hbar}\int[d\mathbf{k}]\frac{\partial
E}{\partial k_{a}}\frac{\partial E}{\partial k_{b}}\left(-\frac{\partial
f_{\mathbf{k}}}{\partial E}\right)\\\
=\frac{e}{\hbar}\int[d\mathbf{k}]\sum_{n}\braket{n}{\hat{v}_{a}}{n}\braket{n}{\hat{v}_{b}}{n}\delta(E_{\mathbf{k}}-E_{n})$
(6)

Thus, the current responsivity $R_{a}$ of the Hall rectifier could be given by
the output current per adsorbed power which reads

$\aligned R_{a}=\frac{I_{H}}{P}=\frac{1}{W}\frac{D_{az}}{\hbar\sigma_{aa}}$
(7)

where the term of $\tau$/(1+$i\omega\tau$) with electron relaxation time is
canceled out.

The monolayer $\text{TaIrTe}_{4}$ belongs to a centrosymmetric space group
$P2_{1}/m$, where nonlinear response is forbidden due to the inversion
symmetry. After applying an electric field perpendicular to the layer, this
inversion symmetry is broken and only a mirror symmetry
{$\mathcal{M}_{y}|(0,1/2,0)$} is preserved. This symmetry leads to an odd
$\frac{\partial\Omega_{z}}{\partial k_{x}}$ and an even
$\frac{\partial\Omega_{z}}{\partial k_{y}}$. Therefore, only the components
with $b=y$ ($D_{yz}$, $\chi_{xyy}$, $\chi_{yyx}$, $\sigma_{yy}$ and $R_{y}$)
are allowed to exist. The numerical integration over the whole Brillouin zone
(BZ) is performed on a dense $k$-grid of 2000$\times$2000 and 500$\times$500
for the primitive cell and CDW phase of the monolayer $\text{TaIrTe}_{4}$
respectively and are tested to be fully coverage for both BCD and Drude term.
Wilson loop is carried out in Wannier basis to characterize the $Z_{2}$
topological charges of $\text{TaIrTe}_{4}$ under different electric
fields[23].

###  II.2 Ground state calculation

The crystal structure of the monolayer $\text{TaIrTe}_{4}$ is fully optimized
with force difference on each atom no more than 0.001 eV/Å in Vienna Ab Initio
Simulation Package (VASP)[24, 25] and in good agreement with experimental
reports[26, 20]. Ground state calculation is performed in Full Potential
Localized-orbital (FPLO) program to obtain a symmetry conserved Hamiltonian in
Wannier basis[27, 28, 29, 30]. The electric field is simulated by adding an
on-site energy which varies linearly with the Wannier center coordinates
perpendicular to the 2D plane on the Hamiltonian in Wannier basis. The
Hamiltonian of the 15$\times$1$\times$1 supercell is built from the hopping
strength extracted from the Wannier function of the primitive cell. The CDW
phase is simulated by a superlattice modulation of Fröhlich-Peierls
Hamiltonian of $H=H_{r}+Vcos(Qx)u_{r}^{\dagger}u_{r}$, where $V$ is the CDW
modulation strength, $Q$ is the magnitude of the CDW vector and $x$ is the
Wannier center coordinate along $x$ axis[31, 23].

##  III Results and Discussion

###  III.1 Electronic structure of monolayer $\text{TaIrTe}_{4}$

The electronic band structure of monolayer $\text{TaIrTe}_{4}$ is shown in
Fig. 2(b), where all the bands are doubly degenerate due to the inversion
symmetry. From energy dispersion we can find a band inversion near $\Gamma$
point, which corresponds to a QSHI phase with a band gap of around 45 meV, in
agreement with the previous reports[21, 22, 20]. After applying an electric
field along $z$, the inversion symmetry is broken and leads to a band
splitting between spin-up and spin-down channels, see Fig. 2(c-f). This band
splitting gradually grows as the electric field increases. Meanwhile, the band
gap along $S$-$X$ gradually decreases and gets crossed when the field reaches
around 1.0 eV/c, see Fig. 2(d). After the crossing, the band gap is reformed
and the monolayer $\text{TaIrTe}_{4}$ becomes a trivial insulator with a band
gap of around 13 meV(E=2.0 eV/c).

Figure 2:  (a) Brillouin Zone (BZ) of $\text{TaIrTe}_{4}$ monolayer; (b-f)
Energy dispersions of $\text{TaIrTe}_{4}$ monolayer with different electric
fields $E$. $E$ is given in the unit of eV/c, with $c=4.010~{}\text{\AA}$ as
the layer thickness of $\text{TaIrTe}_{4}$ monolayer.

###  III.2 Non-linear Hall effect in monolayer $\text{TaIrTe}_{4}$

Figure 3: (a) Chemical potential dependent BCD of $\text{TaIrTe}_{4}$
monolayer at different electric fields. Four peaks can be found near the Fermi
energy, with $\mu_{1}$=-22 meV, $\mu_{2}$=-14 meV, $\mu_{3}$=12 meV,
$\mu_{4}$=40 meV. (b) The BCD of $\text{TaIrTe}_{4}$ monolayer at chemical
potentials of $\mu_{2}$ and $\mu_{4}$ with varying electric fields. (c) The
chemical potential dependent Drude weight $\sigma_{yy}$ of $\text{TaIrTe}_{4}$
monolayer at different electric fields. (d) The chemical potential dependent
current responsivity times width (RW) of $\text{TaIrTe}_{4}$ monolayer with
different electric fields.

The above band structure analysis demonstrates the inversion symmetry broken
after applying an out-of-plane field, which is essential for generating a non-
linear response. Besides, topological phase transitions would happen for some
given electric fields. Since such phase transitions are often along with
dramatic changes in Berry curvature distribution, we analyzed corresponding
non-linear Hall transport in detail, see Fig. 3. In the absence of the
electric field, the BCD is forced to zero due to the inversion symmetry (black
line). After applying a small electric field of E = 0.4 eV/c, the $D_{yz}$
component of BCD increases sharply from zero, consistent with our symmetry
analysis. Besides, a peak with the magnitude of 2.4 Å can be found at the
chemical potential of 40 meV (red line).

As the field continually increases to 1.0 eV/c, a phase transition from QSHI
to normal insulator happens. Meanwhile, a new peak appears at around $\mu_{1}$
and the peak at $\mu_{4}$ becomes larger (green line). This can be attributed
to the strength of inversion symmetry breaking induced by the electric field.
After the phase transition when the electric field reaches around 2.0 eV/c
(blue line), two peaks at $\mu_{2}$ and $\mu_{3}$ appear with opposite signs
with respect to that at $\mu_{1}$ and $\mu_{4}$.

To have a further understanding of the tunability of BCD, we analyzed the
field dependent $D_{yz}$ at given chemical potentials of $\mu_{2}$ and
$\mu_{4}$, respectively, see Fig. 3(b). For the behavior away from Fermi
energy ($\mu_{4}$), the change of $D_{yz}$ is trivial as it increases
monotonically up to 1.0 eV/c and saturates at around 3.5 Å. Meanwhile, for the
case near Fermi energy ($\mu_{2}$), the rate of increase in $D_{yz}$ slows
down at 1.0 eV/c and subsequently decreases rapidly after 1.4 eV/c, resulting
in a sign change at 1.6 eV/c. This indicates the emergence of some negative
contribution after the topological phase transition. Besides, the magnitude of
this negative contribution increases much faster than the positive counterpart
with the increasing electric field, resulting in a sign change near the Fermi
energy.

To obtain the absorbed power of the THz Hall rectifier, we also calculated the
Drude term $\sigma_{yy}$, see Fig. 3(c). Due to the intra-band Drude term, a
zero plateau emerges within the band gap near the Fermi level. The magnitude
of $\sigma_{yy}$ grows rapidly as it gets away from the gap. When an electric
field is applied, the basic shape of $\sigma_{yy}$ is generally kept, and
changes mainly occur in the zero plateau range and the curve broadening. Thus,
the current responsivity R becomes larger near the band edge as it varies
inversely with the absorbed power $\sigma_{yy}$. This can be confirmed by the
analysis of the RW plot in Fig. 3(d). Although the magnitude of the BCD peak
near $\mu_{2}$ is smaller compared to the peak at $\mu_{1}$, the current
responsivity exhibits distinct behavior, as the peak near $\mu_{1}$
demonstrates greater robustness and tunability.

The intensity of RW could reach around 1.4$\times 10^{-2}$ $\mu$m/V,
indicating the potential to get a current responsivity R of 0.14 V-1 with a
sample width of 0.1 $\mu$m. Taking advantage of the controllable growth nature
of 2D materials, a smaller sample width can be achieved to yield a stronger
signal. Additionally, the direction of the nonlinear Hall current can be
flipped by the sign of the applied electric field, as illustrated in the
comparison between the red solid and dot curves in Fig. 3(a,b,d).

Figure 4:  The Berry curvature dipole distribution
$\tilde{D}_{yz\bm{k}}=\sum_{n}\frac{f_{n\bm{k}}}{V}\frac{\partial\Omega_{z\bm{k}}^{n}}{\partial
k_{y}}$ under different electric fields of (a) E = 0.4 eV/c, (b) E = 1.0 eV/c,
(c) E = 1.4 eV/c, and (d) E = 2.0 eV/c with a given chemical potential
$\mu_{2}$=-14 meV. BZ alone $k_{y}$ axis is zoomed in as the other part is
negligible, colorbars of $\tilde{D}_{yz\bm{k}}$ are all in unit of $10^{4}$.
Figure 5:  The Berry curvature distribution
$\tilde{\Omega}_{z\bm{k}}=\sum_{n}f_{n\bm{k}}\Omega_{z\bm{k}}^{n}$ of
$\text{TaIrTe}_{4}$ monolayer at different chemical potentials of (a)
$\mu_{1}$=-22 meV, (b) $\mu_{2}$=-14 meV, (c) $\mu_{3}$=12 meV, and (d)
$\mu_{4}$=40 meV under an electric field of E=2.0 eV/c. The BCD distribution
$\tilde{D}_{yz\bm{k}}$ of $\text{TaIrTe}_{4}$ monolayer at different chemical
potentials of (e) $\mu_{1}$=-22 meV, (f) $\mu_{2}$=-14 meV, (g) $\mu_{3}$=12
meV, and (h) $\mu_{4}$=40 meV under an electric field of E=2.0 eV/c. BZ along
$k_{y}$ axis is zoomed in as the other part is negligible, color bars of
$\tilde{\Omega}_{z\bm{k}}$ and $\tilde{D}_{yz\bm{k}}$ are in unit of
$10^{2}~{}\hbar/e^{2}(\text{\AA})$ and $10^{4}$, respectively.  Figure 6:  (a)
Band structure of the CDW phase $\text{TaIrTe}_{4}$ monolayer. (b) Band
structure of the CDW phase $\text{TaIrTe}_{4}$ monolayer under an electric
field of E=0.16 eV/c. (c) The chemical potential dependent BCD of the CDW
phase $\text{TaIrTe}_{4}$ monolayer at different electric fields. (d) The
chemical potential dependent current responsivity times width (RW) of the CDW
phase $\text{TaIrTe}_{4}$ monolayer at different electric fields.

To understand the sign change of BCD under different electric fields and
chemical potentials, we analyzed the local distribution $\tilde{D}_{yz\bm{k}}$
and $\tilde{\Omega}^{z}_{\mathbf{k}}$, see Figs. 4 and 5. Since the Fermi
crossing mainly takes place near the $k_{y}=0$ line, the non-zero BCD
distribution is confined in the range of $k_{y}$ between -0.25 and 0.25
$\text{\AA}^{\text{-1}}$, see Figs. 2 and 4. Applying an electric field, a
sign change at the chemical potential $\mu_{2}=-14~{}\text{meV}$ could be
found. The detailed local distribution of $\tilde{D}_{yz\bm{k}}$ at
$\mu_{2}=-14~{}\text{meV}$ is shown in Fig. 4. For the $\tilde{D}_{yz\bm{k}}$
under a small electric field of E=0.4 eV/c, the high intensities mainly locate
near the $\Lambda$ point, see Fig. 4(a).

For convenience, the dominant contribution is divided into three areas around
the $\Lambda$ point, where a1 and a3 exhibit positive dominance while a2 is
negative. With detailed quantitative analysis, we can see that a1 and a3 make
a larger contribution compared to a2 at low electric field, see Fig. 4(a),
which results in the positive ${D}_{yz}$ in Fig. 3(a). As the electric field
increases, the magnitude of $\tilde{D}_{yz\bm{k}}$ in a1 and a3 grows and
decays, respectively. Meanwhile, the magnitude in a2 increases rapidly and
eventually becomes dominated after the topological phase transition. The joint
effect of the three areas explains why the sign change of $D_{yz}$ is later
than the topological phase transition.

The chemical potential-dependent BCD is also analyzed at a given E=2.0 eV/c,
see Fig. 5. Both local Berry curvature $\tilde{\Omega}_{z\bm{k}}$(Fig. 5(a-d))
and BCD $\tilde{D}_{yz\bm{k}}$ (Fig. 5(e-h)) of the four peaks in Fig. 3 are
calculated. Owing to the mirror plane of {$\mathcal{M}_{y}|(0,1/2,0)$},
$\tilde{\Omega}_{z\bm{k}}$ is even with respect to $k_{x}$ and odd with
respect to $k_{y}$ under an out-of-plane electric field. Since BCD is a first-
order derivative of the Berry curvature, it exhibits different parity
characteristics compared to the Berry curvature with respect to momentum.
Therefore, $\tilde{D}_{yz\bm{k}}$ presents as an even function of $k_{x}$ and
$k_{y}$, respectively, see Fig. 5(e-h).

With the above understanding of symmetry analysis, we go to the details about
the Berry curvature distribution in $k$ space, see in Fig. 5(a-d). As depicted
in Fig. 5(a), two hot spots could be seen around $\Theta$ and $\Gamma$ points
in the positive BZ zone, which are negative and positive dominated,
respectively. The three peaks of $\mu_{1}$-$\mu_{3}$ in Fig. 3(a) share
similar Berry curvature distributions, see the comparison of Fig. 5(a-c).
Owing to the crossing of the conduction band, an empty part appears near the
$\Theta$ point in Fig. 5(c). As a consequence, the distribution of
$\tilde{D}_{yz\bm{k}}$ in Fig. 5(e-g) also shows a similar shape. The negative
region in $\tilde{\Omega}_{z\bm{k}}$ splits into two areas with opposite signs
in $\tilde{D}_{yz\bm{k}}$. The intensity of these areas differs as the
negative part is stronger in $\mu_{2}$ and $\mu_{3}$, which primarily
contributes to the sign change of $D_{yz}$ near the Fermi level. Besides, the
magnitude of $\tilde{\Omega}_{z\bm{k}}$ around $\Gamma$ is small and makes
little contribution to the $D_{yz}$. As presented in Figs. 5(d) and (h), there
are multiple band contributions at $\mu_{4}$ = 40 meV, and they are mainly
dominated by the positive intensity, leading to the corresponding peak in Fig.
3(a).

###  III.3 Non-linear Hall transport in CDW phase

Apart from the QSHI state at the charge neutrality point, a new $\text{Z}_{2}$
gap can be generated by placing the Fermi level at van Hove singularity point.
It has been reported that the CDW phase in monolayer $\text{TaIrTe}_{4}$ has a
wave vector of Q*=(0.068,0)[20]. With the inspiration from experimental
reports, we also computed the BCD and corresponding current responsivity near
the CDW gap. According to the quantum electrical transport measurements, a
periodic potential of V=0.13 eV is taken into account to generate the CDW
phase, see Fig. 6(a). Similar to the original primitive cell, all bands in
Fig. 6(a) are doubly degenerated due to the inversion symmetry. Thus, an out-
of-plane electric field is applied to induce the non-linear Hall response, see
Fig. 6(b). As a result, a significant band split was induced under a small
electric field of E=0.16 eV/c (approximately 0.4 eV/nm), see Fig. 6(b). All
three CDW gaps disappear along with the increasing of electric field.

With the guiding principle from band structures, we analyzed the non-linear
Hall transport in detail. Multiple peaks of BCD and current responsivity can
be found in Fig. 6(c,d) and they show similar trends under different electric
fields. There are three clear peaks near the Fermi level. Two positive peaks
with the magnitude of 1.67 Å are located at around -54 meV and -26 meV,
respectively. While a negative peak of -1.31 Å is located at around -3 meV.
These results suggest that the CDW phase of monolayer $\text{TaIrTe}_{4}$ can
also be tuned by shifting the chemical potential near the CDW gap.

##  IV Conclusion

In this work, we systemically studied the electronic structures and the non-
linear Hall transports in the new discovered topological state of dual QSHI in
$\text{TaIrTe}_{4}$. Strong peaks of BCD were identified in the condition of a
gating electric field and found to be switchable in terms of both sign and
magnitude. Through the analysis of momentum-resolved BCD, we reveal that the
switchable phenomenons correspond precisely to the topological phase
transition in both the primitive cell and CDW phase. The results from our
calculations illustrate that the topological band gaps in dual QSHIs offer
natural platforms to obtain strong and tunable NHE and they exhibit promising
potential applications in the next generation of THz radiation detection
technologies.

###### Acknowledgements.

This work is supported by the National Key R&D Program of China
2021YFB3501503, National Natural Science Foundation of China (Grants
No.52271016, No.52188101 ), and Liaoning Province (Grant No. XLYC2203080).
Part of the numerical calculations in this study were carried out on the ORISE
Supercomputer(No. DFZX202319).

## References

  * [1] I. Sodemann and L. Fu, “Quantum nonlinear hall effect induced by berry curvature dipole in time-reversal invariant materials,” Phys. Rev. Lett., vol. 115, p. 216806, Nov. 2015.
  * [2] Z. Z. Du, H.-Z. Lu, and X. C. Xie, “Nonlinear Hall effects,” Nature Reviews Physics, vol. 3, pp. 744–752, Nov. 2021.
  * [3] D. Xiao, M.-C. Chang, and Q. Niu, “Berry phase effects on electronic properties,” Rev. Mod. Phys., vol. 82, pp. 1959–2007, July 2010.
  * [4] J.-S. You, S. Fang, S.-Y. Xu, E. Kaxiras, and T. Low, “Berry curvature dipole current in the transition metal dichalcogenides family,” Phys. Rev. B, vol. 98, p. 121109(R), Sept. 2018.
  * [5] Y. Zhang, Y. Sun, and B. Yan, “Berry curvature dipole in Weyl semimetal materials: An ab initio study,” Phys. Rev. B, vol. 97, p. 041101(R), Jan. 2018.
  * [6] Y. Zhang, J. van den Brink, C. Felser, and B. Yan, “Electrically tuneable nonlinear anomalous Hall effect in two-dimensional transition-metal dichalcogenides WTe2 and MoTe2,” 2D Materials, vol. 5, p. 044001, July 2018.
  * [7] S.-Y. Xu, Q. Ma, H. Shen, V. Fatemi, S. Wu, T.-R. Chang, G. Chang, A. M. M. Valdivia, C.-K. Chan, Q. D. Gibson, J. Zhou, Z. Liu, K. Watanabe, T. Taniguchi, H. Lin, R. J. Cava, L. Fu, N. Gedik, and P. Jarillo-Herrero, “Electrically switchable Berry curvature dipole in the monolayer topological insulator WTe2,” Nature Physics, vol. 14, pp. 900–906, Sept. 2018.
  * [8] C. Wang, Y. Gao, and D. Xiao, “Intrinsic nonlinear hall effect in antiferromagnetic tetragonal CuMnAs,” Phys. Rev. Lett., vol. 127, p. 277201, Dec. 2021.
  * [9] P. A. Pantaleón, T. Low, and F. Guinea, “Tunable large Berry dipole in strained twisted bilayer graphene,” Phys. Rev. B, vol. 103, p. 205403, May 2021.
  * [10] Y. Zhang and L. Fu, “Terahertz detection based on nonlinear Hall effect without magnetic field,” Proceedings of the National Academy of Sciences, vol. 118, p. e2100736118, May 2021.
  * [11] S. Sinha, P. C. Adak, A. Chakraborty, K. Das, K. Debnath, L. D. V. Sangani, K. Watanabe, T. Taniguchi, U. V. Waghmare, A. Agarwal, and M. M. Deshmukh, “Berry curvature dipole senses topological transition in a moiré superlattice,” Nature Physics, vol. 18, pp. 765–770, July 2022.
  * [12] Q. Fu, X. Cong, X. Xu, S. Zhu, X. Zhao, S. Liu, B. Yao, M. Xu, Y. Deng, C. Zhu, X. Wang, L. Kang, Q. Zeng, M.-L. Lin, X. Wang, B. Tang, J. Yang, Z. Dong, F. Liu, Q. Xiong, J. Zhou, Q. Wang, X. Li, P.-H. Tan, B. K. Tay, and Z. Liu, “Berry Curvature Dipole Induced Giant Mid-Infrared Second-Harmonic Generation in 2D Weyl Semiconductor,” Advanced Materials, vol. 35, p. 2306330, Nov. 2023.
  * [13] X.-G. Ye, H. Liu, P.-F. Zhu, W.-Z. Xu, S. A. Yang, N. Shang, K. Liu, and Z.-M. Liao, “Control over berry curvature dipole with electric field in WTe2,” Phys. Rev. Lett., vol. 130, p. 016301, Jan. 2023.
  * [14] S. Duan, F. Qin, P. Chen, X. Yang, C. Qiu, J. Huang, G. Liu, Z. Li, X. Bi, F. Meng, X. Xi, J. Yao, T. Ideue, B. Lian, Y. Iwasa, and H. Yuan, “Berry curvature dipole generation and helicity-to-spin conversion at symmetry-mismatched heterointerfaces,” Nature Nanotechnology, vol. 18, pp. 867–874, Aug. 2023.
  * [15] K. Łempicka Mirek, M. Król, H. Sigurdsson, A. Wincukiewicz, P. Morawiak, R. Mazur, M. Muszyński, W. Piecek, P. Kula, T. Stefaniuk, M. Kamińska, L. D. Marco, P. G. Lagoudakis, D. Ballarini, D. Sanvitto, J. Szczytko, and B. Pietka, “Electrically tunable berry curvature and strong light-matter coupling in liquid crystal microcavities with 2d perovskite,” Science Advances, vol. 8, no. 40, p. eabq7533, 2022.
  * [16] M. Tonouchi, “Cutting-edge terahertz technology,” Nature Photonics, vol. 1, pp. 97–105, Feb. 2007.
  * [17] R. I. Stantchev, X. Yu, T. Blu, and E. Pickwell-MacPherson, “Real-time terahertz imaging with a single-pixel detector,” Nature Communications, vol. 11, p. 2535, May 2020.
  * [18] J. Maciejko, T. L. Hughes, and S.-C. Zhang, “The quantum spin hall effect,” Annual Review of Condensed Matter Physics, vol. 2, no. Volume 2, 2011, pp. 31–53, 2011.
  * [19] S. Wu, V. Fatemi, Q. D. Gibson, K. Watanabe, T. Taniguchi, R. J. Cava, and P. Jarillo-Herrero, “Observation of the quantum spin Hall effect up to 100 kelvin in a monolayer crystal,” Science, vol. 359, pp. 76–79, Jan. 2018.
  * [20] J. Tang, T. S. Ding, H. Chen, A. Gao, T. Qian, Z. Huang, Z. Sun, X. Han, A. Strasser, J. Li, M. Geiwitz, M. Shehabeldin, V. Belosevich, Z. Wang, Y. Wang, K. Watanabe, T. Taniguchi, D. C. Bell, Z. Wang, L. Fu, Y. Zhang, X. Qian, K. S. Burch, Y. Shi, N. Ni, G. Chang, S.-Y. Xu, and Q. Ma, “Dual quantum spin Hall insulator by density-tuned correlations in TaIrTe4,” Nature, Mar. 2024.
  * [21] J. Liu, H. Wang, C. Fang, L. Fu, and X. Qian, “Van der Waals Stacking-Induced Topological Phase Transition in Layered Ternary Transition Metal Chalcogenides,” Nano Lett., vol. 17, pp. 467–475, Jan. 2017.
  * [22] P.-J. Guo, X.-Q. Lu, W. Ji, K. Liu, and Z.-Y. Lu, “Quantum spin Hall effect in monolayer and bilayer TaIrTe4,” Phys. Rev. B, vol. 102, p. 041109(R), July 2020.
  * [23] R. Yu, X. L. Qi, A. Bernevig, Z. Fang, and X. Dai, “Equivalent expression of Z2 topological invariant for band insulators using the non-Abelian Berry connection,” Phys. Rev. B, vol. 84, p. 075119, Aug. 2011.
  * [24] G. Kresse and J. Furthmuller, “Efficiency of ab-initio total energy calculations for metals and semiconductors using a plane-wave basis set,” Comput. Mater. Sci., vol. 6, pp. 15–50, July 1996.
  * [25] G. Kresse and J. Furthmuller, “Efficient iterative schemes for ab initio total-energy calculations using a plane-wave basis set,” Phys. Rev. B, vol. 54, pp. 11169–11186, Oct. 1996.
  * [26] A. Mar, S. Jobic, and J. A. Ibers, “Metal-metal vs tellurium-tellurium bonding in WTe2 and its ternary variants TaIrTe4 and NbIrTe4,” Journal of the American Chemical Society, vol. 114, no. 23, pp. 8963–8971, 1992.
  * [27] K. Koepernik and H. Eschrig, “Full-potential nonorthogonal local-orbital minimum-basis band-structure scheme,” Phys. Rev. B, vol. 59, pp. 1743–1757, Jan. 1999.
  * [28] I. Opahle, K. Koepernik, and H. Eschrig, “Full-potential band-structure calculation of iron pyrite,” Phys. Rev. B, vol. 60, pp. 14035–14041, Nov. 1999.
  * [29] K. Koepernik, O. Janson, Y. Sun, and J. van den Brink, “Symmetry-conserving maximally projected Wannier functions,” Phys. Rev. B, vol. 107, p. 235135, June 2023.
  * [30] J. P. Perdew, K. Burke, and M. Ernzerhof, “Generalized gradient approximation made simple,” Phys. Rev. Lett., vol. 77, pp. 3865–3868, Oct. 1996.
  * [31] H. Fröhlich, “On the theory of superconductivity: The one-dimensional case,” Proceedings of the Royal Society of London. Series A. Mathematical and Physical Sciences, vol. 223, no. 1154, pp. 296–305, 1954.