🤖 AI

Neural Network Verification for Deep Joint Source-Channel Coding

Este artículo introduce el primer marco de propagación de límites para la verificación formal de decodificadores de Codificación Conjunta Fuente-Canal Profunda (DeepJSCC) frente a perturbaciones adversarias y de canal, extendiendo las técnicas de verificación para manejar componentes específicos del decodificador como PReLU y desvanecimiento de Rayleigh, y combinando la codificación estructural con el entrenamiento con regularización de Lipschitz para estrechar significativamente los límites de error certificados y validarlos en hardware del mundo real.

Autores originales: Thanh Le, Hai Duong, Takeshi Matsumura, ThanhVu Nguyen

Publicado 2026-10-09

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Thanh Le, Hai Duong, Takeshi Matsumura, ThanhVu Nguyen

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un mundo donde la forma en que enviamos imágenes por el aire ya no sea un proceso rígido de dos pasos de comprimir una imagen y luego protegerla de la estática. En su lugar, un sistema inteligente único aprende a hacer ambas cosas a la vez, traduciendo una foto directamente en ondas de radio y viceversa. Esta es la promesa de una tecnología llamada codificación conjunta fuente-canal profunda. Actúa como una red neuronal que ha aprendido el lenguaje del propio aire, adaptándose al ruido y a las interferencias sin necesidad de un kit de reparación manual separado. Pero debido a que estos sistemas se construyen mediante el aprendizaje en lugar de reglas de ingeniería estrictas, pueden comportarse de manera impredecible. Si la señal de radio se distorsiona de una forma que el sistema no ha visto antes, la imagen que reconstruye podría no ser solo borrosa; podría ser peligrosamente errónea. Para un coche autónomo que depende de una transmisión de cámara o un robot de fábrica que lee un sensor, una imagen mal interpretada podría provocar un choque o un mal funcionamiento. La pregunta crítica para los ingenieros no es solo qué tan bien funcionan estos sistemas en promedio, sino qué tan mal pueden fallar en el peor escenario posible.

Hasta ahora, no había una forma fiable de responder a esa pregunta para estos sistemas de radio neuronal. Los métodos tradicionales pueden probar un sistema miles de veces para encontrar fallos individuales, pero no pueden probar que un fallo nunca ocurrirá bajo un tipo específico de interferencia. Esto es como probar un puente conduciendo coches sobre él repetidamente; puedes encontrar un punto débil, pero no puedes garantizar matemáticamente que resistirá ante cualquier peso y velocidad del viento. Los investigadores necesitaban una forma de verificar formalmente el sistema, de calcular un límite estricto de cuánto podría degradarse la calidad de la imagen, asegurando que incluso en la peor tormenta de estática, la imagen siga siendo lo suficientemente segura para su uso.

Un equipo de investigadores ha construido ahora el primer marco capaz de realizar este control riguroso sobre la codificación conjunta fuente-canal profunda. Desarrollaron un método para rastrear la trayectoria de una señal distorsionada a través de la red neuronal y calcular un límite superior garantizado de error. Esto significa que ahora pueden decir con certeza que, sin importar cómo se desordene la señal dentro de un rango definido, la imagen reconstruida no será peor que una cantidad específica y mensurable. Para lograr esto, el equipo tuvo que resolver tres obstáculos específicos que previamente habían bloqueado las herramientas de verificación estándar. El primer obstáculo fue un tipo de interruptor matemático dentro de la red que se comporta de forma ligeramente distinta a los interruptores estándar utilizados en la mayoría de la inteligencia artificial. El segundo fue una forma específica en que la red expande pequeños puntos de datos en imágenes más grandes, un paso que las herramientas existentes no podían analizar directamente. El tercero, y quizás el más complejo, involucró la naturaleza misma de las ondas de radio. Cuando una señal viaza por el aire, a menudo sufre un fenómeno llamado desvanecimiento (fading), donde la señal completa rota ligeramente en fase, como un trompo tambaleándose. Las herramientas de verificación estándar trataban cada parte de la señal como si se tambaleara de forma independiente, lo que creaba una estimación del error masiva y excesivamente pesimista. Los investigadores se dieron cuenta de que, debido a que toda la señal se tambalea junta como una sola unidad, podían modelar este movimiento compartido directamente, ajustando dramente la estimación del error potencial.

Para probar su nuevo enfoque, los investigadores lo aplicaron a un sistema diseñado para transmitir imágenes, específicamente utilizando un conjunto de datos de diez categorías comunes como aviones, gatos y camiones. Primero entrenaron el sistema para que fuera robusto, ajustando sus configuraciones internas para que fuera menos sensible a pequeños cambios en la señal. Luego, ejecutaron su marco de verificación para ver si podían probar que el sistema era seguro. Los resultados fueron sorprendentes. Para una versión grande del sistema, el método redujo el error máximo estimado de un valor demasiado alto para ser útil a un número muy pequeño y manejable. Cuando combinaron su nueva forma de modelar el desvanecimiento de radio con el entrenamiento robusto, el sistema pudo certificar que era seguro en casi diez veces más situaciones que antes. En un caso de prueba específico que involucraba una incertidumbre de diez grados en la fase de la señal, el nuevo método encontró 192 escenarios seguros donde el método anterior solo encontraba 19.

El equipo no se detuvo en las simulaciones por computadora. Para demostrar que sus garantías matemáticas se mantenían en el mundo real, construyeron una prueba física utilizando radios definidas por software, que son dispositivos que pueden transmitir y recibir señales de radio utilizando software en lugar de hardware fijo. Configuraron dos de estos dispositivos para comunicarse por el aire, enviando imágenes a través de un enlace de radio real. Midieron la interferencia y los cambios de fase reales en el enlace y luego utilizaron su herramienta de verificación para calcular un límite de seguridad para ese entorno específico. Luego enviaron cientos de imágenes a través del aire y midieron los errores reales. Los resultados confirmaron la teoría: el peor error que observaron en el mundo real fue de 0.082, el cual se mantuvo cómodamente por debajo del límite de seguridad certificado de 0.128. El sistema funcionó exactamente como predijo la matemática, sin exceder nunca el límite.

Este trabajo demuestra que es posible aportar el mismo nivel de garantía de seguridad a los sistemas inalámbricos basados en redes neuronales que existe para la ingeniería tradicional. Al encontrar una forma de modelar la naturaleza compartida del desvanecimiento de radio y adaptar las herramientas de verificación para manejar los componentes específicos de estas redes, los investigadores han abierto la puerta al uso de estos poderosos y adaptativos sistemas en aplicaciones de seguridad crítica. Han demostrado que ahora podemos saber, con certeza matemática, los límites de estos sistemas, asegurando que incluso cuando el aire esté lleno de ruido, el mensaje llegue con la claridad suficiente para ser confiable.

Resumen Técnico: Verificación de Redes Neuronales para el Codificado Conjunto Fuente-Canal Profundo

1. Planteamiento del Problema

El Codificado Conjunto Fuente-Canal Profundo (DeepJSCC) utiliza pares de codificador-decodificador neuronales para transmitir datos de extremo a extremo sobre canales inalámbricos, reemplazando las etapas tradicionales de compresión y codificación separadas. Aunque es efectivo para el rendimiento promedio, los sistemas DeepJSCC carecen de garantías formales con respecto a la calidad de la reconstrucción bajo perturbaciones del canal en el peor de los casos. En aplicaciones de misión crítica (por ejemplo, vehículos autónomos, IoT industrial), una reconstrucción corrupta puede conducir a decisiones erróneas catastróficas.

Las herramientas actuales de Verificación de Redes Neuronales (NNV), que delimitan formalmente el comportamiento en el peor de los casos, no pueden verificar los decodificadores DeepJSCC debido a tres desajustes arquitectónicos y ambientales específicos:

Activaciones PReLU: Los decodificadores DeepJSCC emplean Unidades Rectificadas Paramétricas (PReLU) para aprender pendientes en el lado negativo. Los verificadores estándar solo admiten ReLU (pendiente cero fija). Reemplazar PReLU con ReLU degrada la calidad de la reconstrucción entre 1.78 y 2.22 dB.
Convoluciones Transpuestas: El decodificador utiliza convoluciones transpuestas para el sobremuestreo (upsampling), un tipo de capa que no es soportado nativamente por las herramientas de propagación de límites de vanguardia como $\alpha$ -Crown.
Estructura de Desvanecimiento Rayleigh: Bajo desvanecimiento Rayleigh, todos los símbolos latentes comparten una única rotación de fase residual. La verificación de intervalos estándar trata el ruido de cada símbolo de forma independiente, lo que provoca que el intervalo de entrada se expanda a un hipercubo de $2k$ dimensiones. Este "estallido de intervalo" (interval blow-up) hace que los límites de verificación sean vacuos (inútiles) para espacios latentes de alta dimensión.

Además, los modelos DeepJSCC existentes se entrenan únicamente para minimizar el error promedio, careciendo de la continuidad de Lipschitz necesaria para producir límites certificables y ajustados.

2. Metodología

Los autores proponen un marco de propagación de límites adaptado específicamente para DeepJSCC, combinando modificaciones estructurales al decodificador con un procedimiento de entrenamiento consciente de la robustez.

A. Adaptaciones de Verificación

Para hacer que el decodificador DeepJSCC sea compatible con los verificadores de propagación de límites existentes (específicamente $\alpha$ -Crown), los autores introducen tres reformas técnicas:

Relajación de PReLU: Los autores extienden la optimización de la relajación lineal de $\alpha$ -Crown para acomodar PReLU. En lugar de fijar la pendiente del límite inferior en 0 (como en ReLU), la relajación permite que la pendiente $\alpha$ varíe dentro de $[a, 1]$ , donde $a$ es la pendiente negativa aprendida de la capa PReLU. Esto preserva la solidez del límite sin sacrificar la calidad de reconstrucción obtenida al aprender $a$ .
Sustitución de Convolución Transpuesta: Los autores demuestran que una convolución transpuesta con un paso (stride) $s$ es matemáticamente equivalente a un sobremuestreo de vecino más cercano seguido de una convolución estándar con un kernel específico. Sustituyen las capas de convolución transpuesta por esta estructura de "sobremuestreo-luego-convolución". Esto permite el uso de reglas de relajación de convolución estándar, incurriendo en una pérdida insignificante en la Relación Señal-Ruido de Pico (PSNR) de máximo 0.35 dB.
Propiedad de Entrada de Rayleigh Estructural: Para abordar el estallido de intervalo causado por el desvanecimiento compartido, los autores modelan el canal de desvanecimiento como una capa lineal prevenida al decodificador. En lugar de acotar $k$ símbolos complejos independientes, el verificador acota las dos coordenadas reales del coeficiente de desvanecimiento complejo único $h$ (donde $\hat{s} = hs + n$ ). Esto reduce la dimensionalidad de la entrada de $k$ intervalos a solo 2 grados de libertad, permitiendo que el verificador rastree exactamente la restricción estructural de la rotación de fase compartida.

B. Instanciación de GloRo

Para asegurar que los límites sean lo suficientemente ajustados como para ser útiles, los autores aplican el entrenamiento GloRo (Robustez Global). Añaden una penalización de regularización de Lipschitz a la función de pérdida de entrenamiento, apuntando a la constante de Lipschitz del decodificador ( $K_D$ ).

La penalización se deriva del radio de la propiedad de la entrada, que tiene en cuenta tanto el Ruido Blanco Gaussiano Aditivo (AWGN) como la incertidumbre de fase residual en el desvanecimiento Rayleigh.
Este proceso de ajuste fino reduce la sensibilidad global del decodificador, asegurando que las pequeñas perturbaciones de la entrada (ruido del canal) no resulten en errores de salida desproporcionadamente grandes.

3. Contribuciones Clave

El artículo reclama cuatro contribuciones primarias:

Relajación de PReLU: Una extensión sólida de la relajación lineal de $\alpha$ -Crown que generaliza la verificación de ReLU a PReLU, preservando la ganancia de PSNR de 1.78–2.22 dB de PReLU sobre ReLU.
Sustitución de Sobremuestreo-luego-Convolución: Una prueba de que las convoluciones transpuestas pueden reemplazarse por una forma restringida de sobremuestreo-convolución, permitiendo el soporte nativo en $\alpha$ -Crown con una pérdida de rendimiento mínima (<0.35 dB).
Entrada de Rayleigh Estructural: Un método para formular el desvanecimiento Rayleigh como una perturbación estructural (una capa lineal), reduciendo la dimensión de verificación de la entrada de $2k$ a 2, lo que ajusta significativamente los límites certificados.
GloRo para DeepJSCC: La primera instanciación del entrenamiento regularizado por Lipschitz para decodificadores DeepJSCC, proporcionando radios de forma cerrada para canales AWGN y Rayleigh, permitiendo la certificación de modelos que antes eran no verificables.

4. Resultados Experimentales

Los autores evaluaron su marco en modelos DeepJSCC (Pequeño, Mediano, Grande) entrenados en CIFAR-10, utilizando tanto canales AWGN como de desvanecimiento Rayleigh.

Calidad de Reconstrucción: Los cambios de compatibilidad con el verificador (relajación de PReLU y sustitución de upsample-conv) preservaron la calidad de la reconstrucción. Reemplazar PReLU con ReLU causó una caída de 1.78–2.22 dB, mientras que la relajación de PReLU propuesta mantuvo el rendimiento original. La sustitución de upsample-conv resultó en un cambio de PSNR de menos de 0.35 dB.
Reducción de Lipschitz: El entrenamiento GloRo redujo la constante de Lipschitz del decodificador grande de 215.6 a 25.5. Esta reducción fue crítica; sin GloRo, el límite de Error Absoluto Medio (MAE) certificado permanecía por encima de 1.0 para todas las Relaciones Señal-Ruido (SNR), lo que hacía que el modelo no fuera certificable. Con GloRo, el límite cayó a 0.08 a 30 dB de SNR.
Impacto de la Codificación Estructural: La codificación estructural del coeficiente de desvanecimiento mejoró significativamente la certificación. Con una incertidumbre de fase de 10 grados ( $\delta=10^\circ$ ), la codificación estructural redujo el límite certificado mediano hasta en un 41% en comparación con la codación de intervalo. Certificó 192 casos seguros frente a solo 19 de la codificación de intervalo (una ganancia de 10 $\times$ ).
Validación Sobre el Aire (Over-the-Air): Los autores validaron los certificados en hardware real utilizando dos transceptores ADALM-PlutoSDR.
- Condiciones: SNR de operación de 27.4 dB y fase residual $\delta=5.4^\circ$ .
- Resultado: El peor MAE observado a través de 300 tramas (10 clases de CIFAR-10 $\times$ 30 transmisiones) fue de 0.082. El límite superior certificado fue de 0.128.
- Conclusión: El error en el mundo real se mantuvo estrictamente dentro del límite teórico, confirmando que el certificado se sostiene en enlaces de radio físicos.

5. Significación y Reivindicaciones

El artículo posiciona su marco como el primer marco de propagación de límites capaz de verificar formalmente los decodificadores DeepJSCC bajo modelos de canales inalámbricos físicos.

Fiabilidad: Aborda la preocupación de fiabilidad de la "caja negra" de DeepJSCC en escenarios críticos de seguridad mediante la provisión de garantías formales sobre el error de reconstrucción en el peor de los casos, en lugar de depender de pruebas de muestra finita que no pueden garantizar la ausencia de fallos.
Viabilidad: El trabajo demuestra que la verificación formal es viable para arquitecturas neuronales complejas y no estándar (PReLU, convoluciones transpuestas) y modelos de canales físicos (desvanecimiento Rayleigh) sin sacrificar los beneficios de rendimiento de la arquitectura original.
Validez de Hardware: La validación sobre el aire es una afirmación significativa, cerrando la brecha entre la verificación teórica y la realidad física. Los autores afirman que el certificado derivado del modelo de canal restringe con precisión el comportamiento de la implementación de hardware.
Complementariedad: Los resultados resaltan que el entrenamiento de robustez (GloRo) y la codificación estructural son complementarios; GloRo aborda la amplificación de errores del decodificador, mientras que la codificación estructural aborda la expansión de la entrada del canal. Ambos son necesarios para una certificación efectiva en entornos de alta dimensión y desvanecimiento.

Los autores concluyen que, si bien su enfoque actualmente se aplica a DeepJSCC convolucional, el trabajo futuro debe abordar los sucesores basados en atención (por ejemplo, WITT), que requieren dominios de abstracción más allá de las relajaciones actuales de PReLU/ReLU.