🤖 AI

Neural Network Verification for Deep Joint Source-Channel Coding

Cet article introduit le premier cadre de propagation de bornes pour la vérification formelle des décodeurs de codage source-canal conjoint profond (DeepJSCC) contre les perturbations adverses et de canal en étendant les techniques de vérification pour gérer des composants spécifiques du décodeur tels que PReLU et l'évanouissement de Rayleigh, et en combinant l'encodage structurel avec un entraînement régularisé par Lipschitz pour resserrer considérablement les bornes d'erreur certifiées et les valider sur du matériel réel.

Auteurs originaux : Thanh Le, Hai Duong, Takeshi Matsumura, ThanhVu Nguyen

Publié 2026-10-09

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Thanh Le, Hai Duong, Takeshi Matsumura, ThanhVu Nguyen

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez un monde où la façon dont nous envoyons des images par les ondes n'est plus un processus rigide en deux étapes consistant à compresser une image puis à la protéger contre les parasites. Au lieu de cela, un système intelligent unique apprend à faire les deux à la fois, traduisant directement une photo en ondes radio et inversement. C'est la promesse d'une technologie appelée codage conjoint source-canal profond. Elle agit comme un réseau de neurones qui a appris le langage même de l'air, s'adaptant au bruit et aux interférences sans avoir besoin d'un kit de réparation manuel distinct. Mais parce que ces systèmes sont construits par apprentissage plutôt que par des règles d'ingénierie strictes, ils peuvent se comporter de manière imprévisible. Si le signal radio est déformé d'une manière que le système n'a pas encore rencontrée, l'image qu'il reconstruit pourrait ne pas être simplement floue ; elle pourrait être dangereusement erronée. Pour une voiture autonome s'appuyant sur un flux de caméra ou un robot d'usine lisant un capteur, une image mal interprétée pourrait entraîner un accident ou un dysfonctionnement. La question cruciale pour les ingénieurs n'est pas seulement de savoir comment ces systèmes fonctionnent en moyenne, mais à quel point ils peuvent échouer dans le pire scénario possible.

Jusqu'à présent, il n'existait aucun moyen fiable de répondre à cette question pour ces systèmes radio neuronaux. Les méthodes traditionnelles peuvent tester un système des milliers de fois pour trouver des défaillances individuelles, mais elles ne peuvent pas prouver qu'une défaillance ne se produira jamais sous un type d'interférence spécifique. C'est comme tester un pont en faisant passer des voitures dessus de manière répétée ; vous pouvez trouver un point faible, mais vous ne pouvez pas garantir mathématiquement qu'il résistera à chaque poids et vitesse de vent. Les chercheurs avaient besoin d'un moyen de vérifier formellement le système, de calculer une limite absolue sur la dégradation de la qualité de l'image, afin de garantir que même dans la pire tempête de parasites, l'image reste suffisamment sûre pour être utilisée.

Une équipe de chercheurs a maintenant construit le premier cadre capable d'effectuer ce contrôle rigoureux sur le codage conjoint source-canal profond. Ils ont développé une méthode pour tracer le chemin d'un signal déformé à travers le réseau de neurones et calculer une limite supérieure garantie sur l'erreur. Cela signifie qu'ils peuvent désormais affirmer avec certitude que, peu importe la façon dont le signal est brouillé dans une plage définie, l'image reconstruite ne sera pas pire qu'un certain montant mesurable. Pour rendre cela possible, l'équipe a dû surmonter trois obstacles spécifiques qui bloquaient auparavant les outils de vérification standards. Le premier obstacle était un type de commutateur mathématique à l'intérieur du réseau qui se comporte légèrement différemment des commutateurs standards utilisés dans la plupart des intelligences artificielles. Le deuxième était une manière spécifique dont le réseau étend de petits points de données en images plus larges, une étape que les outils existants ne pouvaient pas analyser directement. Le troisième, et peut-être le plus complexe, concernait la nature même des ondes radio. Lorsqu'un signal voyage à travers l'air, il subit souvent un phénomène appelé évanouissement (fading), où l'ensemble du signal subit une légère rotation de phase, comme une toupie qui vacille. Les outils de vérification standards traitaient chaque partie du signal comme si elle vacillait indépendamment, ce qui créait une estimation de l'erreur massive et excessivement pessimiste. Les chercheurs ont réalisé que, puisque l'ensemble du signal vacille ensemble comme une seule unité, ils pouvaient modéliser ce mouvement partagé directement, resserrant ainsi considérablement l'estimation de l'erreur potentielle.

Pour tester leur nouvelle approche, les chercheurs l'ont appliquée à un système conçu pour transmettre des images, utilisant spécifiquement un ensemble de données de dix catégories communes comme les avions, les chats et les camions. Ils ont d'abord entraîné le système pour qu'il soit robuste, en ajustant ses paramètres internes afin qu'il soit moins sensible aux petites variations du signal. Ensuite, ils ont utilisé leur cadre de vérification pour voir s'ils pouvaient prouver que le système était sûr. Les résultats ont été frappants. Pour une version étendue du système, la méthode a réduit l'erreur de pire cas estimée — une valeur trop élevée pour être utile — à un nombre très petit et gérable. Lorsqu'ils ont combiné leur nouvelle façon de modéliser l'évanouissement radio avec l'entraînement robuste, le système a pu certifier qu'il était sûr dans près de dix fois plus de situations qu'auparavant. Dans un cas de test spécifique impliquant une incertitude de dix degrés dans la phase du signal, la nouvelle méthode a trouvé 192 scénarios sûrs là où l'ancienne méthode n'en trouvait que 19.

L'équipe ne s'est pas arrêtée aux simulations informatiques. Pour prouver que leurs garanties mathématiques tenaient bon dans le monde réel, ils ont construit un test physique utilisant des radios définies par logiciel (SDR), qui sont des disposités capables de transmettre et de recevoir des signaux radio en utilisant des logiciels plutôt que du matériel fixe. Ils ont installé deux de ces dispositifs pour communiquer par les ondes, envoyant des images via une liaison radio réelle. Ils ont mesuré les interférences réelles et les déphasages sur la liaison, puis ont utilisé leur outil de vérification pour calculer une borne de sécurité pour cet environnement spécifique. Ils ont ensuite envoyé des centaines d'images à travers les ondes et mesuré les erreurs réelles. Les résultats ont confirmé la théorie : la pire erreur observée dans le monde réel était de 0,082, ce qui restait confortablement en dessous de la limite de sécurité certifiée de 0,128. Le système s'est comporté exactement comme la mathématique le prédisait, ne dépassant jamais la borne.

Ce travail démontre qu'il est possible d'apporter le même niveau d'assurance de sécurité aux systèmes sans fil basés sur les réseaux de neurones qu'à l'ingénierie traditionnelle. En trouvant un moyen de modéliser la nature partagée de l'évanouissement radio et en adaptant les outils de vérification pour gérer les composants spécifiques de ces réseaux, les chercheurs ont ouvert la voie à l'utilisation de ces systèmes puissants et adaptatifs dans des applications critiques pour la sécurité. Ils ont montré que nous pouvons désormais connaître, avec une certitude mathématique, les limites de ces systèmes, garantissant que même lorsque l'air est saturé de bruit, le message parvient assez clairement pour être fiable.

Résumé Technique : Vérification de Réseaux de Neurones pour le Codage Conjoint Source-Canal Profond

1. Énoncé du Problème

Le codage conjoint source-canal profond (DeepJSCC) utilise des paires encodeur-décodeur neuronales pour transmettre des données de bout en bout sur des canaux sans fil, remplaçant ainsi les étapes traditionnelles de compression et de codage séparées. Bien qu'efficaces pour la performance moyenne, les systèmes DeepJSCC manquent de garanties formelles concernant la qualité de la reconstruction face aux perturbations de canal les plus défavorables (worst-case). Dans les applications critiques (ex. : véhicules autonomes, IoT industriel), une reconstruction corrompue peut entraîner des décisions en aval catastrophiques.

Les outils actuels de vérification de réseaux de neurones (NNV), qui borne formellement le comportement dans le pire des cas, ne peuvent pas vérifier les décodeurs DeepJSCC en raison de trois décalages architecturaux et environnementaux spécifiques :

Activations PReLU : Les décodeurs DeepJSCC utilisent des unités rectifiées paramétriques (PReLU) pour apprendre les pentes du côté négatif. Les vérificateurs standards ne supportent que le ReLU (pente nulle fixe). Le remplacement de PReLU par ReLU dégrade la qualité de la reconstruction de 1,78 à 2,22 dB.
Convolutions Transposées : Le décodeur utilise des convolutions transposées pour l'upsampling, un type de couche qui n'est pas nativement supporté par les outils de propagation de bornes de pointe comme $\alpha$ -Crown.
Structure de l'Évanouissement de Rayleigh : Sous un évanouissement de Rayleigh, tous les symboles latents partagent une rotation de phase résiduelle unique. La vérification par intervalles standard traite le bruit de chaque symbole indépendamment, ce qui fait que l'intervalle d'entrée s'étend vers un hypercube de dimension $2k$ . Ce « gonflement d'intervalle » rend les bornes de vérification vacues (inutiles) pour les espaces latents de haute dimension.

De plus, les modèles DeepJSCC existants sont entraînés uniquement pour minimiser l'erreur moyenne, manquant de la continuité de Lipschitz requise pour produire des bornes certifiables et serrées.

2. Méthodologie

Les auteurs proposent un cadre de propagation de bornes spécifiquement adapté au DeepJSCC, combinant des modifications structurelles du décodeur avec une procédure d'entraînement sensible à la robustesse.

A. Adaptations de la Vérification

Pour rendre le décodeur DeepJSCC compatible avec les vérificateurs de propagation de bornes existants (spécifiquement $\alpha$ -Crown), les auteurs introduisent trois réformes techniques :

Relaxation PReLU : Les auteurs étendent l'optimisation de la relaxation linéaire d' $\alpha$ -Crown pour accommoder le PReLU. Au lieu de fixer la pente de la borne inférieure à 0 (comme pour le ReLU), la relaxation permet à la pente $\alpha$ de varier dans $[a, 1]$ , où $a$ est la pente négative apprise de la couche PReLU. Cela préserve la validité de la borne sans sacrifier la qualité de reconstruction gagnée par l'apprentissage de $a$ .
Substitution par Convolution Transposée : Les auteurs prouvent qu'une convolution transposée avec un pas (stride) $s$ est mathématiquement équivalente à un upsampling par plus proche voisin suivi d'une convolution standard avec un noyau spécifique. Ils substituent les couches de convolution transposée par cette structure « upsample-puis-convolution ». Cela permet l'utilisation des règles de relaxation de convolution standard, n'entraînant une perte négligeable du rapport signal sur bruit de crête (PSNR) d'au plus 0,35 dB.
Propriété Structurelle d'Entrée de Rayleigh : Pour traiter le gonflement d'intervalle causé par l'évanouissement partagé, les auteurs modélisent le canal d'évanouissement comme une couche linéaire prépendue au décodeur. Au lieu de borner $k$ symboles complexes indépendants, le vérificateur borne les deux coordonnées réelles du coefficient de fading complexe unique $h$ (où $\hat{s} = hs + n$ ). Cela réduit la dimensionnalité de l'entrée de $k$ intervalles à seulement 2 degrés de liberté, permettant au vérificateur de suivre exactement la contrainte structurelle de la rotation de phase partagée.

B. Instanciation de GloRo

Pour garantir que les bornes soient suffisamment serrées pour être utiles, les auteurs appliquent l'entraînement GloRo (Global Robustness). Ils ajoutent une pénalité de régularisation de Lipschitz à la fonction de perte d'entraînement, ciblant la constante de Lipschitz du décodeur ( $K_D$ ).

La pénalité est dérivée du rayon de la propriété de l'entrée, qui prend en compte à la fois le bruit blanc gaussien additif (AWGN) et l'incertitude de phase résiduelle dans l'évanouissement de Rayleigh.
Ce processus de réglage fin réduit la sensibilité globale du décodeur, garantissant que de petites perturbations d'entrée (bruit de canal) ne produisent pas des erreurs de sortie disproportionnées.

3. Contributions Clés

Le papier revendique quatre contributions principales :

Relaxation PReLU : Une extension robuste de la relaxation linéaire d' $\alpha$ -Crown qui généralise la vérification ReLU au PReLU, préservant le gain de PSNR de 1,78–2,22 dB du PReLU par rapport au ReLU.
Substitution Upsample-then-Convolution : Une preuve que les convolutions transposées peuvent être remplacées par une forme upsampling-convolution restreinte, permettant le support natif dans $\alpha$ -Crown avec une perte de performance minimale (<0,35 dB).
Entrée de Rayleigh Structurelle : Une méthode pour formuler l'évanouissement de Rayleigh comme une perturbation structurelle (une couche linéaire), réduisant la dimension de vérification de l'entrée de $2k$ à 2, ce qui resserre considérablement les bornes certifiées.
GloRo pour DeepJSCC : La première instanciation de l'entraînement régularisé par Lipschitz pour les décodeurs DeepJSCC, fournissant des rayons en forme fermée pour les canaux AWGN et de Rayleigh, permettant la certification de modèles qui étaient auparavant invérifiables.

4. Résultats Expérimentaux

Les auteurs ont évalué leur cadre sur des modèles DeepJSCC (Small, Medium, Large) entraînés sur CIFAR-10, en utilisant des canaux AWGN et d'évanouissement de Rayleigh.

Qualité de Reconstruction : Les changements de compatibilité du vérificateur (relaxation PReLU et substitution upsample-conv) ont préservé la qualité de reconstruction. Le remplacement de PReLU par ReLU a provoqué une chute de 1,78–2,22 dB, tandis que la relaxation PReLU proposée a maintenu la performance originale. La substitution upsample-conv a entraîné un changement de PSNR de moins de 0,35 dB.
Réduction de Lipschitz : L'entraînement GloRo a réduit la constante de Lipschitz du grand décodeur de 215,6 à 25,5. Cette réduction était critique ; sans elle, la borne de l'erreur absolue moyenne (MAE) certifiée restait supérieure à 1,0 pour tous les rapports signal sur bruit (SNR), rendant le modèle non certifiable. Avec GloRo, la borne est tombée à 0,08 à 30 dB de SNR.
Impact de l'Encodage Structurel : L'encodage structurel du coefficient de fading a considérablement amélioré le succès de la certification. À une incertitude de phase de 10 degrés ( $\delta=10^\circ$ ), l'encodage structurel a abaissé la médiane de la borne certifiée jusqu'à 41 % par rapport à l'encodage par intervalle. Il a certifié 192 cas sûrs contre seulement 19 pour l'encodage par intervalle (un gain de 10 $\times$ ).
Validation Over-the-Air : Les auteurs ont validé les certificats sur du matériel réel en utilisant deux émetteurs-récepteurs ADALM-PlutoSDR.
- Conditions : SNR de fonctionnement de 27,4 dB et phase résiduelle $\delta=5,4^\circ$ .
- Résultat : La pire MAE observée sur 300 trames (10 classes CIFAR-10 $\times$ 30 transmissions) était de 0,082. La borne supérieure certifiée était de 0,128.
- Conclusion : L'erreur réelle est restée strictement à l'intérieur de la borne théorique, confirmant que le certificat tient sur des liaisons radio physiques.

5. Signification et Revendications

Le papier se positionne comme le premier cadre de propagation de bornes capable de vérifier formellement les décodeurs DeepJSCC sous des modèles de canaux sans fil physiques.

Fiabilité : Il répond à l'inquiétude de la fiabilité de la « boîte noire » des DeepJSCC dans des scénarios critiques pour la sécurité en fournissant des garanties formelles sur l'erreur de reconstruction dans le pire des cas, plutôt que de compter sur des tests à échantillon fini qui ne peuvent garantir l'absence de fautes.
Faisabilité : Ce travail démontre que la vérification formelle est réalisable pour des architectures neuronales complexes et non standard (PReLU, convolutions transposées) ainsi que pour les modèles de canaux physiques (évanouissement de Rayleigh) sans sacrifier les avantages de performance de l'architecture originale.
Validité Matérielle : La validation over-the-air est une affirmation significative, comblant le fossé entre la vérification théorique et la réalité physique. Les auteurs affirment que le certificat dérivé du modèle de canal contraint avec précision le comportement de l'implémentation matérielle.
Complémentarité : Les résultats soulignent que l'entraînement de robustesse (GloRo) et l'encodage structurel sont complémentaires ; GloRo traite l'amplification des erreurs par le décodeur, tandis que l'encodage structurel traite l'expansion de l'entrée par le canal. Les deux sont nécessaires pour une certification efficace dans des environnements de haute dimension et d'évanouissement.

Les auteurs concluent que, bien que leur approche s'applique actuellement aux DeepJSCC convolutionnels, les travaux futurs devront aborder les successeurs basés sur l'attention (ex. : WITT) qui nécessitent des domaines abstraits au-delà des relaxations PReLU/ReLU actuelles.