Paper deep dive
Neural Network Verification for Deep Joint Source-Channel Coding
Thanh Le, Hai Duong, Takeshi Matsumura, ThanhVu Nguyen
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 10/10/2026, 2:48:04 AM
Summary
This paper introduces the first bound-propagation framework for verifying Deep Joint Source-Channel Coding (DeepJSCC) decoders, addressing challenges posed by PReLU activations, transposed convolutions, and Rayleigh fading. The authors extend alpha-Crown for PReLU, substitute transposed convolutions with upsample-then-convolution, and model Rayleigh fading as a structural perturbation. They also apply Lipschitz-regularized global robustness training (GloRo) to improve robustness. Experiments show a 41% reduction in median certified bound and a 10x increase in certified safe cases compared to previous methods, with over-the-air validation on software-defined radio confirming the theoretical bounds.
Entities (9)
Relation Signals (9)
GloRo → appliedto → DeepJSCC
confidence 95% · We also instantiate Lipschitz-regularized global robustness training, denoted GloRo... improving global robustness... of DeepJSCC models
GloRo → improves → Global Robustness
confidence 95% · GloRo, improving global robustness and enabling tight certification
DeepJSCC → operatesover → Rayleigh Fading
confidence 95% · under flat Rayleigh fading assumption... DeepJSCC decoder
DeepJSCC → usescomponent → Transposed Convolution
confidence 95% · the decoder uses transposed convolutions to upsample features
DeepJSCC → usescomponent → PReLU
confidence 95% · The DeepJSCC decoder employs PReLU [21] activations throughout
alpha-CROWN → extendedfor → PReLU
confidence 90% · We extend state-of-the-art techniques for optimization of linear relaxation in DNN verification for PReLU... alpha-Crown
Rayleigh Fading → formulatedas → Structural Perturbation
confidence 90% · formulate Rayleigh fading as a structural perturbation prepended directly into the decoder
Transposed Convolution → replacedby → Upsample-then-Convolution
confidence 90% · replace the transposed convolution with its restricted upsample-then-convolution form
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Deep joint source-channel coding (DeepJSCC) transmits data end-to-end over wireless channels using a neural encoder-decoder, but reconstruction quality can degrade sharply under adversarial perturbations and channel disturbances; no method formally bounds this degradation for DeepJSCC. We present the first bound-propagation framework for verifying DeepJSCC's decoder, bounding worst-case reconstruction error over a given wireless channel's noise region. Current deep neural network (DNN) verifiers do not support three DeepJSCC decoder components: parametric rectified linear activations (PReLU), transposed convolutions, and Rayleigh fading. We extend state-of-the-art techniques for optimization of linear relaxation in DNN verification for PReLU, replace the transposed convolution with its restricted upsample-then-convolution form, and formulate Rayleigh fading as a structural perturbation prepended directly into the decoder, thereby reducing the dimensionality of the verification problem. We also instantiate Lipschitz-regularized global robustness training, denoted GloRo, improving global robustness and enabling tight certification of DeepJSCC models for the first time. On DeepJSCC model for image transmission, this global robustness training procedure combined with structural encoding lowers the median certified bound by up to 41% and certifies about ten times more safe cases (192 against 19) than GloRo with interval encoding at a 10-degree error in channel estimation. Over-the-air validation with an orthogonal frequency-division multiplexing (OFDM) implementation on software-defined radio devices confirm the certificate holds on real hardware, with a worst observed error on radio link at 0.082 against a certified bound of 0.128.
Tags
Links
- Source: https://arxiv.org/abs/2610.11994v1
- Canonical: https://arxiv.org/abs/2610.11994v1
Trouble viewing inline? Open PDF directly →
Full Text
83,107 characters extracted from source content.
Expand or collapse full text
X Month, X Month, X Month, X Month, X Month, X .2026.1234567 Corresponding author: Thanh Le (email: hi@thanhle.xyz). IEEEkeywords Bound propagation, deep joint source-channel coding, Lipschitz robustness, neural network verification, semantic communication, software-defined radio. Neural Network Verification for Deep Joint Source-Channel Coding Thanh Le 1 Hai Duong 2 Takeshi Matsumura 1 and ThanhVu Nguyen 2 Affiliation: Wireless Systems Laboratory, National Institute of Information and Communication Technology, Yokosuka, Kanagawa, Japan Affiliation: George Mason University, Fairfax, VA, USA Abstract Deep joint source-channel coding (DeepJSCC) transmits data end-to-end over wireless channels using a neural encoder-decoder, but reconstruction quality can degrade sharply under adversarial perturbations and channel disturbances; no method formally bounds this degradation for DeepJSCC. We present the first bound-propagation framework for verifying DeepJSCC’s decoder, bounding worst-case reconstruction error over a given wireless channel’s noise region. Current deep neural network (DNN) verifiers do not support three DeepJSCC decoder components: parametric rectified linear activations (PReLU), transposed convolutions, and Rayleigh fading. We extend state-of-the-art techniques for optimization of linear relaxation in DNN verification for PReLU, replace the transposed convolution with its restricted upsample-then-convolution form, and formulate Rayleigh fading as a structural perturbation prepended directly into the decoder, thereby reducing the dimensionality of the verification problem. We also instantiate Lipschitz-regularized global robustness training, denoted GloRo, improving global robustness and enabling tight certification of DeepJSCC models for the first time. On DeepJSCC model for image transmission, this global robustness training procedure combined with structural encoding lowers the median certified bound by up to 41% and certifies about ten times more safe cases (192 against 19) than GloRo with interval encoding at a 10-degree error in channel estimation. Over-the-air validation with an orthogonal frequency-division multiplexing (OFDM) implementation on software-defined radio devices confirm the certificate holds on real hardware, with a worst observed error on radio link at 0.082 against a certified bound of 0.128. 1 Introduction Neural networks can encode and decode wireless transmissions end-to-end, replacing hand-crafted source compression and channel codes with a single trained pipeline [1, 2]. DeepJSCC [2] is the first image transmission model built this way: it trains an encoder-decoder pair jointly to map images to complex channel symbols, adapting to channel quality without a separate compression stage and without retraining for each new noise level. Transformer-based successors such as the Wireless Image Transmission Transformer (WITT) [3] extend this approach to attention mechanisms and rate adaptation, and the broader semantic communication literature treats learned joint source-channel coding as a foundation for next-generation wireless systems [4, 5], where task-oriented, semantically-preserving transmission increasingly replaces strict bit-level fidelity [6, 7]. Such learned systems are being considered for mission-critical scenarios, where the decoder cannot be trusted blindly. Examples include bandwidth-constrained, safety-related image transmission for autonomous vehicles, industrial Internet of Things (IoT) sensing, and comparable applications [5, 7]. A corrupted reconstruction can propagate into a wrong downstream decision, e.g., an autonomous vehicle misjudging an obstacle from a degraded camera image, or an industrial controller acting on a misread sensor image [5, 8]. The worst-case behavior of a hand-crafted codec under channel noise is explicitly defined and can be systematically characterized. In contrast, the behavior of a DNN decoder is not explicitly bounded: the DeepJSCC training objective does not constrain how much reconstruction quality may degrade for channel realizations outside the training set, but only optimizes average performance over observed ones. This gap presents a specific reliability concern, e.g., for a deployed DeepJSCC receiver, it is important to determine the extent to which reconstruction quality may degrade under a specified channel disturbance. Evaluating DeepJSCC models using finite-sample testing, which is the standard practice [2, 3], can reveal individual failures but does not provide bounds on the worst-case performance across the full range of possible channel realizations. Similar to conventional software testing, this approach can demonstrate the presence of faults but cannot guarantee their absence. Neural network verification (NNV) can prove absence instead of merely searching for presence of these adversarial inputs. Bound-propagation verifiers [9, 10, 11, 12] compute a certified interval on a network’s own output, e.g., the logit range for a classifier, guaranteed to hold for every input in a specified region simultaneously, without enumerating individual inputs. State-of-the-art NNV tools now scale to networks with millions of parameters [13, 14, 15] with solvers such as DeepPoly [11], α-Crown [12, 16], and interval bound propagation (Ibp) [9] covering various DNN architectures from image classifiers to aircraft collision-avoidance controllers [17]. Recent research has extended formal certification methods to wireless systems. [18] [18] certified an antenna-selection network for massive multiple-input multiple-output (MIMO) systems, our previous works verified a mobile-traffic regression model [19] and a power-control policy network [20]. However, no formal verification framework currently exists for the DeepJSCC decoder under physical wireless channel models. Despite these advancements, existing bound-propagation tools cannot verify the DeepJSCC decoder in its current form. Three specific challenges hinder progress in this area. First, the DeepJSCC decoder employs PReLU [21] activations throughout, allowing each layer to learn a small negative-side slope rather than fixing it at zero. Current verification tools support Rectified Linear Unit (ReLU) activations but not PReLU. Replacing PReLU with ReLU reduces reconstruction quality by up to two decibels (§5.2). Second, the decoder uses transposed convolutions to upsample features, a function not natively supported by α-Crown [12]. Naively replacing them alters the network. Last but not least, under flat Rayleigh fading assumption, each latent symbol acquires the same residual phase rotation remaining after amplitude equalization at the receiver, in addition to independent additive noise [22]. Standard interval encoding treats each latent coordinate as an independently. Consequently, interval’s widths increase with phase uncertainty for each coordinate, despite a single shared rotation affecting all symbols simultaneously. Structured-perturbation verification [23, 24] demonstrates that bounding the generators of a perturbation, rather than its per-coordinate effects, produces significantly tighter certificates. This principle is adapted to the fading channel in the following section. In this paper, we introduce the first bound-propagation framework for the formal verification of DeepJSCC’s decoder, addressing all three challenges while maintaining the reconstruction quality for which DeepJSCC was originally trained. The primary contributions of this paper are: • PReLU relaxation. We extend the optimization of linear relaxation α-Crown to encompass the feasible relaxation slopes of PReLU (§4.1). The standard ReLU relaxation emerges as a special case when the learned negative-side slope is zero. Our derivation generalizes this scenario without loss and preserves the 1.781.78 to 2.222.22 dB of peak signal-to-noise ratio (PSNR) that would otherwise be lost by substituting ReLU. • Upsample-then-convolution substitution. We show that nearest-neighbor upsampling followed by convolution is a restricted transposed convolution (Prop. 3), and the retrained decoder loses no more than 0.350.35 dB of PSNR (§5.2). • Structural Rayleigh input property. We introduce the fading transform as a linear layer and directly bound its two real coordinates. This approach reduces the verifier’s fading input from 2k2k per-symbol intervals to only 22 degrees of freedom of a single complex block fading coefficient(§4.3). • GloRo instantiation for DeepJSCC. We apply GloRo Lipschitz regularization [25] to DeepJSCC’s decoder, providing a closed-form radius under both additive white Gaussian noise (AWGN) and Rayleigh fading. This enables Lipschitz-aware fine-tuning from a pretrained checkpoint (§4.4). This work aligns with efforts that train networks to facilitate verification [26], specialized to a channel-dependent radius. Experiments on DeepJSCC model [2] show that GloRo training drops the large decoder’s Lipschitz constant from 215.6215.6 to 25.525.5, which makes it certifiable for the first time: the upper bound of mean absolute error (MAE) falls from above 11 at every signal-to-noise ratio (SNR) to 0.080.08. Structural encoding lowers the median certified bound by up to 41%41\% across model sizes, from 0.460.46 to 0.270.27 on large. At the widest phase uncertainty we test (δ=10∘δ=10 ), the full pipeline certifies 192192 safe cases against 1919 for GloRo training with interval encoding alone, a 10×10× gain. Over-the-air tests on two ADALM-PlutoSDR transceivers confirm the certificate on real hardware: across the ten CIFAR-10 classes the worst observed error is 0.0820.082, against a certified bound of 0.1280.128. 2 Preliminaries 2.1 DeepJSCC System Model We consider image transmission over a bandwidth-limited wireless channel, as shown in Fig. 1. The transmitter sends an input image x∈ℝnx ^n to the receiver by mapping x to a complex-valued channel input symbol s∈ℂks ^k. This mapping is the encoder ℰ:ℝn→ℂkE:R^n ^k in Fig. 1, following the DeepJSCC design [2]. The input size n is typically much larger than the compressed representation size k; following the literature on DeepJSCC, we call the ratio k/nk/n the bandwidth compression ratio. The encoder normalizes s to satisfy an average power constraint, which the communication protocol imposes to avoid interference with other transmissions: 1k[s∗s]≤P 1kE[s*s]≤ P (1) The encoder itself is a sequence of neural network layers: convolutional neural network (CNN) layers, PReLU activations, and a final normalization layer that enforces the power constraint. CNN layers extract image features and reduce them to a compact representation, the complex channel input, while PReLU activations let the encoder learn a non-linear mapping from the source image to the coded wireless signal space. InputxxEncoderℰEPowerNorm.DecoderDOutputx xs sTXRXADALM-PlutoSDR, over the air Fig. 1: The DeepJSCC system model to be analyzed. The wireless channel in Fig. 1 carries s to the receiver, corrupting the symbols with random noise. The receiver maps the corrupted channel output s^∈ℂk s ^k back to an approximate reconstruction x^∈ℝn x ^n of the original image; this mapping is the decoder :ℂk→ℝnD:C^k ^n in Fig. 1. The decoder mirrors the encoder. A stack of transposed convolutional layers with PReLU activations inverts the encoding. A final sigmoid layer then maps the output to [0,1][0,1] before rescaling it to the pixel range. To recover a clean image, the decoder must also denoise the artifacts introduced by the channel. Together, the encoder, channel, and decoder form a joint source-channel coding model: the encoder and decoder are trained jointly, while the channel is a differentiable, non-trainable layer that connects them during training. Under AWGN, it applies s^=s+n s=s+n with n∼(0,σ2I)n (0,σ^2I). Under slow Rayleigh fading, the channel instead applies s^=hs+n s=hs+n, where h is the residual the receiver’s channel estimator leaves rather than the raw fading coefficient. Equalizing by an estimate h h that is accurate in amplitude leaves the unit-modulus rotation h=ejθh=e^jθ with |θ|≤δ|θ|≤δ, where δ is the phase accuracy the estimator guarantees [22]. We assume amplitude equalization is exact, so |h|=1|h|=1 and only the residual phase is unknown. DeepJSCC evaluates quality by PSNR between x and x x, computed from the mean squared error (MSE): PSNR(x,x^) (x, x) =10log10(xmax2MSE(x,x^)), =10 _10\! ( x_ ^2MSE(x, x) ), (2) MSE(x,x^) (x, x) =1n∑i=1n(xi−x^i)2, = 1n _i=1^n(x_i- x_i)^2, (3) where xmaxx_ is the maximum possible pixel value. 2.2 Neural Network Verification The channel corrupts the latent symbols before decoding, resulting in a lower-quality reconstruction of the original message (e.g., an image). Neural network verification can quantify how much this quality can degrade under a given noise range, providing a useful certificate, e.g., a proof that a minimum quality is always achieved. Formally, consider a DNN N and a property ϕφ of the form ϕin→ϕout _in→ _out over the inputs and outputs of N. The DNN verification problem asks whether ϕφ is valid for N. Bound-propagation methods [9, 11, 12] solve this problem by over-approximating each layer. These methods are incomplete: if the over-approximation still satisfies ϕφ, the property is proven; otherwise the verifier returns unknown, even when the true network may satisfy ϕφ. In contrast, complete verifiers based on satisfiability modulo theories (SMT) solving [17], mixed-integer programming [27], branch-and-bound [28], or DPLL(t) [29] decide ϕφ exactly: given enough time, they either prove the property or produce a genuine counterexample. Complete verifiers often use fast incomplete bound propagation as a subroutine to prune branches [16, 28, 29]. 2.3 Bound Propagation Bound propagation computes a sound interval [y¯,y¯][ y, y] on the output objective y of N over an input region ϕin _in. In this paper, ϕin _in is an interval on the latent channel symbols. The main bound-propagation methods form a precision-cost trade-off. Ibp [9] is fastest and loosest. DeepPoly [11, 10] back-substitutes linear relaxations in one pass. α-Crown [12] further tunes the relaxation slopes by gradient descent, which is slower but yields the tightest bounds among incomplete verifiers. 2.3.1 Interval bound propagation Ibp [9] maintains only a concrete interval at each layer, starting from the input interval ϕin=[x¯,x¯] _in=[ x, x]. Consider an affine layer z=Wx+bz=Wx+b with incoming bounds x∈[x¯,x¯]x∈[ x, x]. The pre-activation bounds are z¯ z =W+x¯+W−x¯+b, =W^+ x+W^- x+b, (4) z¯ z =W+x¯+W−x¯+b, =W^+ x+W^- x+b, where W+=max(W,0)W^+= (W,0) and W−=min(W,0)W^-= (W,0) are taken elementwise. The sign split is required: a negative weight reverses which endpoint of [x¯,x¯][ x, x] yields the minimum or maximum of that term. For z^=ReLU(z) z=ReLU(z) with z∈[z¯,z¯]z∈[ z, z], monotonicity gives z¯^=ReLU(z¯),z^¯=ReLU(z¯). z=ReLU( z), z=ReLU( z). (5) Ibp applies (4)–(5) layer by layer to the output. Each step is fast but discards correlations among layer outputs. Fig. 2visualizes (5) at one unstable ReLU: the interval keeps only the endpoints z¯^=ReLU(z¯)=0 z=ReLU( z)=0 and z^¯=ReLU(z¯)=z¯ z=ReLU( z)= z, so the admissible (z,z^)(z, z) pairs form the entire interval region [z¯,z¯]×[z¯^,z^¯][ z, z]×[ z, z] (shaded), which is the over-approximation area and discards the relation between z and z z. The bounds therefore widen and often become vacuous on deep networks. z z(z¯,0)( z,0)(z¯,z¯)( z, z)z¯ zz¯ zz^¯ zz¯^=0 z=0 Fig. 2: Interval bound propagation through an unstable ReLU over [z¯,z¯][ z, z]. 2.3.2 Linear relaxation Linear relaxation is tighter bound propagation methods by bounding each layer’s pre-activation z(l)z^(l) by affine functions of the network inputs x: A¯(l)x+b¯(l)≤z(l)≤A¯(l)x+b¯(l). A^(l)x+ b^(l)\;≤\;z^(l)\;≤\; A^(l)x+ b^(l). (6) Affine and convolutional layers compose these bounds exactly. A ReLU layer requires a local over-approximation. Consider a ReLU layer with pre-activation z∈[z¯,z¯]z∈[ z, z], where z¯<0<z¯ z<0< z, and output z^=ReLU(z) z=ReLU(z). The layer is stable if z¯≥0 z≥ 0 (always active) or z¯≤0 z≤ 0 (always inactive): then the map is exact and needs no relaxation. An unstable ReLU is over-approximated by two linear functions (Fig. 3). The tightest upper bound is the line through (z¯,0)( z,0) and (z¯,z¯)( z, z): z^≤d¯z+b¯,d¯=z¯z¯−z¯,b¯=−z¯z¯z¯−z¯. z\;≤\; dz+ b, d= z z- z, b=- z z z- z. (7) The lower bound is any line z^≥αz z≥α z with α∈[0,1]α∈[0,1]. In Fig. 3, the solid blue line is the upper bound (7) and the thick dashed red line is the lower bound for one such α; the arrow shows that α can rotate this line anywhere between the thin dashed lines α=0α=0 and α=1α=1. The shaded region is the over-approximation area for the drawn α, and its shape depends on α. DeepPoly picks an endpoint α=0α=0 or α=1α=1 to minimize the over-approximated area (shaded in blue). z z(z¯,0)( z,0)(z¯,z¯)( z, z)z¯ zz¯ zz¯ zupperα=0α=0α=1α=1lowerα∈[0,1]α∈[0,1] Fig. 3: Linear relaxation of an unstable ReLU over [z¯,z¯][ z, z] with lower slope α∈[0,1]α∈[0,1]. 2.3.3 Back-substitution and concretization Back-substitution is the procedure DeepPoly uses to eliminate intermediate layers: it repeatedly replaces each intermediate layer’s variable by its lower or upper affine bound (6) until the resulting bound depends only on x. Concretization then evaluates the linear forms over ℬB: z¯(l) z^(l) =minx∈ℬ(A¯(l)x+b¯(l)), = _x \;( A^(l)x+ b^(l)), (8) z¯(l) z^(l) =maxx∈ℬ(A¯(l)x+b¯(l)). = _x \;( A^(l)x+ b^(l)). For an ℓp _p ball ℬ=x:‖x−x0‖p≤εB=\x:\|x-x_0\|_p≤ \, Hölder’s inequality [28] gives the closed form z¯(l) z^(l) =A¯(l)x0+ε‖A¯(l)‖q+b¯(l), = A^(l)x_0+ \| A^(l)\|_q+ b^(l), (9) z¯(l) z^(l) =A¯(l)x0−ε‖A¯(l)‖q+b¯(l), = A^(l)x_0- \| A^(l)\|_q+ b^(l), where 1p+1q=1 1p+ 1q=1. The resulting bound [z¯(l),z¯(l)][ z^(l), z^(l)] decide the neuron stability and the linear relaxation in the next layers. 2.3.4 Optimization of linear bound α-Crown treats the lower slopes α as trainable parameters in [0,1][0,1]. It optimizes them by gradient descent on the certified output bound. Alg. 1 summarizes the procedure for an L-layer network that alternates an affine map and a ReLU at each layer l=1,…,Ll=1,…,L. DeepPoly is the special case with T=0T=0 and a heuristic α∈0,1α∈\0,1\. Alg. 1 α-Crown bound propagation input : L-layer network with affine maps W(l),b(l)l=1L\W^(l),b^(l)\_l=1^L and ReLU layers; input ball ℬ=x:‖x−x0‖p≤εB=\x:\|x-x_0\|_p≤ \; iterations T; step size η output : output bounds [z¯(L),z¯(L)][ z^(L), z^(L)] 1 Compute layer intervals [z¯(l),z¯(l)][ z^(l), z^(l)] for l=1,…,Ll=1,…,L by Ibp (5) 2 Initialize slopes α(l)∈[0,1]α^(l)∈[0,1] for each unstable ReLU 3 for t←1t← 1 to T do 4 for l←1l← 1 to L do 5 (A¯,b¯),(A¯,b¯)←(I,0),(I,0)( A, b),( A, b)←(I,0),(I,0) 6 for k←lk← l to 11 by −1-1 do 7 (d¯(k),b¯(k),α(k))←Relax(z¯(k),z¯(k),α(k))( d^(k), b^(k),α^(k)) ( z^(k), z^(k),α^(k) ) 8 (A¯,b¯),(A¯,b¯)←Combine(d¯(k),b¯(k),α(k),(A¯,b¯),(A¯,b¯))( A, b),( A, b) ( d^(k), b^(k),α^(k),( A, b),( A, b) ) 9 (A¯,b¯)←(A¯W(k),A¯b(k)+b¯)( A, b)←( A\,W^(k), A\,b^(k)+ b) 10 (A¯,b¯)←(A¯W(k),A¯b(k)+b¯)( A, b)←( A\,W^(k), A\,b^(k)+ b) 11 z¯(l),z¯(l)←Concretize((A¯,b¯),(A¯,b¯)) z^(l), z^(l) (( A, b),( A, b) ) (9) 12 α←Project[0,1](α+η∇αz¯(L))α _[0,1] (α+η _α z^(L) ) 13 return [z¯(L),z¯(L)][ z^(L), z^(L)] The algorithm first obtains one interval per layer with Ibp. Each iteration visits layers l=1,…,Ll=1,…,L (Alg. 1). For layer l, it back-substitutes from layer k=lk=l down to 11 (Alg. 1–Alg. 1). At each k, RelaxRelax turns the ReLU bounds [z¯(k),z¯(k)][ z^(k), z^(k)] and slope α(k)α^(k) into the upper line (d¯(k),b¯(k))( d^(k), b^(k)) of Fig. 3, and CombineCombine folds (d¯(k),b¯(k),α(k))( d^(k), b^(k),α^(k)) into the running coefficients (A¯,b¯),(A¯,b¯)( A, b),( A, b) by the sign of each entry, before the affine map (W(k),b(k))(W^(k),b^(k)) is applied. ConcretizeConcretize (Alg. 1) then evaluates the resulting linear form over ℬB to yield the layer interval via (9). A projected gradient step (Alg. 1) updates the slopes α to tighten the output bound. Optimizing α improves on fixed DeepPoly at the cost of T full backward passes. 2.4 Lipschitz-Certified Training Bound propagation formally evaluates a trained model: it certifies how much the output can change under a given input perturbation. It does not change the model weights, so it cannot by itself improve robustness. We therefore complement verification with GloRo-style training [25], which builds robustness into the network during learning. Definition 1 (Lipschitz constant). A function N is Lipschitz continuous with constant K (w.r.t. a chosen norm) if ‖N(x)−N(x′)‖≤K‖x−x′‖for all inputs x,x′.\|N(x)-N(x )\|\;≤\;K\|x-x \| all inputs $x,x $. (10) The smallest such K is the Lipschitz constant of N. Intuitively, K is a global sensitivity: it upper-bounds how fast the output can change when the input moves. If ‖x−x′‖≤ε\|x-x \|≤ , then (10) gives ‖N(x)−N(x′)‖≤Kε\|N(x)-N(x )\|≤ K everywhere, not only near one test point. A small K therefore quantifies global robustness of the DNN: no pair of inputs within distance ε can produce an output gap larger than KεK . Definition 2 (Lipschitz constant of a DNN). For an L-layer network, GloRo upper-bounds K by the product of per-layer Lipschitz constants: K≤∏l=1LK(l),K\;≤\; _l=1^LK^(l), (11) where K(l)=‖W(l)‖2K^(l)=\|W^(l)\|_2 (the spectral norm) for an affine or convolutional layer, and K(l)K^(l) is the activation’s Lipschitz constant for a ReLU or PReLU layer: 11 for ReLU, and max(1,|a|) (1,|a|) for PReLU with negative slope a. Spectral norms are estimated during training by power iteration, which approximates ‖W(l)‖2\|W^(l)\|_2 by repeatedly multiplying a random unit vector by W(l)⊤W(l)W^(l) W^(l) until convergence. GloRo regularizes K directly during training: it adds a penalty term on K to the loss function, such that gradient descent shrinks the DNN’s global sensitivity. ℒGloRo(θ)=ℒ(θ)+λg(K),L_GloRo(θ)\;=\;L(θ)\;+\;λ\,g(K), (12) for loss function ℒL, a regularization weight λ, and a monotonically increasing penalty g on K. 3 Problem Formulation This section formulates DeepJSCC verification as the DNN verification problem with an input property on the latent symbols and an output property on the reconstruction quality. 3.1 Input Property Definition 3 (Input property). Let s∈ℂks ^k be the transmitted latent symbols and let s^∈ℂk s ^k be the symbols that the decoder receives. Let ‖z‖∞:=max(|Re(z)|,|Im(z)|)\|z\|_∞:= (|Re(z)|,|Im(z)|). The input property ϕin _in is an interval around each symbol of s s: ϕin=s^:∥s^i−ci∥∞≤ri,i=1,…,k, _in\;=\; \ s:\| s_i-c_i\|_∞≤ r_i,\ i=1,…,k \, (13) for a center c∈ℂkc ^k and radius r∈ℝ≥0kr _≥ 0^k that depend on channel assumptions. AWGN channel. Under AWGN, s^=s+n s=s+n with n∼(0,σ2I)n (0,σ^2I). The AWGN standard deviation on each axis of n depends on the channel SNR γ (in dB): σ(γ)=12⋅10γ/10.σ(γ)= 12· 10^γ/10. (14) Let κ be the number of standard deviations the interval extends on each axis, e.g., κ=3κ=3 covers about 99.7%99.7\% of the AWGN noise mass per axis, not jointly over all 2k2k axes. Finally, the parameter for input property are: c=s,r=κσ(γ).c=s, r=κσ(γ). (15) Rayleigh channel. We assume slow fading, the regime where h stays effectively constant over one packet’s transmission. Under this assumption, s^=hs+n s=hs+n where h denotes the residual fading after imperfect channel estimation and equalization, e.g., h=ejθh=e^jθ, |θ|≤δ|θ|≤δ. The input domain for h is the arc ϕhδ=ejθ:|θ|≤δ _h^δ=\e^jθ:|θ|≤δ\. The reachable set hsi\hs_i\ is the arc of radius |si|=Re(si)2+Im(si)2|s_i|= Re(s_i)^2+Im(s_i)^2 that sis_i sweeps as it rotates through ±δ±δ. DNN verifiers take intervals as inputs, so we bound the reachable set hsi\hs_i\ by an interval around sis_i; Prop. 1 below shows this bound is sound, i.e., it never excludes a value hsihs_i that some h∈ϕhδh∈ _h^δ can actually produce. Proposition 1 (Residual fading interval is sound). For h=ejθh=e^jθ with |θ|≤δ|θ|≤δ and δ∈[0,π]δ∈[0,π], ‖hsi−si‖∞≤ 2sin(δ2)|si|.\|hs_i-s_i\|_∞\;≤\;2 ( δ2 )|s_i|. Proof. |h−1|2=(cosθ−1)2+sin2θ=2−2cosθ=4sin2(θ2)|h-1|^2=( θ-1)^2+ ^2θ=2-2 θ=4 ^2( θ2), so |h−1|=2|sin(θ2)||h-1|=2| ( θ2)|. Since |θ|≤δ≤π|θ|≤δ≤π and sin is increasing on [0,π2][0, π2], |h−1|≤2sin(δ2)|h-1|≤ 2 ( δ2). Hence |hsi−si|=|h−1||si|≤2sin(δ2)|si||hs_i-s_i|=|h-1|\,|s_i|≤ 2 ( δ2)|s_i|, and ‖hsi−si‖∞≤|hsi−si|\|hs_i-s_i\|_∞≤|hs_i-s_i| since ‖z‖∞≤|z|\|z\|_∞≤|z| for every z∈ℂz . ∎ Centering the interval at sis_i and adding the κσ(γ)κσ(γ) noise interval for nin_i gives the Rayleigh input property: ci=si,ri=2sin(δ2)|si|+κσ(γ).c_i=s_i, r_i=2 ( δ2 )|s_i|+κσ(γ). (16) Unlike the AWGN, the radius varies per transmitted symbol, and the fading term 2sin(δ2)|si|2 ( δ2)|s_i| does not shrink with SNR. 3.2 Output Property An output property need to that reflects reconstruction quality, yet bound-propagation verifiers only certify a scalar bound on a linear transformation of the network’s output. DeepJSCC’s natural quality metric, PSNR Eq. 2 and MSE Eq. 3, does not fit that requirement as they are nonlinear. We therefore bound the network’s output by MAEMAE. Definition 4 (Output property). For a threshold τ>0τ>0 and clean image x∈ℝnx ^n, the output property ϕout _out holds for a reconstruction x x if MAE(x,x^)=1n∑i=1n|xi−x^i|≤τ.MAE(x, x)\;=\; 1n _i=1^n|x_i- x_i|\;≤\;τ. (17) For a scalar residual r=xi−x^ir=x_i- x_i, the exact identity hold: |r|=ReLU(r)+ReLU(−r)|r|\;=\;ReLU(r)+ReLU(-r) (18) Particularly, if r≥0r≥ 0, ReLU(r)+ReLU(−r)=r+0=|r|ReLU(r)+ReLU(-r)=r+0=|r|; if r<0r<0, ReLU(r)+ReLU(−r)=0+(−r)=|r|ReLU(r)+ReLU(-r)=0+(-r)=|r|. MAEMAE is therefore exactly representable with the ReLU primitives our bound propagation already supports [23]. The property is safe if no input in ϕin _in violates ϕout _out. Bound propagation certifies an interval [y¯,y¯][ y, y] on the output objective y=MAE(x,x^)y=MAE(x, x) over every s^∈ϕin s∈ _in. If the over-approximation satisfies ϕout _out, e.g., y¯≤τ y≤τ, the result is safe. 3.3 Verification Framework ϕin _inon s sDecoderD[x¯^,x^¯][ x, x]clean imagexxMAEMAEvia (18)[lb,ub][lb,ub]ub≤τub\!≤\!τ?safeunknownyesno Fig. 4: The verification framework for DeepJSCC. Fig. 4shows the verification framework for the receiver of DeepJSCC. Bound propagation carries the input property ϕin _in through the decoder D to a certified interval on the reconstruction denotes [x¯^,x^¯][ x, x]. It then compares that interval against the clean image x via the two-ReLU MAEMAE identity (18). The result is a certified interval [y¯,y¯][ y, y] on y=MAE(x,x^)y=MAE(x, x). The final check against the output property ϕout _out (Def. 4) follows §2.2: y¯≤τ y≤τ returns safe, otherwise unknown. 4 Propose Approach We make DeepJSCC verifiable and certifiably robust with four contributions: a sound PReLU relaxation that extends α-Crown to DeepJSCC’s activations (§4.1), a transposed-convolution replacement that α-Crown supports natively (§4.2), a structural Rayleigh input property that exposes h to bound propagation (§4.3), and a GloRo instantiation with a closed-form radius for both channels (§4.4). 4.1 PReLU Relaxation with an Auto-Tuned Slope DeepJSCC uses PReLU activations for every layer except the final sigmoid output layer, to learn a non-linear mapping from the source signal space to the coded signal space [2]. PReLU generalizes ReLU by learning the negative-side slope a instead of fixing it at 00. Definition 5 (Parametric ReLU). For a pre-activation z∈ℝz and a layer’s learned negative-side slope a, PReLU(z)=z,z≥0,az,z<0.PReLU(z)= casesz,&z≥ 0,\\ az,&z<0. cases (19) Every PReLU layer in the encoder and decoder shares one such a. This single extra parameter per layer improves accuracy over ReLU at negligible computational cost [21]. DeepPoly’s ReLU relaxation (§2.3) assumes a lower-bound feasible interval of [0,1][0,1]: any slope α∈[0,1]α∈[0,1], including the endpoint α=0α=0, gives a sound lower bound z^≥αz z≥α z on ReLU’s output. Once the layer’s learned slope a>0a>0, reusing ReLU’s linear relaxation is unsound because if z<0z<0 the true PReLU output is z^=az<0 z=az<0. This, ReLU’s relaxation cannot simply be reused as-is. z z(z¯,az¯)( z,a z)(z¯,z¯)( z, z)z¯ zz¯ zz¯ zupperslope aaslope 11lowerslope ∈[a,1]∈[a,1] Fig. 5: Linear relaxation of an unstable PReLU over [z¯,z¯][ z, z] with learned slope a. PReLU is piecewise-linear but non-linear at the origin, so we over-approximate an unstable PReLU neuron with two linear functions over the pre-activation interval z∈[z¯,z¯]z∈[ z, z]. This keeps back-substitution exact linear algebra. Fig. 5 shows the resulting wedge, the PReLU counterpart of Fig. 3. The upper bound is the line through (z¯,az¯)( z,a z) and (z¯,z¯)( z, z). The lower bound is again a line through the origin but its feasible slopes stay within [a,1][a,1]. In Fig. 5, the solid blue line is the upper bound (20), the thick dashed red line is the lower bound for one slope in the feasible interval [a,1][a,1], the arrow shows that this slope can rotate anywhere between the thin dashed lines of slope a and slope 11, and the shaded region is the over-approximation area for the drawn slope. Definition 6 (PReLU relaxation). Let z∈[z¯,z¯]z∈[ z, z] and z^=PReLU(z) z=PReLU(z). If z¯≥0 z≥ 0 or z¯≤0 z≤ 0, the neuron is stable and z^=z z=z or z^=az z=az exactly, with no relaxation. Otherwise (z¯<0<z¯ z<0< z), for every α∈[0,1]α∈[0,1], (a+α(1−a))z≤z^≤d¯z+b¯, (a+α(1-a) )z\;≤\; z\;≤\; dz+ b, (20) d¯=z¯−az¯z¯−z¯,b¯=az¯−d¯z¯. d= z-a z z- z, b=a z- d z. Setting a=0a=0 in Eq. 20 gives exactly ReLU’s line z^≤d¯z+b¯ z≤ dz+ b (7) and lower family z^≥αz z≥α z, α∈[0,1]α∈[0,1]: a nonzero a only rescales that same α onto [a,1][a,1] instead of [0,1][0,1]. So Eq. 20 is a drop-in replacement for RelaxRelax at Alg. 1 of Alg. 1 wherever that algorithm reaches a PReLU layer. α-Crown still treats α as trainable, projected onto [a,1][a,1]. A bound is sound if it is guaranteed to contain the true value: a sound interval [y¯,y¯][ y, y] satisfies y¯≤y≤y¯ y≤ y≤ y for every value y the network can actually produce, even if [y¯,y¯][ y, y] is wider than necessary. Soundness is what makes a certificate trustworthy [30]: an unsound bound could silently miss a bad case, the way an underestimated link margin could silently miss an outage. ReLU’s relaxation is sound over α∈[0,1]α∈[0,1]; Prop. 2 establishes the guarantee for PReLU. Proposition 2 (PReLU relaxation soundness). For z¯<0<z¯ z<0< z, a≤1a≤ 1, z∈[z¯,z¯]z∈[ z, z], and α∈[0,1]α∈[0,1] we have (a+α(1−a))z≤PReLU(z)≤d¯z+b¯, (a+α(1-a) )z\;≤\;PReLU(z)\;≤\; dz+ b, where d¯=z¯−az¯z¯−z¯ d= z-a z z- z and b¯=az¯−d¯z¯ b=a z- d z. Proof. Write d=a+α(1−a)∈[a,1]d=a+α(1-a)∈[a,1]. If z<0z<0, then dz≤az=PReLU(z)dz≤ az=PReLU(z) since d≥ad≥ a. If z≥0z≥ 0, then dz≤z=PReLU(z)dz≤ z=PReLU(z) since d≤1d≤ 1. If z<0z<0, then PReLU(z)=az≤d¯z+b¯PReLU(z)=az≤ dz+ b because az≤d¯z+b¯⇔z¯(a−1)(z−z¯)≤0az≤ dz+ b z(a-1)(z- z)≤ 0, which holds since z¯>0 z>0, a≤1a≤ 1, and z≥z¯z≥ z. If z≥0z≥ 0, then PReLU(z)=z≤d¯z+b¯PReLU(z)=z≤ dz+ b because z≤d¯z+b¯⇔(1−a)z¯(z¯−z)≤0z≤ dz+ b (1-a) z( z-z)≤ 0, which holds since z¯<0 z<0, a≤1a≤ 1, and z≤z¯z≤ z. ∎ The endpoints α∈0,1α∈\0,1\ also cover the stable cases of Def. 6 (d=ad=a and d=1d=1). Setting a=0a=0 recovers ReLU’s line and feasible interval [0,1][0,1], so Prop. 2 strictly generalizes DeepPoly’s ReLU soundness. 4.2 Substituting Transposed Convolution with Upsampling The decoder in [2] decode the latent symbols with transposed convolutional layers, each layer doubling the spatial resolution until the output matches the source image. Transposed convolution’s output-to-input map is transposed and fractionally strided, a sparsity pattern ordinary convolution does not share, so it needs its own linear-relaxation rule. Even ordinary convolution never forms this matrix explicitly, since it would not fit in a commercial graphics processing unit (GPU)’s memory; α-Crown [12] propagates bounds through the convolution’s own patch representation. A transposed-convolution relaxation would need an analogous patch-mode rule on top of the relaxation itself, which is a difficult engineering task. We substitute every decoder transposed convolution with nearest-neighbor upsampling followed by an ordinary convolution, both operations our bound propagation handles exactly or near-exactly. Prop. 3 below shows the substitution stays within the same operator family, stated in one spatial dimension with one channel; the two-dimensional multi-channel case applies the same identity per index and channel. Let (u∗v)[n]=∑ju[j]v[n−j](u v)[n]= _ju[j]v[n-j] denote convolution. Definition 7 (Transposed convolution). The stride-s transposed convolution of an input x with kernel w is y[n]=∑mx[m]w[n−sm].y[n]\;=\; _mx[m]w[n-sm]. (21) Each input entry x[m]x[m] places a copy of the kernel at position smsm, so the output resolution grows by a factor of s. Definition 8 (Upsample-then-convolution). Nearest-neighbor upsampling by s copies each entry s times: xup[j]=x[⌊j/s⌋]x_up[j]=x[ j/s ]. Convolution with kernel v then follows: y=xup∗v.y\;=\;x_up v. (22) Proposition 3 (Upsample-then-convolution is a transposed convolution). For every kernel v, nearest-neighbor upsampling by s followed by convolution with v equals the stride-s transposed convolution with kernel w=s∗vw=1_s v, where s1_s is the all-ones kernel of length s. Proof. Let x0x_0 insert s−1s-1 zeros between entries: x0[j]=x[j/s]x_0[j]=x[j/s] if s divides j and x0[j]=0x_0[j]=0 otherwise. First, (x0∗w)[n]=∑jx0[j]w[n−j]=∑mx[m]w[n−sm](x_0 w)[n]= _jx_0[j]w[n-j]= _mx[m]w[n-sm], which is (21): convolving the zero-inserted input is exactly the stride-s transposed convolution. Second, xup=x0∗sx_up=x_0 1_s: entry j of x0∗sx_0 1_s sums x0[j−i]x_0[j-i] over 0≤i<s0≤ i<s, and the only multiple of s among j−s+1,…,j-s+1,…,j is s⌊j/s⌋s j/s , leaving x[⌊j/s⌋]x[ j/s ]. By associativity, xup∗v=(x0∗s)∗v=x0∗(s∗v)x_up v=(x_0 1_s) v=x_0 (1_s v), the stride-s transposed convolution with kernel s∗v1_s v. ∎ By Prop. 3, the substituted layer produces the same output shape and stays in the same operator family as the transposed convolution it replaces. We empirically confirm this substitution preserves DeepJSCC’s reconstruction performance (§5). 4.3 Structural Perturbation of Fading Residual Interval The Rayleigh interval (16) is sound but loose: each per-symbol radius ri=2sin(δ2)|si|+κσ(γ)r_i=2 ( δ2)|s_i|+κσ(γ) is derived from h’s worst case for that symbol alone, though all k symbols share one residual h. The true reachable set is therefore a one-dimensional curve inside ℝ2kR^2k, yet the per-symbol interval inflates it to a full 2k2k-dimensional hypercube. Recent work on structured-perturbation verification [23, 24] argues that whenever a perturbation is generated by fewer degrees of freedom than the space it inhabits, the verifier should reason over the generators directly. Prepending the generative map as a DNN layer and bounding only the low-dimensional input then lets bound propagation track the structural constraint exactly, without inter-coordinate slack. §2.1 already states the exact channel formula s^=hs+n s=hs+n, while Eq. 16 only certifies a fixed, per-symbol over-approximation of its effect. We propose replacing s s as the verifier’s input with the two quantities that generate it, h and n: h is bounded by its support ϕhδ _h^δ (Def. 3), and n keeps its existing noise-interval bound. We prepend a layer to the network graph that computes hshs directly, broadcasting the single h across all k symbols, and recover the original formula s^=hs+n s=hs+n by adding the existing noise term n. h↦hsh hs is exactly linear in h, since s is the fixed, known latent for the instance being verified. In real coordinates it is an exact block-diagonal 2k×22k× 2 matrix multiply, one rotation-scaling block MiM_i per symbol, all sharing the same h: (Re(hsi)Im(hsi))=(Re(si)−Im(si)Im(si)Re(si))(Re(h)Im(h)). pmatrixRe(hs_i)\\ Im(hs_i) pmatrix= pmatrixRe(s_i)&-Im(s_i)\\ Im(s_i)&Re(s_i) pmatrix pmatrixRe(h)\\ Im(h) pmatrix. (23) This affine layer is exactly what our bound propagation algorithms already handles. The addition with n is exact as it already is for the AWGN case. The fading arc ϕhδ=ejθ:|θ|≤δ _h^δ=\e^jθ:|θ|≤δ\ (solid line in Fig. 6) is enclosed by independent intervals Re(h)∈[cosδ,1]Re(h)∈[ δ,1], Im(h)∈[−sinδ,sinδ]Im(h)∈[- δ, δ] (shaded). Re(h)Re(h)Im(h)Im(h)δ =1h=1ejδe^jδe−jδe^-jδ Fig. 6: Fading residual h and its interval enclosure. Exposing h turns the joint input into the product domain ϕin=ϕhδ×n:‖n‖∞≤κσ(γ). _in\;=\; _h^δ× \n:\|n\|_∞≤κσ(γ) \. (24) The joint input is then enclosed by an interval on (h,n)(h,n), so Hölder concretization (9) (p=∞p=∞, q=1q=1) applies. 4.4 GloRo for DJSCC We instantiate GloRo for DeepJSCC’s decoder D: the task loss ℒL is the MSE reconstruction loss, and the penalty g(K)g(K_D) is derived below from the input property. The decoder is built entirely from convolutions, some preceded by upsampling (§4.2), PReLU activations, and a final sigmoid. Eq. 11’s product K≤∏l=1LK(l)K_D≤ _l=1^L_DK_D^(l) extends to the whole decoder with two more per-layer constants. Nearest-neighbor upsampling by 22 in each spatial dimension replicates every pixel into a 2×22× 2 block, so its Lipschitz constant is 22. The output sigmoid has Lipschitz constant 14 14, its maximum slope. Every layer’s constant is known in closed form, so K_D is cheap to compute. We derive the radius for GloRo training from the input property: by the Lipschitz definition Def. 1, ‖(s^)−(s)‖2≤K‖s^−s‖2≤Kr\|D( s)-D(s)\|_2≤ K_D\| s-s\|_2≤ K_Dr, where r is the ℓ2 _2 radius of the input property around the clean latent s: the smallest value with ‖s^−s‖2≤r\| s-s\|_2≤ r for every s^∈ϕin s∈ _in (Def. 3). Under AWGN, each of the 2k2k real axes of s^−s=n s-s=n stays within κσ(γ)κσ(γ) (Eq. 15), so rAWGN=2kκσ(γ)r_AWGN= 2k\,κσ(γ). Because MSEMSE averages over the n entries of x, the triangle inequality gives, for every s^∈ϕin s∈ _in, MSE(x,(s^))≤MSE(x,(s))+Kr/n MSE(x,D( s))≤ MSE(x,D(s))+K_Dr/ n. Only the second term depends on K_D, so we add its square to the reconstruction loss: ℒGloRo(θ)=MSE(x,(s^))+λ(Kr)22k,L_GloRo(θ)\;=\;MSE(x,D( s))\;+\;λ (K_Dr)^22k, (25) where s s is sampled through the channel as in regular training, and the penalty equals (Kr)2/n(K_Dr)^2/n up to the constant factor n/(2k)n/(2k), which λ absorbs. We fine-tune from a pretrained checkpoint, updating only the decoder. A smaller K_D tightens the certified [y¯,y¯][ y, y] that DNN verifier computes. Under Rayleigh fading, we keep the same loss form (25). By Prop. 1, |h−1|≤2sin(δ2)|h-1|≤ 2 ( δ2), and the hshs-layer linearity (§4.3) gives ‖s^−s‖2≤2sin(δ2)‖s‖2+2kκσ(γ)\| s-s\|_2≤ 2 ( δ2)\|s\|_2+ 2k\,κσ(γ). With ‖s‖2=k\|s\|_2= k (§2.1), the Rayleigh radius is: rRayleigh(γ,δ)=k(2sin(δ2)+2κσ(γ)).r_Rayleigh(γ,δ)\;=\; k\, (2 ( δ2)+ 2\,κσ(γ) ). (26) Substituting rRayleighr_Rayleigh for r in (25) adapts GloRo training to Rayleigh fading. 5 Experiments Our evaluation11 1 Code: https://anonymous.4open.science/r/verify-djscc-33C8/ answers the following research questions: RQ1: Do our verifier-compatibility choices preserve DeepJSCC’s reconstruction quality? RQ2: How does DeepJSCC’s certified robustness vary across different channel assumptions? RQ3: How much does GloRo tighten the certified bound? RQ4: Does structural encoding of property help? RQ5: Does theoretical safe certificate transfer to over-the-air software-defined-radio (SDR) transmission? 5.1 Experimental Design Models and data. We evaluate three decoder sizes (Tab. 1): small, medium, and large, all with the upsample-then-convolution decoder of §4.2. Models are trained on CIFAR-10 [31] for 100100 epochs under a randomized training-time SNR curriculum (γ∼(1,13)γ (1,13) dB). We formally verify the models at SNRs γ∈10,15,20,25,30γ∈\10,15,20,25,30\ dB. Under Rayleigh fading, the decoder additionally trains under a randomized residual-phase curriculum (δ∼(0∘,30∘)δ (0 ,30 ) per batch, §2.1); verification and GloRo certification both sweep estimator accuracy at δ∈0∘,2.5∘,5∘,7.5∘,10∘δ∈\0 ,2.5 ,5 ,7.5 ,10 \. Tab. 1: Decoder configurations evaluated. small medium large Latent dimension k 32 192 256 Encoder layers 3 4 5 Decoder layers 4 4 5 Parameters 7.7k 29.1k 143.4k Verifiers. We compare Ibp, DeepPoly, and α-Crown, all implemented in our own bound-propagation Python library since existing libraries do not cover the PReLU relaxation of §4.1 out of the box. On standard fully connected and convolutional ReLU networks, our implementations produce bounds that match auto_LiRPA [12]. Training methods. Naive training minimizes MSEMSE loss with Adam [32]. GloRo training follows §4.4 [25], fine-tuning a Naive-trained checkpoint for 20 epochs. Spectral norms use 10 power-iteration steps per weight matrix per training step. We set λ=10−4λ=10^-4 in Eq. 25: higher values collapse PSNR across all three model sizes, while lower values leave K_D unchanged; λ=10−4λ=10^-4 reduces K_D while preserving reconstruction quality for all sizes. Metrics. We use PSNR to compare training runs. Certified bounds are on MAE (Def. 4): every [y¯,y¯][ y, y] below bounds MAEMAE, not PSNRPSNR, and we report the upper bound y¯ y. Runtime. All experiments run on a single NVIDIA RTX 4080 SUPER GPU (16 GB), paired with an AMD Ryzen 9 5900X 12-core central processing unit (CPU) and 128 GB of DDR4-3200 random-access memory (RAM). SDR hardware. The over-the-air experiment (§5.7) uses two ADALM-PlutoSDR transceivers on a 915 MHz carrier at a 2 MHz sample rate. A Raspberry Pi 4 controls both transceivers, one transmitting and one receiving, and stores the received frames for offline decoding. We attenuate the transmitter by 20 dB and hold the receiver gain fixed at 30 dB. Higher settings saturated the receiver’s analog-to-digital converter, and the resulting clipping destroyed frame coherence. Each frame carries one OFDM symbol, a 512-point inverse fast Fourier transform (IFFT) with a 64-sample cyclic prefix, behind an 11-chip Barker preamble for frame synchronization. Every fourth subcarrier carries a known binary phase-shift keying (BPSK) pilot, which leaves 384 free bins, of which the first k=256k=256 carry the DeepJSCC latents. The receiver estimates the channel from those pilots by least squares, interpolates it across bins, and equalizes amplitude and phase together. Before the image transmissions, 300 probe frames of complex Gaussian tones characterize the link. We wipe the phase from each frame, then take the 99th percentile of the per-tone residual phase as δ and the error power as the operating SNR. 5.2 Effect of Verifier-Compatibility Changes We isolate each verifier-compatibility change from §4 with a paired ablation against the original DeepJSCC decoder (PReLU, transposed convolution), training all three model sizes under the AWGN channel with Naive training (§5.1). Fig. 7 reports test PSNR and MAE for the original decoder, the upsample-then-convolution substitution (§4.2), and a ReLU decoder in place of PReLU (§4.1). Replacing PReLU with ReLU cost 1.781.78, 2.012.01, and 2.222.22 dB of PSNR on small, medium, and large respectively, a 23%23\%, 29%29\%, and 28%28\% increase in MAE. The penalty grew with model size because a deeper decoder stacks more activation layers, and each one discards the negative-side signal that its learned slope would otherwise carry. This supports §4.1’s claim that PReLU’s single extra parameter per layer is worth its added relaxation cost. Verifying a ReLU-substituted decoder would answer a question about a different, worse model, which is why we derive a PReLU relaxation instead of substituting the activation away. The upsample-then-convolution substitution left reconstruction quality essentially intact: PSNR moved by at most 0.350.35 dB across all sizes (+0.05+0.05 dB on small, −0.35-0.35 dB on medium, −0.28-0.28 dB on large), and MAE by under 7%7\% at every size. The sign of the change varied with model size, which suggests the residual gap reflects training variation rather than a systematic loss. This is consistent with Prop. 3: both layers belong to the same operator family. §4.2’s claim therefore holds: the substitution buys a verifiable decoder at a small cost. (a) PSNRPSNR (b) MAEMAE Fig. 7: Reconstruction quality of the original, upsample-then-convolution, and ReLU decoders. 5.3 Certified Robustness Across Channel Models Fig. 8: Test PSNR over 100 training epochs for all three model sizes under AWGN and Rayleigh fading. Fig. 8reports test PSNR at a fixed evaluation SNR of 10 dB, the midpoint of the training curriculum γ∼(1,13)γ (1,13) dB. All models improved rapidly during the first 20 epochs, then slowed and plateaued. The small model achieved 99% of its peak PSNR by epochs 35 to 38, while the medium and large models converged between epochs 60 and 65. Rayleigh-trained models demonstrated similar initial improvement rates but plateaued at lower performance levels. This outcome is attributed to the fading residual h=ejθh=e^jθ (§2.1), which represents a phase rotation absent in AWGN training. Consequently, the Rayleigh channel is harder to decode. For the small, medium, and large models, Rayleigh-trained variants exhibited mean squared error (MSE) increases of 5.1%5.1\%, 11.4%11.4\%, and 10.5%10.5\%, respectively, compared to their AWGN counterparts, corresponding to PSNR reductions of 0.220.22, 0.470.47, and 0.430.43 dB. Model size influenced final PSNR more than channel type. The small model, using 94.6%94.6\% fewer parameters than large, achieved a PSNR that was 6.96.9 dB lower under both channel conditions. The medium model, with 79.7%79.7\% fewer parameters (4.9×4.9× smaller), achieved PSNR values within 1.61.6 dB of large under AWGN and within 1.81.8 dB under Rayleigh fading. Fig. 9: Certified MAE upper bound y¯ y under AWGN vs. SNR, per model size (DeepPoly). Fig. 10: Certified MAE upper bound y¯ y under Rayleigh fading vs. SNR and residual phase δ, per model size (DeepPoly). Fig. 9shows the certified MAE upper bound y¯ y under AWGN. For small (k=32k=32), y¯ y fell from 1.231.23 at SNR 1010 dB to 0.100.10 at 3030 dB. For medium (k=192k=192), y¯ y stayed above 11 until SNR 2525 dB and reached 0.190.19 at 3030 dB. For large (k=256k=256), y¯ y never dropped below 11: bound propagation across 256256 latent dimensions accumulated too much interval error for the verifier to certify anything useful. Certification is more tractable for smaller models, as fewer latent dimensions constrain interval expansion. Fig. 10 extends the analysis to Rayleigh fading, sweeping SNR and residual phase δ∈0∘,2.5∘,5∘,7.5∘,10∘δ∈\0 ,2.5 ,5 ,7.5 ,10 \. At δ=0∘δ=0 , the bound matched the AWGN result; as δ increases, the fading term 2sin(δ/2)|si|2 (δ/2)|s_i| in the input radius (Eq. 16) widens the input property and loosens the bound. For small at 3030 dB, y¯ y rose from 0.100.10 at δ=0∘δ=0 to 0.590.59 at δ=10∘δ=10 . For medium, the bound was only useful at δ=0∘δ=0 (y¯=0.17 y=0.17 at 3030 dB); any residual phase pushed y¯ y above 0.60.6. For large, y¯ y exceeded 11 in all conditions. SNR and δ jointly determine y¯ y. Higher SNR reduces the noise radius, whereas larger δ increases the fading radius, resulting in competing effects. The dominant factor between SNR and δ has significant implications for system design. For the small model at the highest tested SNR, increasing the residual phase error from a perfect estimate to 10∘10 raised y¯ y from 0.100.10 to 0.590.59. This represents an approximate sixfold increase that cannot be mitigated by increasing transmit power, as the noise radius is negligible at 3030 dB and the fading radius remains independent of SNR. Therefore, when a link operates well above the noise floor, the channel estimator’s accuracy, rather than transmit power, determines the strength of the certificate the receiver can provide. This observation also clarifies why per-symbol interval encoding becomes the limiting constraint at large δ, thereby motivating the structural encoding approach evaluated in §5.5. 5.4 Effect of GloRo Training on Certified Robustness Fig. 11 presents GloRo fine-tuning initiated from the naive checkpoint across 20 epochs. The figure tracks test PSNR, the Lipschitz constant K_D, and robust loss for each model size under AWGN and Rayleigh fading. The Lipschitz constant K_D decreased substantially during the first five epochs, from 41.941.9 to 6.56.5 for small and from 215.6215.6 to 25.525.5 for large. All three model sizes stabilized by epoch 10. Twenty epochs of fine-tuning were sufficient, as the remaining ten epochs resulted in minimal changes to K_D. The PSNR cost associated with regularizing K_D was 0.720.72 dB for small, 1.141.14 dB for medium, and 2.012.01 dB for large under AWGN. The corresponding Rayleigh fading costs were similar, at 0.730.73, 1.091.09, and 2.112.11 dB, respectively. Larger models incurred greater PSNR costs because their K_D values were higher and required more contraction. Fig. 11: GloRo fine-tuning over 20 epochs per model size under AWGN and Rayleigh fading. Fig. 12plots the certified MAE upper bound y¯ y as a cumulative distribution function (CDF) per model size, comparing naive and GloRo training under AWGN and Rayleigh fading (δ=0∘δ=0 , all SNRs pooled). For small under AWGN, y¯ y fell from 1.231.23 to 0.530.53 at SNR 1010 dB, a 57%57\% reduction. At SNR 3030 dB, naive and GloRo both reached y¯≈0.10 y≈ 0.10: the AWGN noise ball dominates the bound at high SNR, so tightening K_D adds nothing there. For medium, the gain concentrated at high SNR: y¯ y dropped from 0.190.19 to 0.080.08 at 3030 dB. For large, naive training never certified anything useful (y¯>1 y>1 at every SNR), whereas GloRo brought y¯ y to 0.850.85 at 1010 dB and 0.080.08 at 3030 dB, making large certifiable in our experiments. At δ=0∘δ=0 , Rayleigh bounds fell by comparable fractions. GloRo shifted the entire bound distribution to the left for every model size and both channels, indicating that the improvement is not limited to a subset of images. The two effects of GloRo oppose each other, and the dominant effect depends on the specific model. For large, a PSNR cost of 2.012.01 dB resulted in the difference between no certificate and obtaining a certificate at every tested SNR, making this trade-off advantageous. For small at 3030 dB, naive and GloRo approaches achieved y¯≈0.10 y≈ 0.10, indicating that the 0.720.72 dB cost did not yield a tighter bound. This outcome occurs because y¯ y is determined by the term that dominates the input radius. When the noise ball is dominant, as at high SNR on a small latent, reducing K_D cannot further tighten a bound already constrained by the input region. GloRo is most effective when the bound’s looseness stems primarily from the decoder’s amplification rather than the channel, which characterizes the operational regime of all larger models. (a) Small (b) Medium (c) Large Fig. 12: CDF of the certified MAE upper bound y¯ y for naive and GloRo-trained decoders. 5.5 Joint Verification of the Fading Coefficient 13(a)compares interval and structural encoding as the residual phase δ grows from 0∘0 to 10∘10 on the small model at SNR 2020 dB. At δ=0∘δ=0 , both approaches coincided at y¯≈0.32 y≈ 0.32: there is no phase uncertainty, so the per-symbol interval is already tight. As δ increases, the interval bound rises sharply, reaching y¯≈0.52 y≈ 0.52 at δ=10∘δ=10 . This occurs because each of the 2k2k interval half-widths increases by 2sin(δ/2)|si|2 (δ/2)|s_i| (Eq. 16), and these independent excesses accumulate. The structural bound stays nearly flat over the same range, at y¯≈0.33 y≈ 0.33 when δ=10∘δ=10 . Reasoning over the single shared h (§4.3) provides the verifier with two additional degrees of freedom, independent of k. As a result, the phase term contributes minimal slack. 13(b) extends the comparison across all three model sizes (S/M/L == small/medium/large), pooling all SNRs and phases δ∈0∘,2.5∘,5∘,7.5∘,10∘δ∈\0 ,2.5 ,5 ,7.5 ,10 \. For small, the structural median fell from 0.280.28 to 0.190.19; for medium, from 0.430.43 to 0.270.27; for large, from 0.460.46 to 0.270.27. The improvement increased with model size. Larger k results in more per-symbol interval terms, so the fixed-dimensional input of structural encoding saves more accumulated slack. The narrowing of interquartile ranges indicates that the benefit is consistent across SNR and phase conditions, rather than influenced by a small number of instances. (a) y¯ y vs. δ (small, SNR 2020 dB). (b) y¯ y per model size (all SNRs and δ pooled). Fig. 13: Interval vs. structural encoding of the fading coefficient under Rayleigh fading. Structural encoding substantially reduces δ-sensitivity and lowers the bound across all model sizes (Fig. 13). Structural encoding replaces 2k2k interval inputs with a single affine layer over two real variables (Eq. 23). Consequently, the verifier propagates a smaller input region through one additional exact layer and performs less computation overall. This advantage contrasts with verification scenarios, where larger networks present greater computational challenges. The removed penalty scales with k, so structural encoding provides the greatest benefit for models where interval encoding is least effective. Together with §5.3, these findings demonstrate that the fading radius limits the certificate once a link surpasses the noise floor. Structural encoding prevents this radius from scaling with the latent dimension. 5.6 Certified Safety Count of the Full Pipeline The preceding sections measured y¯ y in isolation. A practical deployment question requires a broader perspective: specifically, the number of (image, threshold) pairs a verifier can certify and the time required to do so. We counted certified-safe pairs on the large model at δ=10∘δ=10 , the widest phase uncertainty we consider. Ten images, one from each CIFAR-10 class, combined with five SNRs, resulted in 5050 bound queries. Each query was evaluated against seven MAE thresholds τ∈0.25,0.275,…,0.40τ∈\0.25,0.275,…,0.40\, resulting in 50×750×7 cactus instances per encoding. A cactus instance is a (property, network, threshold) query. α-Crown is applied to each τ individually and terminates at the first pass where y¯<τ y<τ. 14(a)presents a comparison between DeepPoly and α-Crown on the GloRo-trained model, pooling results from both interval and structural encodings. Both verifiers certified the same 211211 instances: 1919 on interval and 192192 on structural encoding. DeepPoly completed each query in approximately 0.100.10 s. α-Crown returned in about 0.110.11 s, because the first DeepPoly-equivalent pass met every τ that these runs cleared. Therefore, DeepPoly serves as the preferred default when the property is specified at these thresholds. Ibp did not certify any instance in any of the training or encoding configurations evaluated. Computation speed is inconsequential if the relaxation method fails to certify any instances. 14(b)compares interval and structural encodings under α-Crown, aggregating results from both Naive and GloRo training. Naive training did not certify any instances under either encoding. In the absence of Lipschitz regularization, the decoder amplified the input region excessively, preventing y¯ y from falling below the specified thresholds. GloRo combined with interval encoding certified 1919 instances. GloRo with structural encoding certified 192192 instances, 10×10× more. Neither component substitutes for the other. GloRo is essential; without it, no instances are certified due to the dominant amplification effect of the decoder. Structural encoding converts the available headroom into certified instances at large δ by eliminating the per-symbol expansion that would re-inflate the input region. This ordering is consistent with the results presented in §5.4. GloRo addresses the decoder’s contribution to the bound, while structural encoding targets the channel’s contribution. These two methods operate on distinct terms, resulting in complementary rather than overlapping improvements. (a) DeepPoly vs. α-Crown. (b) Interval vs. structural. Fig. 14: Certified-safe instance count vs. verification time. 5.7 Over-the-Air Transfer to SDR All previously established bounds are based on a channel model. This section evaluates whether a certificate derived from that model remains valid when applied to a real radio link. We characterize the channel between the two ADALM-PlutoSDR transceivers (§5.1), verify the decoder at the measured operating point, then transmit and check the reconstructions against the bound. Pilot measurements yielded an operating SNR of 27.427.4 dB and a 9999th-percentile residual phase of δ=5.4∘δ=5.4 , both within the ranges explored in §5.3. Although the link exhibited minimal interference, its SNR significantly exceeded the 11–1313 dB range used during training, indicating that the decoder operated outside its original training conditions. Fig. 15 presents a representative input image and its corresponding over-the-air reconstruction at this operating point for each of the ten CIFAR-10 classes. Fig. 15: Input images (top) and over-the-air reconstructions (bottom) for all ten CIFAR-10 classes. Fig. 16displays, for each class, the observed over-the-air reconstruction error (the maximum MAEMAE over 3030 transmissions of a representative image) alongside its margin to the certified upper bound y¯ y, such that each complete bar represents y¯ y. The certificate held for every class: the observed maximum stayed below y¯ y in each class and in the aggregate, where the worst of 300300 frames (0.08240.0824) stayed below the largest bound (0.12780.1278). Class 77 approached its bound most closely (0.0820.082 versus 0.1280.128), while class 55 exhibited the widest margin (0.0350.035 versus 0.0910.091). Across all classes, the observed maximum ranged from 3838 to 65%65\% of the certified bound. The certificate is neither violated nor excessively permissive; it provides meaningful headroom without being so loose as to permit arbitrary behavior. Each bar aggregates 3030 transmissions of a representative image, for a total of 300300 over-the-air frames shown in the figure. Within each class, the 9999th percentile and the maximum differed by no more than 0.00010.0001. Reconstruction error demonstrated high repeatability: across 3030 independent transmissions through the radio link, the worst trial was only marginally greater than the median. The margin in Fig. 16 is stable slack against the channel model rather than the tail of a noisy measurement. This experimental design introduces one caveat. Each bar corresponds to a fixed image per class, so it evaluates the certificate at ten specific points rather than across the entire test set. The bound applies to every input within the noise region; the measurement confirms its validity at the sampled points. Fig. 16: Per-class observed over-the-air MAEMAE stacked with its margin to the certified bound y¯ y. This guarantee is inherently conditional. It constrains the reconstruction error only while the link remains within the SNR and phase envelope measured by the pilot signals. A receiver operating outside this envelope requires a new certificate. This requirement is not onerous in practice, as re-verification at a new operating point can be performed in well under a second using DeepPoly, as described in §5.6. Consequently, a receiver can re-certify itself whenever its channel estimate changes, incurring a computational cost significantly lower than that of the protected transmission. The measurement demonstrates that the entire process—from channel modeling, through bound-propagation certification, to the physical radio link—remains valid end to end. The bounds the verifier produces offline continue to constrain the hardware’s behavior accurately. 6 Related Work 6.1 Neural Network Verifiers Complete verifiers perform an exact search of the network’s piecewise-linear structure. Reluplex [17] extends the Simplex algorithm to ReLU constraints. Marabou [13] incorporates theory solvers and parallel divide-and-conquer strategies. The DPLL(T)-based NeuralSAT [33, 29] explores activation patterns using bound propagation as its theory solver. Other approaches improve verification scalability by exploiting neuron stability [14], training networks to promote stable neurons [26], decomposing networks into assume-guarantee subproblems [15], and learning branching heuristics through reinforcement learning [34]. Our GloRo instantiation (§4.4) adopts the training-based approach. Bound propagation, the foundation of this work, over-approximates each layer using a sound linear relaxation and back-substitutes these relaxations to the input. Ibp [9] offers the fastest but least precise bounds. DeepPoly [11] back-substitutes symbolic linear bounds in a single pass. Crown [10] and its successors α-Crown [12, 16] and β-Crown [28] optimize relaxation slopes using gradient descent. However, none of these tools provide native support for PReLU or transposed convolution (§4.1, §4.2). Bound propagation tools have won every recent International Verification of Neural Networks Competition (VNN-COMP) [35]. This consistent success motivates our decision to build upon this family of methods. 6.2 Applications of DNN Verification A growing line of work certifies wireless and telecommunication systems. Kim et al. [18] certify robustness of an antenna-selecting network for massive MIMO; Le and Matsumura [19] verify a regression network predicting mobile-traffic load; Le et al. [20] verify a power-control policy network for massive MIMO; Le et al. [36] use formal methods to craft adversarial attacks on a deep reinforcement learning (DRL)-based multi-user MIMO scheduler. Each targets a discrete decision or a single continuous quantity under one noise source. Our setting differs in three ways. We certify DeepJSCC’s decoder under the physical AWGN and Rayleigh fading channel models. The property is a continuous reconstruction bound. Finally, no prior wireless verification addresses PReLU, transposed convolutions, or the per-symbol interval blow-up of a shared fading coefficient, which block off-the-shelf verifiers (§1). 7 Conclusion We addressed three primary challenges that prevent off-the-shelf verifiers from operating with DeepJSCC’s decoder. PReLU, transposed convolution, and a fading channel shared across all latent symbols each allow for a principled reformulation compatible with existing bound-propagation methods: a relaxation that extends the ReLU case, a layer substitution within the same operator family, and an adjustment of verifier input to the channel’s actual low-dimensional generator. None of these reformulations sacrifices reconstruction quality for verifiability; in particular, structural encoding strengthens certificates. The resulting certificate remains valid under real radio channel conditions. Experimental results support these findings: GloRo training reduces the large decoder’s Lipschitz constant from 215.6215.6 to 25.525.5, enabling certification - the upper bound decreases from above 11 at all SNRs to 0.080.08. Over-the-air tests further confirm it: across the ten CIFAR-10 classes the worst observed error is 0.0820.082, against a certified bound of 0.1280.128. Applying this approach to attention-based and rate-adaptive successors, such as WITT [3] and SwinJSCC [37], as well as to modalities beyond images, remains an open research direction. These successors are based on vision transformers (ViTs), whose attention layers require abstract domains beyond the ReLU and PReLU relaxations used in this work. Recent abstract domains developed for verifying large generative pre-trained transformer (GPT) models [38] provide a promising foundation for this extension. References [1] Timothy O’shea and Jakob Hoydis “An Introduction to Deep Learning for the Physical Layer” In IEEE Transactions on Cognitive Communications and Networking 3.4 IEEE, 2017, p. 563–575 [2] Eirina Bourtsoulatze, David Burth and Deniz Gündüz “Deep Joint Source-Channel Coding for Wireless Image Transmission” In IEEE Transactions on Cognitive Communications and Networking 5.3, 2019, p. 567–579 DOI: 10.1109/TCCN.2019.2919300 [3] Ke Yang et al. “WITT: A Wireless Image Transmission Transformer for Semantic Communications” In ICASSP 2023-2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), 2023, p. 1–5 IEEE [4] Yalin Sagduyu, Tugba Erpek, Aylin Yener and Sennur Ulukus “Will 6G Be Semantic Communications? Opportunities and Challenges from Task Oriented and Secure Communications to Integrated Sensing” In IEEE Network IEEE, 2024 [5] Tilahun Getu, Georges Kaddoum and Mehdi Bennis “Semantic Communication: A Survey on Research Landscape, Challenges, and Future Directions” In Proceedings of the IEEE IEEE, 2025 [6] Wanting Yang et al. “Semantic Communications for Future Internet: Fundamentals, Applications, and Challenges” In IEEE Communications Surveys & Tutorials 25.1 IEEE, 2022, p. 213–250 [7] Huiqiang Xie, Zhijin Qin, Geoffrey Li and Biing-Hwang Juang “Deep Learning Enabled Semantic Communication Systems” In IEEE Transactions on Signal Processing 69 IEEE, 2021, p. 2663–2675 [8] Huiqiang Xie and Zhijin Qin “A Lite Distributed Semantic Communication System for Internet of Things” In IEEE Journal on Selected Areas in Communications 39.1 IEEE, 2020, p. 142–153 [9] Shiqi Wang et al. “Formal Security Analysis of Neural Networks Using Symbolic Intervals” In 27th USENIX Security Symposium (USENIX Security 18), 2018, p. 1599–1614 URL: https://dl.acm.org/doi/10.5555/3277203.3277323 [10] Huan Zhang et al. “Efficient Neural Network Robustness Certification with General Activation Functions” In Advances in Neural Information Processing Systems 31, 2018 URL: https://dl.acm.org/doi/10.5555/3327345.3327402 [11] Gagandeep Singh, Timon Gehr, Markus Püschel and Martin Vechev “An Abstract Domain for Certifying Neural Networks” In Proceedings of the ACM on Programming Languages 3.POPL, 2019, p. 1–30 DOI: 10.1145/3290354 [12] Kaidi Xu et al. “Automatic Perturbation Analysis for Scalable Certified Robustness and Beyond” In Advances in Neural Information Processing Systems 33, 2020, p. 1129–1141 URL: https://dl.acm.org/doi/10.5555/3495724.3495820 [13] Guy Katz et al. “The Marabou Framework for Verification and Analysis of Deep Neural Networks” In Computer Aided Verification: 31st International Conference, CAV 2019 Springer, 2019, p. 443–452 [14] Hai Duong, Dong Xu, Thanhvu Nguyen and Matthew. Dwyer “Harnessing Neuron Stability to Improve DNN Verification” In Proc. ACM Softw. Eng. 1.FSE New York, NY, USA: Association for Computing Machinery, 2024 DOI: 10.1145/3643765 [15] Hai Duong, David Shriver, ThanhVu Nguyen and Matthew. Dwyer “Compositional Neural Network Verification via Assume-Guarantee Reasoning” In Advances in Neural Information Processing Systems (NeurIPS), 2025 [16] Kaidi Xu et al. “Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers” In International Conference on Learning Representations, 2021 [17] Guy Katz et al. “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks” In International Conference on Computer Aided Verification, 2017, p. 97–117 Springer DOI: 10.1007/978-3-319-63387-9˙5 [18] Jaekwon Kim, Hyo-Sang Lim and Kwanghoon Choi “Certified Robustness of Antenna Selecting Neural Networks for Massive MIMO Wireless Communications” In IEEE Access IEEE, 2025 DOI: 10.1109/ACCESS.2025.3570973 [19] Thanh Le and Takeshi Matsumura “Formal Verification for Deep Learning-based Mobile Network Traffic Prediction” In The 8th International Conference on Artificial Intelligence in Information and Communications Technologies, 2026 [20] Thanh Le, Takeshi Matsumura, Yusheng Ji and John Lui “Formal Verification for Deep Learning-based Power Control in Massive MIMO” In arXiv preprint arXiv:2607.14500, 2026 [21] Kaiming He, Xiangyu Zhang, Shaoqing Ren and Jian Sun “Delving Deep into Rectifiers: Surpassing Human-level Performance on ImageNet Classification” In Proceedings of the IEEE International Conference on Computer Vision, 2015, p. 1026–1034 [22] David Tse and Pramod Viswanath “Fundamentals of Wireless Communication” New York: Cambridge University Press, 2005 [23] Hai Duong, Thanh Le, Long Nguyen and ThanhVu Nguyen “Verifying Structural Robustness of Deep Neural Network” In Proceedings of the ACM on Software Engineering (FSE), 2026 [24] Hai Duong, Long Nguyen, Thanh Le and ThanhVu Nguyen “Verifying Neural Network Robustness with Dual Perturbations” In Conference on Computer Vision and Pattern Recognition (CVPR), 2026 [25] Klas Leino, Zifan Wang and Matt Fredrikson “Globally-robust Neural Networks” In International Conference on Machine Learning, 2021, p. 6212–6222 PMLR [26] Dong Xu, Nusrat Mozumder, Hai Duong and Matthew. Dwyer “Training for Verification: Increasing Neuron Stability to Scale DNN Verification” In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2024 Springer [27] Vincent Tjeng, Kai Xiao and Russ Tedrake “Evaluating Robustness of Neural Networks with Mixed Integer Programming” In International Conference on Learning Representations, 2019 DOI: 1721.1/119563 [28] Shiqi Wang et al. “Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification” In Advances in Neural Information Processing Systems 34, 2021, p. 29909–29921 [29] Hai Duong, ThanhVu Nguyen and Matthew Dwyer “NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks” In International Conference on Computer Aided Verification, 2025, p. to appear [30] Hai Duong, ThanhVu Nguyen and Matthew. Dwyer “Generating and Checking DNN Verification Proofs” In Advances in Neural Information Processing Systems (NeurIPS), 2025 [31] Alex Krizhevsky and Geoffrey Hinton “Learning Multiple Layers of Features from Tiny Images” Toronto, ON, Canada, 2009 [32] Diederik Kingma and Jimmy Ba “Adam: A Method for Stochastic Optimization” In arXiv preprint arXiv:1412.6980, 2014 [33] Hai Duong, ThanhVu Nguyen and Matthew Dwyer “A DPLL(T) Framework for Verifying Deep Neural Networks” In arXiv preprint arXiv:2307.10266, 2024 DOI: 10.48550/arXiv.2307.10266 [34] Hai Duong, Thanh Le and ThanhVu Nguyen “Verifying Neural Networks with Reinforcement Learning” Accepted In Advances in Neural Information Processing Systems (NeurIPS), 2026 [35] Kaulen et al. “The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results” In arXiv preprint arXiv:2512.19007, 2025 [36] Thanh Le et al. “FGGM: Formal Grey-box Gradient Method for Attacking DRL-based MU-MIMO Scheduler” In arXiv preprint arXiv:2510.26075, 2025 [37] Ke Yang et al. “SwinJSCC: Taming Swin Transformer for Deep Joint Source-Channel Coding” In IEEE Transactions on Cognitive Communications and Networking IEEE, 2024 [38] Hai Duong, Thanh Le and ThanhVu Nguyen “ZonoGPT: Towards An Abstract Domain for Verifying Large GPT Models” In arXiv preprint arXiv:2609.34457, 2026 IEEEbiography []THANH LE received the B.E. degree in information and communication technology and the M.S. degree in data science from Hanoi University of Science and Technology, Vietnam, in 2019 and 2021, respectively, and the Ph.D. degree in informatics from The Graduate University for Advanced Studies, SOKENDAI, Tokyo, Japan, in 2025. Since 2025, he has been a Researcher with the Wireless Systems Laboratory, National Institute of Information and Communications Technology (NICT), Japan. His research focuses on bringing formal methods from software engineering to analyze, verify, and improve the robustness of AI-enabled wireless systems. IEEEbiography []HAI DUONG received the B.S. and M.S. degrees in electrical engineering from Hanoi University of Science and Technology, Hanoi, Vietnam, in 2019 and 2021, respectively. He is currently pursuing the Ph.D. degree in computer science with George Mason University, Fairfax, VA, USA, where he works at the ROARS Lab on deep neural network verification. He develops NeuralSAT, a neural network verification tool that ranked second overall in VNN-COMP 2024 and 2025. His research interests include DNN verification and testing, proof generation and checking, formal methods, and automated reasoning. IEEEbiography []TAKESHI MATSUMURA received the M.S. and Ph.D. degrees in Electronic Engineering and Nano-mechanics Engineering from Tohoku University in 1998 and 2020, respectively. From 1998 to 2007, he was engaged in the R&D of wireless communications devices in several private companies. He joined National Institute of Information and Communications Technology (NICT) in 2007, focusing on white-space and 5G systems. From 2016 to 2019, he has served as Associated Professor at Graduate School of Informatics, Kyoto University. He returned to NICT in April to take on the role of Research Manager and became Director of Wireless Systems Laboratory in 2021. He now serves as Research Executive Director at Network Research Institute and Project Manager of the Moonshot Goal 1 project. His research interests include white-space communication, wide-area wireless networks, 5G systems, and reliability-ensuring platform for cybernetic avatar teleoperation. He is a member of IEICE and IEEE. IEEEbiography []THANHVU NGUYEN received the B.S. and M.S. degrees in computer science from The Pennsylvania State University, USA, in 2003 and 2006, respectively, and the Ph.D. degree in computer science from the University of New Mexico, Albuquerque, USA, in 2014. He was a Postdoctoral Researcher with the University of Maryland, College Park, from 2014 to 2016, and an Assistant Professor with the University of Nebraska–Lincoln from 2016 to 2021. He is currently an Associate Professor of Computer Science and the Director of the M.S. Software Engineering program at George Mason University, USA. He is a recipient of the NSF CAREER Award, the NSF CRII Award, two Amazon Research Awards, and three test-of-time paper awards, including the IEEE TSE Most Influential Paper Award and the ACM SIGSOFT ICSE 10-Year Most Influential Paper Award. He is a Senior Member of ACM and IEEE. His research lies at the intersection of software engineering and formal methods, focusing on AI safety and program correctness.