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

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 [21,23,24]. 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 [12, 32, 40]. The arena of network verification has primarily concentrated on image inputs, particularly emphasizing the assurance of safety and robustness in various classification neural networks [2, 7, 19, 31, 43, 44]. Previous investigations have scrutinized a range of network architectures, encompassing feed-forward neural networks (FFNNs [42]), convolutional neural networks (CNNs [44]), semantic segmentation networks (SSNs [43]), and a few using Recurrent Neural Networks (RNNs [41]) employing diverse set-based reachability tools such as Neural Network Verification (NNV [26,45]) and JuliaReach [6], among others. Models utilizing NNs for audio classification have found application in diverse tasks, ranging from Music Genre Classification [8, 10, 11] and Environmental Sound Classification [4, 9, 13] to Audio Generation [33, 36]. 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 [35, 46], medical diagnosis [15, 30], and industrial monitoring [47]. This study introduces an extension, building upon the foundations laid by two recent studies [34,41] in the domain of formal verification.