Formal Verification for Deep Learning-based Power Control in Massive MIMO Thanh Le∗ , Takeshi Matsumura∗ , Yusheng Ji† , John C.S. Lui‡ ∗ National Institute of Information and Communications Technology (NICT), Japan
arXiv:2607.14500v1 [cs.NI] 16 Jul 2026
† National Institute of Informatics (NII), Japan, ‡ The Chinese University of Hong Kong (CUHK), China
Abstract—Deep learning is a promising approach to optimize wireless communication by simplifying the search for nearoptimal solutions. Prior studies on deep learning–based wireless communication optimization have explored supervised learning approaches that map raw user information, such as location or channel state information, to optimal power allocation vectors. While this approach demonstrates competitive performance, it is susceptible to adversarial attacks via input perturbations. Current defense mechanisms primarily rely on empirical methods, which do not provide formal guarantees of robustness. We fill this gap by proposing a formal verification framework to evaluate the robustness of deep learning-based power allocation in multi-cell massive multiple-input multiple-output (MIMO) systems against a wide range of potential adversarial input manipulations. To the best of our knowledge, this is the first attempt to formally verify deep neural networks in a regression setting with nonlinear output constraints. We model the adversary’s capabilities using hyper-rectangle constraints on their perturbation, adopt the abstraction-based bound-propagation technique (DeepPoly) to bound the interval of potential allocated powers, and formulate the minimum performance requirements as a constrained program for numerical feasibility analysis. Evaluation on publicly available datasets for power allocation in multi-cell massive MIMO indicates that a well-trained model can guarantee the local robustness under location perturbation by ± 1m while retaining a maximum 1% optimality gap. Index Terms—massive MIMO, neural network verification
I. I NTRODUCTION Massive multiple-input multiple-output (MIMO) technology is a key component of next-generation wireless networks, designed to accommodate the growing number of connected user equipments (UE) and their diverse demands for new services and applications [1]. By deploying a large number of antennas at the base station (BS), massive MIMO can leverage multiplexing gains and enable high data rates. In multi-cell massive MIMO networks, optimizing power control is crucial for achieving high performance and reducing interference between UEs both within a cell and across different cells. Power control in massive MIMO increasingly leverages deep neural network (DNN) to reduce complexity by inferring near-optimal solutions within O(1) time complexity while requiring less engineering effort to design new heuristics if the problem formulation changes. Exciting developments have emerged in this area, e.g., DNN has been supervised to approximate optimal power allocation algorithms in massive MIMO systems [2]. This work utilizes the ability of DNN to approximate arbitrary functions to map the positions of UEs in the multi-cell network to their optimal power allocation.
A few following studies have focused on training distributed architectures using only local information within each cell [3], [4]. Another work has addressed varying numbers of users by utilizing convolutional neural network (CNN) [5], while deep reinforcement learning has been applied to control power in massive MIMO networks with user mobility [6]. However, DNN-based power allocation is susceptible to adversarial attacks, where small perturbations can be added to inputs and manipulated DNNs into allocating non-optimal power to UEs [7], [8]. These perturbations are small enough to evade anomaly detection system but carefully crafted to significantly impair the DNN’s performance, e.g., reducing transmission rates, fairness, and degrade quality of service. Previous work [7] proposed an attack on DNN-based power control with the input being the locations of UEs. By using global navigation satellite system (GNSS) spoofing techniques, attackers can alter the positions of nearby UEs, thereby causing infeasible and non-optimal power allocations. To the best of our knowledge, there are three main defense approaches: (1) denoising autoencoders, (2) adversarial training, and (3) neural network verification (NNV). Firstly, denoising autoencoder networks can be employed to rectify malicious inputs [9]; however, this incurs additional computational overhead during inference. Secondly, adversarial training mixes sampled adversarial inputs to the training dataset for retraining [10]. However, given the real-valued, highdimensional input space, the sampled adversarial inputs do not guarantee completeness. Besides, this type of non-certifying defense was found to be evaded by stronger adversarial attack schemes [11]. To mitigate this cat-and-mouse game, there is a gaining traction in defenses with NNV [12], [13], [14], as NNV methods provide absolute robustness guarantee. General NNV techniques have primarily focused on verifying the safety of computer vision [15], [16], natural language processing, and goal-oriented semantic communication [17], most of them are classification or unconstrained regression tasks [18]. In contrast, our problem involves verifying nonlinear performance guarantees, e.g., guarantee minimum product of signal to interference-plus-noise ratio (SINR), which cannot be directly addressed by general NNV techniques and require additional post-processing. In DNN-based for wireless communication domain, a previous work verified robustness of DNN-based antenna selection for massive MIMO systems [19], in which DNNs are trained to classify channel information to optimal antenna configurations. As far as we
know, verifying DNN in regression-based tasks with non-linear throughput and fairness constraints remains an open challenge. We fill this gap by proposing a verification framework for DNN-based power control in massive MIMO systems. Our proposed framework systematically analyzes whether the trained DNN meets performance requirements under various levels of adversarial perturbations. First, we convert different levels of adversarial perturbation into a wide variety of hyperrectangle input properties. We apply abstraction-based boundpropagation NNV technique called DeepPoly [12], [14] to compute an over-approximation of the output, which covers all possible power allocations. Then, we propose an adaptation of the existing NNV to work with the optimization goal in the considered problem. Particularly, we check whether the model satisfies a guarantee on product of SINR, e.g., the optimality gap must fall below a certain threshold, by formulating a constrained program for feasibility analysis. II. P RELIMINARIES A. System Model To investigate the robustness of deep learning-based power control in a multi-cell massive MIMO networks, we reproduce the system model and DNN-based power control method which have been made publicly available in [2]. In this system, the massive MIMO network consist of J cells, each cell having a BS of M antennas and covers K UEs. The downlink PK signal transmitted by the BS in cell j is given by vj = k=1 wjk ujk , where ujk ∈ N (0, ρjk ) is the data signal in the downlink for UE k in BS l, with a precoding vector wjk ∈ C M that determines the transmission beamforming satisfying ||wjk ||2 = 1, thus, ρjk is the transmission power. The best precoding schemes that have been adopted by [2] in generating dataset is multicell-minimum mean square error (M-MMSE). The downlink SINR for UE k in cell j is: ρjk ajk , (1) γjk = PJ PK 2 l=1 i=1 ρli blijk + σ where σ 2 is the additive white Gaussian noise (AWGN) H j variance and the average channel gain is ajk = |E[wjk hjk ]|2 j , with hjk denoting the channel between BS j and UE k in cell j. The average interference gain is: ( H l 2 H l E[|wli hjk | ] − |E[wli hjk ]|2 , if (l, i) = (j, k), blijk = H l 2 E[|wjk hjk | ], otherwise. (2) B. Power Control Problem In this study, we attempt to verify the DNN-based optimal power allocation strategy to maximize the max-product SINR [2], which is formulated as: maximize ρjk :∀j,k
subject to
J Y K Y
γjk ,
(3a)
j=1 k=1 K X k=1
ρjk ≤ Pmax ,
j ∈ [1, J].
(3b)
The problem above seeks to maximize objective in Eq. 3a, which is the product of UEs’ SINR, while Eq. 3b ensures that the allocated power adhere to the maximum power threshold Pmax promoting a trade-off between UE’s performance and total throughput. Compared to uniform max power control and max-min spectral efficiency power control, max product SINR offers a balance between fairness and efficiency [2]. C. Deep Learning-based Power Control In [2], DNNs are employed to compute an approximated optimal power allocation that maximizes the SINR product of all UEs. A publicly available dataset1 is provided as (n) T ∈ RJ×K×2 represents an input {x(n) , ρ(n) }N n=1 , where x feature contains location of UEs, the output label ρ(n) ∈ [0, ρmax ]J×K is the optimal power, and NT denotes the size of the dataset. We denote a regression-based DNN model as N (.; θ), with x as the input to the model and the predicted output as N (x; θ) = ρ, where θ constitutes the set of parameters of the model N . The corresponding loss function is represented as L(x, ρ; θ). The goal of the DNN model is to learn the mapping from the UEs’ geographical positions, x, to the optimal power allocation solution, ρ produced by mathematical optimization tools. A feed-forward neural network architecture and mean square error (MSE) loss function that has been adopted to approximate the optimal power allocation. In the standard setting outlined in [2], the input x is a vector representing the geographical locations of all UEs in the system, while ρ is a vector containing the optimal power solution obtained by solving the power allocation problem (refer to Eq. 3) D. NNV - An Overview Given a DNN N and a property ϕ, the general NNV problem asks if ϕ is a valid property of N . Typically, ϕ is a formula of the form ϕin =⇒ ϕout , where ϕin is a property over the inputs of N and ϕout is a property over the outputs of N . This property has been used to encode safety and security requirements of DNN [20]. A DNN verifier attempts to find a counterexample to N that satisfies ϕin but violates ϕout . If no such counterexample exists, ϕ is an unsatisfiable property of N (UNSAT or proven robust); otherwise, satisfiable (SAT). III. P ROPOSED V ERIFICATION F RAMEWORK Fig. 1 illustrates our proposed robustness guarantees framework for DNN-based power control in massive MIMO through a three-phase pipeline. First, we formulate local robustness input properties encapsulating possible adversarial noise around system inputs. Then, an abstraction-based bound-propagation DNN verifier method [12], [14] is adopted to compute bounds on possible power allocations provided by a trained DNN. Finally, given the power allocation bounds, we formulate a constrained program to prove the non-existence of a power allocation that violates the maximum optimality gap guarantee, e.g., reducing the optimization objective by more than ζ. 1 https://data.ieeemlc.org/Ds2Detail
A. Local Robustness Properties Formulation Adversarial Noise
B. DNN Bound Propagation DNN for power control
Bounds on possible power allocation
(6a)
Wireless Channel UEs ' location
Channel precoding
C. Performance Guarantee via Feasibility Analysis
(6b)
Feasible?
UNSAT (robust)
Yes
(6c)
Average channel gain and interference gain
No
SAT
Fig. 1: Overview of the proposed NNV framework to verify DNN-based power control in multi-cell massive MIMO networks.
A. Local Robustness Properties Formulation We first define the input properties encoding the local robustness requirements of DNN-based power allocation. Following the threat model in [7], [10], we assume that an attacker can introduce controlled perturbations to the input fed into the DNN. For instance, the attacker may manipulate the reported positions of UEs using spoofing techniques, in which global navigation satellite system receivers are deployed near the users’ actual locations. Furthermore, the perturbation remains minimal relative to the actual input x(n) . The adversary’s objective is to compute input perturbations along the gradient direction to maximize the loss function (e.g, maximize MSE loss to optimal power allocation), thereby degrading the performance of the DNN-based power allocation system. To formally verify the robustness of the considered DNNbased power allocation scheme, we define input specifications ϕin := [ηL , ηU ], such that ηL and ηU are two vectors having the same size as input x(n) , to encode permitted perturbation levels. The adversary seeks to generate an adversarial example x′ within a constrained neighborhood of x such that the DNN output becomes erroneous. This adversarial example is constructed by adding a bounded perturbation x′ = x(n) + η to the original input x(n) , where η ∈ [ηL , ηU ]. Similarly, output specifications ϕout are introduced to capture minimum performance guarantees, requiring that the achieved performance remains at least 1 − ζ times that of the optimal solution under controlled conditions. This property, referred to as local robustness, ensures stability against small adversarial perturbations around given inputs.
lower and upper bounds for each neuron’s output with respect to its perturbed input. The procedure begins by relaxing non-linear activation functions into linear constraints. These relaxations of bounds on output of non-linear activations are then propagated through the network architecture, layer by layer, from the input to the final output. DeepPoly accepts input specifications consisting of bounds [x(n) +ηL , x(n) +ηU ], along with the trained DNN in Verification of Neural Networks Competitions (VNN-COMPs) format [23]. The output is a set of tight bounds [ρL , ρU ] on the DNNs’ outputs. Note that NNV has been generalized to general computational graphs [14], enabling the computation of linear output bounds not restricted to feed-forward neural networks but also able to find bounds of modern architectures, e.g., CNNs, ResNets, or Transformers. However, we will adhere to the feed-forward neural network architecture used in publicly available implementations to ensure reproducibility and consistency with previous works [2], [7]. C. Performance Guarantee via Feasibility Analysis The performance guarantee of DNN-based power control in multi-cell massive MIMO networks cannot be captured by existing NNV properties, which primarily target classification tasks or generic regression objectives with linear constraints [23]. We propose a constrained program to encode the non-linear performance guarantee as follow: ρL ≤ ρ ≤ ρU , γjk = PJ
In this phase, we aim to bound the upper and lower limits of power allocations given the input property and the trained DNN. Bounding the output range of a DNN under constrained input perturbations has emerged as a critical topic in NNV and certified adversarial defense [12], [14]. For a neural network N (x, θ), we analyze its behavior at a nominal input x(n) subject to a bounded perturbation η, where x = x(n) + η and x lies within an lp -norm ball Bp (x(n) , r). Computing exact output bounds of a DNN is generally intractable [21], [22]. To address this challenge, we employ DeepPoly [12] abstraction, which provides provable linear relaxation of bounds on neuron outputs given specified input perturbations. This method constructs two linear functions that serve as guaranteed
PK
i=1 ρli blijk + σ J Y K J Y K Y Y ∗ γjk ≤ (1 − ζ) γjk , j=1 k=1 j=1 k=1 l=1
B. DNN Bound Propagation
(4a) ρjk ajk 2
,
(4b) (4c)
where Eq. 4a constrains the power allocation variables ρ to lie within the bounds [ρL , ρU ] obtained from the DNN bound propagation, Eq. 4b defines the SINR γjk for each UE k in cell j based on the power allocation and channel conditions, and Eq. 4c encodes the performance guarantee by ensuring that the product of all SINR values does not fall below (1 − ζ) ∗ times the optimal product γjk . Feasibility of this program is verified using numerical optimization tools. If there exists no feasible solution then the verification problem is deemed to be unsatisfiable or UNSAT. Consequently, the DNN can guarantee to achieve a relative optimality gap of ζ for all adversarial
inputs within [ηL , ηU ]. Otherwise, the verification problem is satisfiable (SAT) and there may exist an exploitation. Since the output bounds [ρL , ρU ] represent an overapproximation, and the feasibility analysis in Eq. 4 check for violation in the superset of all possible values of ρ, the proof of robustness is a sound proof. Soundness ensures that the proposed verification framework will never produce any false positive. If a DNN is claimed to be robust against an input bound [ηL , ηU ], then the claim is guaranteed to be true. IV. E VALUATION R ESULTS A. Evaluation Setups 1) Dataset: We verify the robustness of the DNN-based power control models for multi-cell massive MIMO networks2 , which are trained using the publicly available dataset [2]. We then extract a training set of 329, 000 pairs of UE locations and their optimal power allocations, and another 500 samples form the test dataset, which is independent of the training dataset [7]. The dataset is generated with J = 4 cells, with each cell covering a square area of 250 × 250 m. A wraparound topology is used to better represent interference for UEs in the edges of the network. Within each cell, there are K = 5 UEs at a randomly and uniformly distributed location, and at a distance that is larger than 35m from the BS. The bandwidth is B = 20 MHz, with the total receiver noise power σ = −94 dBm. The pilot reuse factor τp = 1, and the maximum transmit power per UE is 20 dBm. 2) DNN Hyperparameters, input/output properties: Similar to previous work [7], we tested on two DNN architectures: (a) fc.small contain fully connected layers with [64, 32, 32, 32, 5] neurons and (b) fc.medium contain fully connected layers with [512, 256, 128, 128, 5] neurons. Two networks have 6,981 and 202,373 trainable parameters, respectively, and employ ReLU as activation units. Both models are trained on 329, 000 data pairs for 50 epochs, with a batch size of 1024 and a learning rate of 3e−4 using the Adam optimizer. The input properties for verification are constructed based on the perturbation constraint from previous adversarial attackers [7], [8]. We assume the input is in the L∞ -norm, e.g., the adversarial perturbation constraint is given as [ηL , ηU ] := [−η0 , η0 ]J×K×2 . The level of perturbation η0 is a scalar with values from {0.01, 0.1, 1, 10, 100} (meter(s)) which correspond to distance perturbation of 1 cm to 100 m. The output properties, which are the maximum optimality gap ζ, are a scalar and take values from {0.001, 0.005, 0.01, 0.05, 0.1}, which guarantee to retain 90% to 99.9% of the optimally trained model. For each property, we test the local robustness of 30 randomly drawn set of UEs input locations from the test dataset. Also, we need to test J = 4 models for J = 4 cells. Thus, the total number of verification properties for the general scenario is 3, 000 properties. 2 The Python implementation of our proposed framework is available at https://github.com/thanhlexyz/verify cfmimo
Perturbation level η0
fc.small fc.medium
± 1cm
± 10cm
± 1m
± 10m
± 100m
0.002 0.007
0.015 0.068
0.153 0.688
1.560 7.664
22.610 341.999
TABLE I: The average L1 -distance between ρL and ρU (mW).
3) Evaluation Metrics: L1 -distance between lower and upper output bound: We measure the L1 -based distance between the lower bound ρL and upper bound ρU computed by abstraction-based NNV [12], [14]. A smaller L1 -distance indicates tighter bounds and more predictable model behavior. Unsatisfiable percentage: We report the percentage of UNSAT properties, averaged across multiple test inputs x(n) . An UNSAT result indicates that the verification tool successfully proves that the DNN model maintains the required optimality gap ζ despite input perturbations within the specified bounds [ηL , ηU ]. B. Robustness Analysis We trained two architectures, fc.medium and fc.small, on a publicly available dataset to reproduce previous work [2], [7], [10], which map UE locations to maximum product SINR power allocation. Under normal operational conditions without adversarial perturbations, both models achieve competitive performance with average throughput per UE of approximately 30 Mbit/s or about 1.5bit/s/Hz, which corresponds to data from Fig. 2a in [2]. Tab. I presents the output bound analysis for both DNN architectures across different perturbation levels. The results demonstrate the relationship between input uncertainty and the bounds on output power allocation. As the perturbation level η0 increases, the L1-distance between lower and upper bounds grows exponentially for both models. This behavior aligns with our expectations, where larger input perturbations lead to wider output ranges. However, despite having identical network depth, the fc.medium model consistently produces looser bounds compared to fc.small. This occurs because the wider architecture, with more neurons per layer, introduces additional complexity and nonlinearity, making abstractionbased verification more conservative in its bound estimates. Tab. II and Tab. III present the verification success rates for both model architectures across different combinations of perturbation levels η0 and optimality gap requirements ζ. The general trend reveals that 100% UNSAT rates are consistently achieved when both the perturbation level η0 is sufficiently small and the tolerable optimality gap ζ is sufficiently large. The fc.small model consistently exhibits higher verification success rates (PUNSAT ) compared to fc.medium across most experimental configurations. Particularly for the fc.small model, our verification results guarantee that input perturbations below 1m can maintain 99% of optimal performance (ζ ≤ 0.01) with 100% confidence. These guarantees have significant implications for practical network deployment. BS can implement anomaly-detection
Perturbation level η0
ζ = 0.001 ζ = 0.005 ζ = 0.01 ζ = 0.05 ζ = 0.1
Perturbation level η0
± 1cm
± 10cm
± 1m
± 10m
± 100m
100.0 100.0 100.0 100.0 100.0
100.0 100.0 100.0 100.0 100.0
6.7 80.0 100.0 100.0 100.0
0.0 0.0 0.0 70.0 100.0
0.0 0.0 0.0 0.0 0.0
ζ = 0.001 ζ = 0.005 ζ = 0.01 ζ = 0.05 ζ = 0.1
± 1cm
± 10cm
± 1m
± 10m
± 100m
100.0 100.0 100.0 100.0 100.0
13.3 100.0 100.0 100.0 100.0
0.0 0.0 10.0 100.0 100.0
0.0 0.0 0.0 0.0 3.3
0.0 0.0 0.0 0.0 0.0
TABLE II: The average percentage of UNSAT properties for model fc.small.
TABLE III: The average percentage of UNSAT properties for model fc.medium.
mechanisms to identify potential adversarial attacks by monitoring location reports for movement speeds exceeding specifications derived from our verification bounds. For instance, network operators can leverage the evaluation results when designing safe DNN-based power allocation for massive MIMO networks, ensuring an optimality gap of no more than 10% by constraining UE movement to less than 10m between location update intervals.
service and scale verification to larger deep-learning models and more complex network settings. ACKNOWLEDGEMENT The authors thank the NICT AI R&D Promotion Unit for providing cloud GPU credits. R EFERENCES [1]
[2]
[3]
[4]
[5]
Fig. 2: Compare two models fc.small and fc.medium in terms of the average percentage of UNSAT verification properties per each perturbation level η0 and ζ = 0.5%.
[6]
[7]
[8]
Fig. 2 provides a more fine-grained analysis of the verification results presented in the previous tables, examining verification success rates across a continuous range of perturbation levels, η0 ∈ [0.1, 10] meters, with a fixed optimality gap tolerance of ζ = 0.5%. The results demonstrate that fc.small maintains a high UNSAT rate for all perturbation levels up to 1m, indicating strong provable robustness within this range. In contrast, fc.medium exhibits a sharp decline in UNSAT percentage, degrading rapidly as perturbation levels increase beyond 0.5m. Critically, both models lose all provable robustness guarantees when perturbation levels exceed 5m, with percentage of provable properties drop to 0%. This establishes a clear operational boundary for safe deployment of these DNN-based power control systems.
[9]
[10]
[11]
[12]
[13] [14] [15]
[16]
[17]
V. C ONCLUSION This work proposed a formal verification framework for DNN-based power allocation in massive MIMO, providing optimality gap guarantee for DNN-based power control against adversarial location perturbations via abstraction-based bounds and feasibility checking. Evaluation results show that the smaller network architecture (fc.small) attains 100% verification success up to 1m while preserving 99% performance. Future works will be extended to verifying different quality of
[18]
[19] [20]
[21]
[22] [23]
E. Björnson, J. Hoydis, L. Sanguinetti, et al., “Massive MIMO networks: Spectral, energy, and hardware efficiency,” Foundations and Trends® in Signal Processing, vol. 11, no. 3-4, pp. 154– 655, 2017. L. Sanguinetti, A. Zappone, and M. Debbah, “Deep learning power allocation in massive MIMO,” in 2018 52nd Asilomar conference on signals, systems, and computers, IEEE, 2018, pp. 1257– 1261. S. Chakraborty, E. Björnson, and L. Sanguinetti, “Centralized and distributed power allocation for max-min fairness in cell-free massive MIMO,” in 2019 53rd Asilomar conference on signals, systems, and computers, IEEE, 2019, pp. 576–580. M. Zaher, Ö. T. Demir, E. Björnson, and M. Petrova, “Learning-based downlink power allocation in cell-free massive MIMO systems,” IEEE Transactions on Wireless Communications, vol. 22, no. 1, pp. 174–188, 2023. T. Van Chien, T. N. Canh, E. Björnson, and E. G. Larsson, “Power control in cellular massive MIMO with varying user activity: A deep learning solution,” IEEE Transactions on Wireless Communications, vol. 19, no. 9, pp. 5732–5748, 2020. X. Zhang, V. A. Le, M. Kaneko, J. C. Lui, and Y. Ji, “Multi-Agent Deep Reinforcement Learningbased Uplink Power Control in Cell-Free Massive MIMO with Mobile Users,” IEEE Transactions on Vehicular Technology, 2025. B. Manoj, M. Sadeghi, and E. G. Larsson, “Adversarial attacks on deep learning based power allocation in a massive MIMO network,” in ICC 2021-IEEE International Conference on Communications, IEEE, 2021, pp. 1–6. P. M. Santos, B. Manoj, M. Sadeghi, and E. G. Larsson, “Universal adversarial attacks on neural networks for power allocation in a massive MIMO system,” IEEE Wireless Communications Letters, vol. 11, no. 1, pp. 67–71, 2021. R. Sahay, M. Zhang, D. J. Love, and C. G. Brinton, “Defending adversarial attacks on deep learning-based power allocation in massive MIMO using denoising autoencoders,” IEEE Transactions on Cognitive Communications and Networking, vol. 9, no. 4, pp. 913–926, 2023. B. Manoj, M. Sadeghi, and E. G. Larsson, “Downlink power allocation in massive MIMO via deep learning: Adversarial attacks and training,” IEEE Transactions on Cognitive Communications and Networking, vol. 8, no. 2, pp. 707–719, 2022. A. Athalye, N. Carlini, and D. Wagner, “Obfuscated gradients give a false sense of security: Circumventing defenses to adversarial examples,” in International conference on machine learning, PMLR, 2018, pp. 274–283. G. Singh, T. Gehr, M. Püschel, and M. Vechev, “An abstract domain for certifying neural networks,” Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, pp. 1–30, 2019. J. Cohen, E. Rosenfeld, and Z. Kolter, “Certified adversarial robustness via randomized smoothing,” in International conference on machine learning, PMLR, 2019, pp. 1310–1320. K. Xu et al., “Automatic perturbation analysis for scalable certified robustness and beyond,” Advances in Neural Information Processing Systems, vol. 33, pp. 1129–1141, 2020. H. Duong, L. Nguyen, T. Le, and T. Nguyen, “Verifying neural network robustness with dual perturbations,” in Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2026, pp. 27 916–27 925. H. Duong, T. Le, L. Nguyen, and T. Nguyen, “Verifying structural robustness of deep neural network,” Proceedings of the ACM on Software Engineering, vol. 3, no. FSE, pp. 1492–1514, 2026. T. Le, H. Duong, T. Nguyen, and T. Matsumura, “Verifying dnn-based semantic communication against generative adversarial noise,” arXiv preprint arXiv:2602.08801, 2026. T. Le and T. Matsumura, “Formal verification for deep learning-based mobile network traffic prediction,” in 2026 International Conference on Artificial Intelligence in Information and Communication (ICAIIC), IEEE, 2026, pp. 246–250. J. Kim, H.-S. Lim, and K. Choi, “Certified Robustness of Antenna Selecting Neural Networks for Massive MIMO Wireless Communications,” IEEE Access, 2025. H. Duong, T. Nguyen, and M. B. Dwyer, “Neuralsat: A high-performance verification tool for deep neural networks,” in International Conference on Computer Aided Verification, Springer, 2025, pp. 409–423. H. Duong, D. Shriver, T. Nguyen, and M. Dwyer, “Compositional neural network verification via assume-guarantee reasoning,” Advances in Neural Information Processing Systems, vol. 38, pp. 64 158–64 182, 2026. H. Duong and T. Nguyen, “Neuralsat: Scaling constraint solving for dnn verification (competition contribution),” in International Symposium on AI Verification, Springer, 2025, pp. 253–259. K. Kaulen et al., “The 6th international verification of neural networks competition (vnn-comp 2025): Summary and results,” arXiv preprint arXiv:2512.19007, 2025.