Resumen Técnico: Verificación de Redes Neuronales de Punto Flotante a Nivel de Software
Planteamiento del Problema
Si bien la verificación de redes neuronales ha avanzado significamente al proporcionar garantías formales para modelos idealizados de números reales, estos enfoques a menudo no logran considerar los detalles de implementación específicos de los sistemas desplegados. En aplicaciones críticas para la seguridad (p. ej., CPS, IoT), las redes neuronales se implementan utilizando aritmética de punto flotante de precisión finita (típicamente IEEE 754 de 32 bits) y dependen de bibliotecas matemáticas estándar (p. ej., math.h). Estos detalles de bajo nivel introducen errores de redondeo y comportamientos no asociativos que pueden invalidar las pruebas de seguridad derivadas de modelos de precisión infinita. Por ejemplo, el documento demuestra que la función de activación SoftSign, que es no decreciente en aritmética de números reales, deja de serlo cuando se implementa en punto flotante de 32 bits.
Los intentos existentes de verificar el código de redes neuronales a nivel de software han arrojado resultados mixtos. Los verificadores de software suelen tener dificultades para escalar a instancias de redes neuronales grandes, lo que obliga a los profesionales a recurrir a modelos de precisión infinita no consistentes con la realidad o a abandonar la verificación en favor de las pruebas. Además, se ha observado que las herramientas existentes producen resultados incorrectos en ciertas configuraciones, lo que genera dudas sobre su fiabilidad como oráculos de seguridad para implementaciones de punto flotante. Existe una falta de evaluación rigurosa y estandarizada de los verificadores de software automatizados específicamente en código de redes neuronales.
Metodología
Para abordar estas brechas, los autores realizaron una evaluación rigurosa de ocho verificadores de software automatizados de vanguardia en código de redes neuronales. La metodología consistió en tres componentes principales:
Construcción de Benchmarks (NeuroCodeBench 2.0): Los autores construyeron un benchmark exhaustivo que comprende 912 ejemplos de verificación. Este benchmark cubre:
- Funciones Matemáticas: 58 instancias que prueban propiedades (p. ej., monotonicidad, periodicidad, límites lineales) de funciones estándar de
math.h.
- Funciones de Activación: 57 instancias que prueban propiedades de activaciones comunes (p. ej., ReLU, TanH, SoftSign, GELU).
- Capas Neuronales: 86 instancias que cubren transformaciones afines, normalización, capas de pooling y capas SoftMax.
- Redes Neuronales Completas: 711 instancias que incluyen redes de Hopfield, redes ReLU codificadas mediante SAT, redes de aproximación polinómica, redes con límites de Lipschitz y redes derivadas de VNN-COMP (tareas de Densidad de Probabilidad y Aprendizaje por Refuerzo).
- Verdad Fundamental (Ground Truth): Cada instancia está pre-etiquetada como "segura" o "insegura" utilizando técnicas como pruebas de fuerza bruta, construcción exhaustiva o generación de contraejemplos, asegurando un veredicto correcto conocido para la evaluación.
Estandarización y Compatibilidad: Para garantizar una comparación justa y la reproducibilidad, los autores convirtieron todas las instancias del benchmark al formato utilizado por la Competición Internacional de Verificación de Software (SV-COMP). Esto implicó la creación de archivos C autónomos que incluyen la implementación del modelo, las propiedades de seguridad y las dependencias necesarias. El flujo de trabajo utilizó el framework BenchExec para gestionar los límites de recursos y la ejecución, asegurando que las herramientas se ejecutaran con las mismas configuraciones utilizadas en la edición 2024 de SV-COMP.
Evaluación Experimental: El estudio evaluó ocho herramientas (2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer) bajo dos condiciones:
- Línea Base (Baseline): Ejecución de los verificadores en las instancias puras del benchmark.
- Modelos Operacionales: Provisión de implementaciones explícitas en C de la biblioteca
math.h (usando MUSL y CORE-MATH) para observar si el suministro de las definiciones de las funciones mejora los resultados de la verificación.
- Análisis Histórico: Los autores también analizaron el rendimiento histórico de una herramienta (ESBMC) de 2018 a 2026 para observar las tendencias en el campo.
Contribuciones Clave
- NeuroCodeBench 2.0: La creación de un benchmark a gran escala con verdad fundamental diseñado específicamente para la verificación a nivel de software de redes neuronales de punto flotante. Incluye 912 instancias que van desde funciones simples hasta redes completas con hasta 170K parámetros.
- Integración con SV-COMP: El benchmark fue formateado para ser compatible con la infraestructura de SV-COMP, lo que lo convierte en parte del conjunto de benchmarks oficiales para la edición de 2026. Esto permite una evaluación automatizada y reproducible utilizando configuraciones de herramientas estándar.
- Evaluación Rigurosa: El primer estudio sistemático que compara ocho verificadores de software de vanguardia en código de redes neuronales, revelando una varianza significativa en el rendimiento y la corrección.
- Análisis de Modelos Operacionales: Una investigación sobre si el suministro de implementaciones explícitas de bibliotecas matemáticas (MUSL, CORE-MATH) mejora el rendimiento del verificador, encontrando que el impacto depende de la herramienta y suele ser insignificante o negativo.
Resultados
La evaluación arrojó varios hallazgos críticos sobre el estado actual de la verificación de software para redes neuronales:
- Baja Corrección y Escalabilidad: Los resultados fueron descritos como "bastante decepcionantes". Las herramientas exhibieron una gran varianza a través del benchmark; la mejor herramienta (CBMC) resolvió correctamente 371 de 912 instancias, mientras que otras resolvieron significativamente menos. La tasa de solución promedio por categorías varió, con algunas categorías complejas (p. ej., Aprendizaje por Refuerzo) mostrando tasas de solución de tan solo el 3%. La mayoría de las herramientas no pudieron verificar más de una sola capa neuronal a la vez.
- Veredictos Incorrectos: Varias herramientas produjeron una alta tasa de resultados incorrectos. Por ejemplo, CBMC produjo casi un 25% de veredictos definitivos incorrectos (principalmente falsos positivos), y Pinaka y UAutomizer también mostraron tasas de error significativas. Solo ESBMC no produjo veredictos incorrectos entre las herramientas que resolvieron un número sustancial de instancias.
- Impacto de los Modelos Operacionales: El suministro de implementaciones explícitas de
math.h (MUSL o CORE-MATH) no condujo a mejoras visibles en general. Para algunas herramientas (CBMC, ESBMC, Pinaka), el rendimiento disminuyó debido a la complejidad añadida de verificar el código de la biblioteca. Para otras (CPAChecker, PeSCo), el número de instancias resueltas aumentó, pero esto a menudo vino acompañado de un aumento en los veredictos incorrectos.
- Límites de Escalabilidad: Las herramientas tuvieron dificultades significativas con las redes neuronales completas. La tasa de solución cayó a dígitos únicos para categorías complejas como Aprendizaje por Refuerzo y Densidad de Probabilidad. Incluso para redes sintéticas, herramientas como ESBMC solo pudieron resolver instancias con anchuras muy pequeñas (p. ej., anchura 4) antes de agotar el tiempo de ejecución.
- Progreso Histórico: El análisis de ESBMC de 2018 a 2026 mostró mejoras no monotónicas pero generalmente constantes. Un pico notable de veredictos incorrectos en 2022-2023 se atribuyó a un error de implementación en un algoritmo de k-inducción, el cual fue corregido tras el lanzamiento de NeuroCodeBench 1.0. La introducción de NeuroCodeBench 1.0 en 2024 condujo a una reducción drástica de los veredictos incorrectos en toda la comunidad, aunque el impacto de NeuroCodeBench 2.0 (finales de 2025) fue más moderado.
Significado y Reivindicaciones
El artículo sostiene que, si bien la verificación de redes neuronales a nivel de software es conceptualmente factible, los verificadores de software de vanguardia actuales aún no están listos para manejar esta tarea de manera efectiva. El estudio destaca que las herramientas actuales no pueden verificar de manera fiable más de una sola capa, devuelven resultados incorrectos con frecuencia y carecen de soporte completo para las bibliotecas matemáticas estándar.
Los autores argumentan que su trabajo sirve como un necesario "baño de realidad" para la comunidad de verificación. Al proporcionar un benchmark riguroso con verdad fundamental conocida, demuestran que la brecha entre la verificación idealizada y la implementación de software es actualmente demasiado amplia para que las herramientas existentes la cierren sin mejoras significativas. El documento plantea que el lanzamiento de NeuroCodeBench ya ha estimulado el progreso, como lo demuestra la reducción de los veredictos incorrectos tras su lanzamiento inicial. Sin embargo, los autores concluyen que certificar la implementación completa de las redes neuronales contra desviaciones numéricas extremas sigue siendo un desafío a largo plazo que requiere soporte nativo para bibliotecas matemáticas y procedimientos de decisión personalizados adaptados a la aritmética de punto flotante.