1 Introduction↩︎

Massive mimo technology is a key component of next-generation wireless networks, designed to accommodate the growing number of connected ue and their diverse demands for new services and applications [1]. By deploying a large number of antennas at the 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 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, , 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 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, , 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 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) 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, high-dimensional 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]–[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 non-linear performance guarantees, , guarantee minimum product of 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 hyper-rectangle input properties. We apply abstraction-based bound-propagation 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, , the optimality gap must fall below a certain threshold, by formulating a constrained program for feasibility analysis.

2 Preliminaries↩︎

2.1 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 signal transmitted by the bs in cell \(j\) is given by \(v_j = \sum_{k=1}^K \mathbf{w}_{jk} u_{jk}\), where \(u_{jk} \in \mathcal{N}(0, \rho_{jk})\) is the data signal in the downlink for ue \(k\) in bs \(l\), with a precoding vector \(w_{jk} \in \mathcal{C}^M\) that determines the transmission beamforming satisfying \(||w_{jk}||^2=1\), thus, \(\rho_{jk}\) is the transmission power. The best precoding schemes that have been adopted by [2] in generating dataset is mmmse. The downlink sinr for ue \(k\) in cell \(j\) is: \[\gamma_{jk} = \frac{\rho_{jk} a_{jk}}{\sum_{l=1}^J \sum_{i=1}^K \rho_{li} b_{lijk} + \sigma^2},\] where \(\sigma^2\) is the awgn variance and the average channel gain is \(a_{jk} = |\mathbb{E}[{\mathbf{w}_{jk}^H \mathbf{h}_{jk}^j}]|^2\) , with \(\mathbf{h}_{jk}^j\) denoting the channel between bs \(j\) and ue \(k\) in cell \(j\). The average interference gain is: \[b_{lijk} = \begin{cases} \mathbb{E}[|\mathbf{w}_{li}^H \mathbf{h}^{l}_{jk}|^2] - |\mathbb{E}[{\mathbf{w}_{li}^H \mathbf{h}^{l}_{jk}}]|^2, \text{ if } (l, i) = (j, k), \\ \mathbb{E}[|\mathbf{w}_{jk}^H \mathbf{h}^{l}_{jk}|^2], \text{ otherwise.} \end{cases}\]

2.2 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: \[\tag{1} \begin{align} \underset{\rho_{jk}: \forall j, k}{\text{maximize}} \quad & \prod_{j=1}^{J} \prod_{k=1}^K \gamma_{jk}, \tag{2} \\ \text{subject to} \quad & \sum_{k=1}^K \rho_{jk} \le P_{\text{max}}, \quad j \in [1, J]. \tag{3} \end{align}\] The problem above seeks to maximize objective in 2 , which is the product of ues’ sinr, while 3 ensures that the allocated power adhere to the maximum power threshold \(P_{max}\) 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].

2.3 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 dataset¹ is provided as \(\{x^{(n)}, \rho^{(n)}\}_{n=1}^{N_T}\), where \(x^{(n)} \in \mathbb{R}^{J \times K \times 2}\) represents an input feature contains location of ues, the output label \(\rho^{(n)} \in [0, \rho_{max}]^{J \times K}\) is the optimal power, and \(N_T\) denotes the size of the dataset. We denote a regression-based dnn model as \(N(.; \theta)\), with \(x\) as the input to the model and the predicted output as \(N(x; \theta) = \rho\), where \(\theta\) constitutes the set of parameters of the model \(N\). The corresponding loss function is represented as \(\mathcal{L}(x, \rho; \theta)\). The goal of the dnn model is to learn the mapping from the ues’ geographical positions, \(x\), to the optimal power allocation solution, \(\rho\) produced by mathematical optimization tools. A feed-forward neural network architecture and 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 \(\rho\) is a vector containing the optimal power solution obtained by solving the power allocation problem (refer to 1 )

2.4 nnv - An Overview↩︎

Given a dnn \(N\) and a property \(\phi\), the general nnv problem asks if \(\phi\) is a valid property of \(N\). Typically, \(\phi\) is a formula of the form \(\phi_{in} \implies \phi_{out}\), where \(\phi_{in}\) is a property over the inputs of \(N\) and \(\phi_{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 \(\phi_{in}\) but violates \(\phi_{out}\). If no such counterexample exists, \(\phi\) is an unsatisfiable property of \(N\) (UNSAT or proven robust); otherwise, satisfiable (SAT).

3 Proposed Verification Framework↩︎

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, , reducing the optimization objective by more than \(\zeta\).

3.1 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 dnn-based power allocation scheme, we define input specifications \(\phi_{in} := [\eta_L, \eta_U]\), such that \(\eta_L\) and \(\eta_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)} + \eta\) to the original input \(x^{(n)}\), where \(\eta \in [\eta_L, \eta_U]\). Similarly, output specifications \(\phi_{out}\) are introduced to capture minimum performance guarantees, requiring that the achieved performance remains at least \(1 -\zeta\) 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.

3.2 DNN Bound Propagation↩︎

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, \theta)\), we analyze its behavior at a nominal input \(x^{(n)}\) subject to a bounded perturbation \(\eta\), where \(x = x^{(n)} + \eta\) and \(x\) lies within an \(l_p\)-norm ball \(\mathcal{B}_p(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 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)} + \eta_L, x^{(n)} + \eta_U]\), along with the trained dnn in vnncomp format [23]. The output is a set of tight bounds \([\rho_L, \rho_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, , 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].

3.3 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: \[\tag{4} \begin{align} \rho_L &\le \rho \le \rho_U, \tag{5} \\ \gamma_{jk} &= \frac{\rho_{jk} a_{jk}}{\sum_{l=1}^J \sum_{i=1}^K \rho_{li} b_{lijk} + \sigma^2}, \tag{6} \\ \prod_{j=1}^J \prod_{k=1}^K \gamma_{jk} &\le (1 - \zeta) \prod_{j=1}^J \prod_{k=1}^K \gamma^{*}_{jk}, \tag{7} \end{align}\] where 5 constrains the power allocation variables \(\rho\) to lie within the bounds \([\rho_L, \rho_U]\) obtained from the dnn bound propagation, 6 defines the sinr \(\gamma_{jk}\) for each ue \(k\) in cell \(j\) based on the power allocation and channel conditions, and 7 encodes the performance guarantee by ensuring that the product of all sinr values does not fall below \((1-\zeta)\) times the optimal product \(\gamma^{*}_{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 \(\zeta\) for all adversarial inputs within \([\eta_L, \eta_U]\). Otherwise, the verification problem is satisfiable (SAT) and there may exist an exploitation.

Since the output bounds \([\rho_L, \rho_U]\) represent an over-approximation, and the feasibility analysis in 4 check for violation in the superset of all possible values of \(\rho\), 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 \([\eta_L, \eta_U]\), then the claim is guaranteed to be true.

4 Evaluation Results↩︎

4.1 Evaluation Setups↩︎

4.1.1 Dataset↩︎

We verify the robustness of the dnn-based power control models for multi-cell massive mimo networks², 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 \times 250\) m. A wrap-around 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 \(\sigma=-94\) dBm. The pilot reuse factor \(\tau_p=1\), and the maximum transmit power per ue is \(20\) dBm.

4.1.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_\infty\)-norm, , the adversarial perturbation constraint is given as \([\eta_L, \eta_U] := [-\eta_0, \eta_0]^{J \times K \times 2}\). The level of perturbation \(\eta_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 \(\zeta\), 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.

4.1.3 Evaluation Metrics↩︎

\(L_1\)-distance between lower and upper output bound: We measure the \(L_1\)-based distance between the lower bound \(\rho_L\) and upper bound \(\rho_U\) computed by abstraction-based nnv [12], [14]. A smaller \(L_1\)-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 \(\zeta\) despite input perturbations within the specified bounds \([\eta_L, \eta_U]\).

4.2 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].

1 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 \(\eta_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 abstraction-based verification more conservative in its bound estimates.

¿tbl:tab:unsat:small? and [tbl:tab:unsat:medium] present the verification success rates for both model architectures across different combinations of perturbation levels \(\eta_0\) and optimality gap requirements \(\zeta\). The general trend reveals that 100% UNSAT rates are consistently achieved when both the perturbation level \(\eta_0\) is sufficiently small and the tolerable optimality gap \(\zeta\) is sufficiently large. The fc.small model consistently exhibits higher verification success rates (\(P_{\text{UNSAT}}\)) compared to fc.medium across most experimental configurations. Particularly for the fc.small model, our verification results guarantee that input perturbations below \(1\)m can maintain 99% of optimal performance (\(\zeta \leq 0.01\)) with 100% confidence.

These guarantees have significant implications for practical network deployment. bs can implement anomaly-detection 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.

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, \(\eta_0 \in [0.1, 10]\) meters, with a fixed optimality gap tolerance of \(\zeta=0.5\%\). The results demonstrate that fc.small maintains a high UNSAT rate for all perturbation levels up to \(1\)m, 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.

5 Conclusion↩︎

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 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.