PaperlayerView exact revision on arXiv

Source-linked AI summary

Neural Network Verification for Deep Joint Source-Channel Coding

Thanh Le, Hai Duong, Takeshi Matsumura, ThanhVu Nguyen

arXiv:2610.11994v1cs.SEcs.AI

TL;DR

DeepJSCC has no formal worst-case reconstruction bounds, and existing verifiers do not support several components of its decoder. This paper reformulates those components for bound propagation and combines verification with GloRo training; the resulting pipeline lowers certified bounds and is validated over the air.

  • Problem

    Existing verifiers cannot directly handle DeepJSCC decoder components including PReLU, transposed convolutions, and Rayleigh fading.

    Source: §I · p. 2

  • Method

    The paper adapts bound propagation to DeepJSCC’s decoder and applies GloRo Lipschitz regularization for certification under wireless channel disturbances.

    Source: §I · p. 2

  • Results

    At 10° phase uncertainty, structural encoding with GloRo certifies 192 safe cases against 19 for GloRo with interval encoding, while over-the-air tests report a worst observed error of 0.082 against a certified bound of 0.128.

    Source: §I · p. 2, §VII · p. 14

  • Takeaways & Limitations

    The resulting certificate remains valid under real radio channel conditions, and the reformulations preserve reconstruction quality while structural encoding strengthens certificates.

    Source: §VII · p. 14

Abstract

from arXiv · show

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.

I. Introduction

DeepJSCC lacks formal worst-case reconstruction guarantees under wireless channel disturbances, while existing verifiers cannot directly handle key decoder components. This paper introduces a bound-propagation framework and reformulates those components for verification.

I. Introduction

  • DeepJSCC training optimizes average performance on observed channel realizations, while finite-sample testing cannot bound worst-case reconstruction quality across all possible realizations.The gap matters in settings where corrupted images may contribute to incorrect downstream decisions.Source: §I · pp. 1–2
  • Existing bound-propagation tools cannot directly verify the decoder because it uses PReLU activations, transposed convolutions, and a shared residual phase rotation under Rayleigh fading.ReLU substitution can reduce reconstruction quality by up to two decibels, while independently interval-bounding latent coordinates ignores the shared rotation.Source: §I · p. 2
  • The proposed framework extends optimized linear relaxations to PReLU, substitutes upsampling followed by convolution for transposed convolution, and bounds Rayleigh fading through its two real coordinates.The structural fading representation reduces the verifier input from 2k per-symbol intervals to two degrees of freedom for one complex block-fading coefficient.Source: §I · p. 2
  • The framework also applies GloRo Lipschitz regularization to the decoder, providing a closed-form robustness radius for AWGN and Rayleigh fading.This allows Lipschitz-aware fine-tuning from a pretrained checkpoint.Source: §I · p. 2

A. DeepJSCC System Model

  • DeepJSCC jointly maps an input image to complex channel symbols and reconstructs an image from the corrupted symbols using an encoder, wireless channel, and decoder.The encoder enforces an average power constraint; the decoder uses transposed convolutions and PReLU activations, then applies a sigmoid before pixel rescaling.Source: A. DeepJSCC System Model · p. 3
  • Under slow Rayleigh fading, the received symbols equal the transmitted symbols multiplied by a residual phase factor plus additive noise; the assumed phase error is bounded by δ.The model assumes exact amplitude equalization, leaving only the residual phase unknown.Source: A. DeepJSCC System Model · p. 3

B. Neural Network Verification

Neural network verification can certify reconstruction quality over a specified channel-noise region, rather than only testing individual inputs. Bound propagation provides sound output intervals, with tighter methods trading computation for precision.

B. Neural Network Verification

  • The verification property links a latent-symbol input region to a reconstruction-quality output property, and bound propagation can certify a minimum quality over the noise range.A bound that does not prove the property yields “unknown,” even when the true network may satisfy it.Source: B. Neural Network Verification · p. 3, C. Bound Propagation · p. 3

C. Bound Propagation

  • Bound propagation computes a sound output interval over the input region; Ibp is fastest and loosest, while α-Crown tunes relaxation slopes for tighter bounds at greater cost.DeepPoly back-substitutes linear relaxations in one pass.Source: C. Bound Propagation · p. 3

1) Interval bound propagation

  • Ibp propagates concrete intervals layer by layer, but discards correlations, so its over-approximation can widen and become vacuous on deep networks.For affine layers, it splits positive and negative weights to bound the output endpoints.Source: 1) Interval bound propagation · pp. 3–4

2) Linear relaxation

  • For an unstable ReLU, linear relaxation bounds its output with upper and lower lines; DeepPoly chooses a lower slope of 0 or 1, shaping the over-approximation area.A stable ReLU is exact and needs no relaxation.Source: 2) Linear relaxation · p. 4

3) Back-substitution and concretization

Back-substitution eliminates intermediate variables so bounds depend only on the input. α-Crown optimizes relaxation slopes to tighten the certified output bound.

3) Back-substitution and concretization

  • Back-substitution repeatedly replaces intermediate variables with their affine bounds until the resulting bound depends only on the input.Concretization evaluates the resulting linear forms over the input region to obtain bounds.Source: 3) Back-substitution and concretization · p. 4
  • Concretized bounds determine neuron stability and the linear relaxation used in subsequent layers.For an ℓp ball, the passage invokes Hölder’s inequality to obtain a closed form.Source: 3) Back-substitution and concretization · p. 4

4) Optimization of linear bound

  • α-Crown optimizes lower slopes α by gradient descent on the certified output bound; unlike fixed DeepPoly slopes, this requires T full backward passes.Each iteration obtains intervals with Ibp, back-substitutes layer by layer, concretizes, then updates α with a projected gradient step.Source: 4) Optimization of linear bound · pp. 4–5

D. Lipschitz-Certified Training

Verification bounds a trained model’s output change but does not alter its weights, so the paper complements certification with GloRo-style training. GloRo regularizes global sensitivity through a product of layerwise Lipschitz constants.

D. Lipschitz-Certified Training

  • Bound propagation evaluates a trained model but cannot itself improve robustness because it does not change the model weights.The paper therefore complements verification with GloRo-style training.Source: D. Lipschitz-Certified Training · p. 5
  • A small Lipschitz constant K upper-bounds output change by Kε for any input pair within distance ε, quantifying global sensitivity.The bound applies everywhere, not only near one test point.Source: D. Lipschitz-Certified Training · p. 5
  • GloRo upper-bounds network K by multiplying per-layer Lipschitz constants and penalizes K during training to shrink global sensitivity.Affine and convolutional layers use spectral norms; ReLU has constant 1, while PReLU uses max(1, |a|).Source: D. Lipschitz-Certified Training · p. 5

III. Problem Formulation

The formulation treats channel-corrupted latent symbols as the decoder’s input region and reconstruction quality as its output property. AWGN and slow Rayleigh fading produce different interval descriptions for that input.

A. Input Property

  • DeepJSCC verification is formulated as a DNN verification problem with an input property on latent symbols and an output property on reconstruction quality.The received-symbol input property is an interval around each transmitted latent symbol.Source: §III · p. 5, A. Input Property · p. 5
  • For AWGN, the received symbols equal the transmitted symbols plus complex Gaussian noise, and κ sets how many standard deviations the interval extends on each axis.κ = 3 covers about 99.7% of the noise mass per axis, not jointly over all 2k axes.Source: A. Input Property · p. 5
  • Under slow Rayleigh fading, the residual channel coefficient stays effectively constant over a packet; with imperfect estimation it can be modeled as a phase rotation bounded by δ.The reachable values for each symbol lie on an arc as the phase varies from −δ to δ.Source: A. Input Property · p. 5
  • The interval enclosure is sound because it never excludes a received symbol that an allowed fading coefficient could produce.This bounds the reachable set {h s_i} with an interval around s_i for interval-based verifiers.Source: A. Input Property · p. 5
  • The phase-rotation deviation is bounded by 2 sin(δ/2)|s_i|, yielding a sound interval enclosure around each transmitted symbol.The bound follows from |h−1| ≤ 2 sin(δ/2) for |θ| ≤ δ ≤ π.Source: A. Input Property · p. 6
  • The Rayleigh input interval adds the AWGN noise interval to the fading term, whose radius varies by transmitted symbol and does not shrink with SNR.Unlike AWGN, the interval radius is not uniform across symbols.Source: A. Input Property · p. 6

B. Output Property

The verification framework bounds reconstruction quality using MAE and checks the resulting interval against a threshold. Its PReLU relaxation extends ReLU’s feasible slopes to accommodate learned negative-side slopes while retaining sound bounds.

B. Output Property

  • The verifier bounds reconstruction quality with MAE, since PSNR and MSE are nonlinear, and checks whether the certified MAE interval satisfies the output threshold.MAE is represented exactly using two ReLU primitives; a bound satisfying the threshold returns safe.Source: B. Output Property · p. 6

C. Verification Framework

  • The verification framework propagates the input property through the decoder, bounds the reconstruction, computes MAE against the clean image, and checks the output threshold.If the certified upper bound exceeds the threshold, the result is unknown.Source: C. Verification Framework · p. 6

IV. Propose Approach

  • The proposed framework extends α-Crown’s PReLU relaxation, replaces unsupported decoder operations, models fading structurally, and instantiates GloRo for DeepJSCC.The approach is intended to make DeepJSCC certifiably robust.Source: §IV · p. 6

A. PReLU Relaxation with an Auto-Tuned Slope

  • The sound PReLU relaxation lets α-Crown tune lower-bound slopes within [a, 1], generalizing ReLU’s [0, 1] interval without substituting away the learned slope.Setting a = 0 recovers the ReLU relaxation.Source: A. PReLU Relaxation with an Auto-Tuned… · p. 7

B. Substituting Transposed Convolution with Upsampling

The decoder’s transposed convolutions are replaced by nearest-neighbor upsampling followed by ordinary convolution, operations supported by bound propagation. The substitution is mathematically equivalent to a stride-s transposed convolution with a corresponding kernel and preserves reconstruction performance empirically.

B. Substituting Transposed Convolution with Upsampling

  • Nearest-neighbor upsampling followed by convolution equals a stride-s transposed convolution with kernel w = 1_s ∗ v.The identity supports replacing decoder transposed convolutions with operations handled by the verifier.Source: B. Substituting Transposed Convolution… · p. 7
  • The substitution preserves the output shape and operator family of the replaced layer.The stated identity extends from one spatial dimension and one channel to two-dimensional, multi-channel layers by applying it per index and channel.Source: B. Substituting Transposed Convolution… · pp. 7–8
  • Experiments confirm that the substitution preserves DeepJSCC’s reconstruction performance.The decoder originally uses transposed convolutions to increase spatial resolution.Source: B. Substituting Transposed Convolution… · pp. 7–8

C. Structural Perturbation of Fading Residual Interval

The structural fading formulation exposes the shared residual fading variable and noise to bound propagation, rather than independently bounding each latent symbol’s channel effect. This retains the shared-channel structure that per-symbol interval encoding loses.

C. Structural Perturbation of Fading Residual Interval

  • The per-symbol Rayleigh interval expands a one-dimensional shared-fading curve into a 2k-dimensional hypercube, making the enclosure loose.Each symbol’s radius is derived from its own worst case even though all k symbols share one residual h.Source: C. Structural Perturbation of Fading… · p. 8
  • The proposed structural encoding bounds the generators h and n directly, prepending a layer that computes hs and then adds the noise term.Broadcasting the single h across all k symbols retains their shared rotation structure.Source: C. Structural Perturbation of Fading… · p. 8
  • The map h ↦ hs is linear for the fixed latent s, and bound propagation handles this affine layer and the noise addition exactly.In real coordinates, the map is a block-diagonal 2k × 2 multiply whose per-symbol blocks share h.Source: C. Structural Perturbation of Fading… · p. 8

D. GloRo for DJSCC

The paper instantiates GloRo for the DeepJSCC decoder using MSE reconstruction loss and a Lipschitz-based penalty derived from the input property. It computes channel-specific input radii for the robustness penalty.

D. GloRo for DJSCC

  • GloRo uses the decoder’s MSE reconstruction loss and a penalty derived from the input property.The training loss samples the latent through the channel, and the decoder is fine-tuned from a pretrained checkpoint.Source: D. GloRo for DJSCC · p. 8
  • The decoder’s Lipschitz constant is computed from per-layer constants for convolutions, upsampling, PReLU activations, and the final sigmoid.Nearest-neighbor upsampling by 2 in each spatial dimension has Lipschitz constant 2; the sigmoid has constant 1.Source: D. GloRo for DJSCC · p. 8
  • The GloRo penalty uses the decoder Lipschitz constant multiplied by the input-property radius, with channel-specific radii for AWGN and Rayleigh fading.The Rayleigh radius replaces the AWGN radius in the same loss form.Source: D. GloRo for DJSCC · p. 8

V. Experiments

The experiments test whether verifier-compatible decoder changes preserve reconstruction quality and examine certified robustness across AWGN and Rayleigh fading. They vary model size, SNR, and residual phase to characterize the bounds.

A. Experimental Design

  • The models use small, medium, and large decoders trained on CIFAR-10 for 100 epochs with randomized SNRs from 1 to 13 dB.Verification sweeps SNRs of 10, 15, 20, 25, and 30 dB; Rayleigh tests also sweep residual phase through 10°.Source: A. Experimental Design · p. 9

B. Effect of Verifier-Compatibility Changes

  • Replacing PReLU with ReLU reduced PSNR by 1.78, 2.01, and 2.22 dB for small, medium, and large models; upsample-then-convolution changed PSNR by at most 0.35 dB.The upsample-then-convolution substitution also changed MAE by under 7% at every size.Source: B. Effect of Verifier-Compatibility… · p. 9

C. Certified Robustness Across Channel Models

  • Rayleigh-trained models had PSNR reductions of 0.22, 0.47, and 0.43 dB for small, medium, and large models, respectively.The medium model's PSNR was within 1.6 dB of large under AWGN and 1.8 dB under Rayleigh fading.Source: C. Certified Robustness Across Channel… · p. 10
  • At 30 dB under AWGN, certified MAE upper bounds were 0.10 for small, 0.19 for medium, and above 1 for large models; added phase uncertainty loosened bounds.For small at 30 dB, the bound rose from 0.10 at 0° residual phase to 0.59 at 10°.Source: C. Certified Robustness Across Channel… · pp. 10–11
  • For the small model at the highest tested SNR, increasing residual phase error from a perfect estimate to 10° raised y from 0.10 to 0.59, an approximate sixfold increase.Source: C. Certified Robustness Across Channel… · p. 11
  • At high SNR, residual phase-estimation accuracy, rather than increased transmit power, determines certificate strength because the fading radius remains independent of SNR.The small model's bound rose from 0.10 to 0.59 as residual phase error increased to 10°.Source: C. Certified Robustness Across Channel… · p. 11

D. Effect of GloRo Training on Certified Robustness

The experiments compare GloRo training and structural fading encoding, then test the full pipeline's safety certificates and their transfer to an SDR radio link. Structural encoding and GloRo together increase certified-safe cases, and the measured radio errors remain below the reported bounds.

D. Effect of GloRo Training on Certified Robustness

  • For the large model, GloRo reduced the certified MAE upper bound from above 1 to 0.85 at 10 dB and 0.08 at 30 dB.For the small model at 30 dB, naive and GloRo bounds were both approximately 0.10 because the noise region dominated.Source: D. Effect of GloRo Training on… · p. 11

E. Joint Verification of the Fading Coefficient

  • Structural encoding lowered pooled certified-bound medians from 0.28 to 0.19 for small, 0.43 to 0.27 for medium, and 0.46 to 0.27 for large models.It replaces 2k interval inputs with a single affine layer over two real variables.Source: E. Joint Verification of the Fading… · p. 12

F. Certified Safety Count of the Full Pipeline

  • 192 safe cases were certified with GloRo and structural encoding, compared with 19 using GloRo and interval encoding.Naive training certified no instances under either encoding in the tested configurations.Source: F. Certified Safety Count of the Full… · p. 12

G. Over-the-Air Transfer to SDR

  • The worst of 300 over-the-air frames had MAE 0.0824, below the largest certified bound of 0.1278.The certificate held for every tested class; the observations were from one representative image per class.Source: G. Over-the-Air Transfer to SDR · p. 13
  • The certificate applies only while the link remains within the SNR and phase envelope measured by pilot signals; operation outside that envelope requires a new certificate.The experiments evaluated ten fixed images, one per CIFAR-10 class, rather than the full test set.Source: G. Over-the-Air Transfer to SDR · p. 13

VI. Related Work

Bound-propagation verifiers provide the paper’s foundation, while prior wireless verification targets different properties and does not address the decoder’s key components. The conclusion presents reformulations for those components, reports certification and radio-test results, and identifies transformer-based successors as future work.

A. Neural Network Verifiers

  • Bound propagation soundly over-approximates layers with linear relaxations and back-substitutes them; existing tools lack native PReLU and transposed-convolution support.The paper builds on this verifier family, whose methods optimize relaxation slopes.Source: A. Neural Network Verifiers · p. 14

B. Applications of DNN Verification

  • Prior wireless verification covers discrete decisions or single continuous quantities, whereas this work certifies continuous reconstruction under AWGN and Rayleigh fading.The cited prior work does not address PReLU, transposed convolutions, or shared-fading interval blow-up.Source: B. Applications of DNN Verification · p. 14

VII. Conclusion

  • The conclusion reformulates PReLU, transposed convolution, and shared fading for bound propagation without sacrificing reconstruction quality; structural encoding strengthens certificates.The certificate is reported to remain valid under real radio conditions.Source: §VII · p. 14
  • 215.6 to 25.5: GloRo lowers the large decoder’s Lipschitz constant; its MAE upper bound falls from above 1 at every SNR to 0.08, while radio error is 0.082 against certified bound 0.128.The over-the-air result spans ten CIFAR-10 classes.Source: §VII · p. 14
  • Applying the approach to attention-based, rate-adaptive successors and non-image modalities remains open; transformer attention requires abstract domains beyond this work’s relaxations.The conclusion names WITT and SwinJSCC as examples of successors.Source: §VII · p. 14
Loading 2610.11994v1…