🤖 machine learning

VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

Este artículo presenta VNN-LIB 2.0, un estándar rigurosamente formalizado para la verificación de redes neuronales que introduce una abstracción de "teoría de redes" para desacoplar la especificación de los modelos ONNX en evolución, al tiempo que proporciona una sintaxis precisa, un sistema de tipos y una semántica mecanizados en Agda para garantizar la consistencia interna y la interoperabilidad.

Autores originales: Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

Publicado 2026-05-11

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

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 que estás intentando que un equipo de robots diferentes resuelva un rompecabezas juntos. En el mundo de la Inteligencia Artificial, estos "robots" son redes neuronales (los cerebros detrás de la IA), y el "rompecabezas" es la verificación (comprobar si la IA tomará una decisión segura o correcta).

Durante mucho tiempo, las personas que construían estos robots y las personas que los verificaban no hablaban el mismo idioma. Utilizaban un estándar llamado VNN-LIB 1.0, pero era como un diccionario con palabras faltantes, sin reglas gramaticales y con definiciones que cambiaban cada vez que alguien las miraba.

Este artículo presenta VNN-LIB 2.0, un nuevo "idioma" riguroso que soluciona estos problemas. Así es como los autores lo explican utilizando conceptos sencillos:

1. El Problema: Un Traductor Roto

Piensa en VNN-LIB 1.0 como un traductor que intentaba hablar dos idiomas a la vez pero seguía confundido.

Sin Gramática: No tenía reglas estrictas sobre cómo escribir una pregunta. Así, un robot podría entender una frase de una manera, y otro robot podría entenderla de manera diferente.
Vocabulario Limitado: Solo podía manejar rompecabezas simples (una entrada, una salida). La IA del mundo real a menudo tiene entradas complejas (como una imagen y algún texto) y múltiples salidas.
Confusión de Punto Flotante: Las computadoras usan números "aproximados" (como 3.14159...), pero el antiguo estándar no especificaba si debías tratarlos como matemáticas exactas o aproximaciones rudas. Esto llevó a errores peligrosos donde un robot pensaba que estaba seguro, pero no lo estaba.
El Problema de la "Caja Negra": El antiguo estándar se basaba en un formato de archivo llamado ONNX (el plano de la IA). Pero ONNX no tenía una definición estricta y oficial de lo que sus símbolos significaban. Era como darle a un robot un plano dibujado con crayones que cambia de opinión constantemente sobre lo que es una "pared".

2. La Solución: La "Teoría de Redes" (El Adaptador Universal)

La mayor innovación en este artículo es un concepto llamado Teoría de Redes.

Imagina que estás construyendo un adaptador de energía universal. No quieres construir un adaptador nuevo para cada enchufe de pared de cada país (cada versión de ONNX). En su lugar, creas una interfaz universal que dice: "Siempre que el enchufe proporcione electricidad, voltaje y tierra, puedo conectar".

La Teoría de Redes ( $\Psi$ ): Esta es esa interfaz universal. No le importa exactamente cómo está dibujado el plano de ONNX. Solo pregunta: "¿Tienes una forma de definir un número? ¿Una forma? ¿Una conexión?"
El Resultado: VNN-LIB 2.0 ahora puede hablar con cualquier versión de ONNX, incluso las futuras, sin necesidad de ser reescrito. Separa la pregunta (la consulta) del plano (el modelo), permitiéndoles evolucionar independientemente.

3. El Nuevo Idioma: VNN-LIB 2.0

Con esta nueva base, los autores construyeron un idioma mucho más inteligente con tres mejoras principales:

Frases Más Ricas (Sintaxis): Ahora puedes preguntar sobre escenarios complejos. En lugar de solo verificar un robot, puedes preguntar: "Si el Robot A y el Robot B trabajan juntos, ¿se mantienen seguros?". También puedes mirar dentro del "cerebro" del robot para verificar sus pensamientos ocultos (capas ocultas), no solo la respuesta final.
Gramática Estricta (Sistema de Tipos): El idioma ahora te obliga a ser preciso. Si intentas sumar una "temperatura" a un "color", el idioma dirá: "No, eso no tiene sentido". Esto evita que la computadora cometa errores matemáticos al mezclar diferentes tipos de números.
Significado Claro (Semántica): Cada palabra en el nuevo idioma tiene una definición matemáticamente probada. No hay adivinanzas. Si escribes una consulta, la computadora sabe exactamente qué problema matemático le estás pidiendo que resuelva.

4. La Opción "Mundo Real" vs. "Matemáticas Perfectas"

El artículo reconoce una situación complicada: Algunos robots se verifican usando "matemáticas perfectas" (números reales), mientras que el robot real se ejecuta con "matemáticas aproximadas" (números de punto flotante).

La Vieja Forma: Esto era un peligro oculto. El verificador diría "Seguro", pero el robot real podría estrellarse.
La Nueva Forma: VNN-LIB 2.0 te permite decir explícitamente: "Sé que esto usa matemáticas aproximadas, pero quiero verificarlo usando matemáticas perfectas de todos modos". Pone una etiqueta de advertencia en la consulta: "Proceda con precaución, esto podría ser ligeramente inexacto". Esto permite a los investigadores usar herramientas poderosas sin fingir que las matemáticas son perfectas cuando no lo son.

5. La Prueba del "Estándar de Oro"

Para asegurarse de no cometer ningún error al escribir este nuevo idioma, los autores no solo lo escribieron; lo programaron en un robot de demostración matemática llamado Agda.

Piensa en Agda como un editor superestricto que verifica cada regla individual del nuevo idioma para asegurar que no haya agujeros lógicos.
Debido a que el idioma está "mecanizado" en Agda, cualquiera puede ahora usar esta prueba para verificar que sus propias herramientas (solucionadores) funcionan correctamente. Convierte el estándar de una "sugerencia" en un "contrato matemáticamente garantizado".

Resumen

En resumen, VNN-LIB 2.0 es un nuevo idioma estricto y flexible para hacer preguntas sobre la seguridad de la IA. Corrige la gramática rota del pasado, permite preguntas complejas sobre múltiples modelos de IA y proporciona una base matemáticamente probada para que, cuando una herramienta diga "Esta IA es segura", podamos realmente confiar en que significa exactamente lo que dice.

Resumen Técnico: VNN-LIB 2.0: Fundamentos Rigurosos para la Verificación de Redes Neuronales

Declaración del Problema

La comunidad de verificación de redes neuronales ha dependido cada vez más del estándar VNN-LIB (Versión 1.0) para facilitar la interoperabilidad entre solucionadores y herramientas de nivel superior. Sin embargo, la Versión 1.0 adolece de cuatro deficiencias críticas que le impiden servir como una base formal rigurosa:

Falta de Sintaxis Formal: La Versión 1.0 no define formalmente la sintaxis del lenguaje de consultas, lo que conduce a implementaciones mutuamente incompatibles por parte de diferentes solucionadores.
Expresividad Limitada: El estándar asume una única red con una única entrada y salida. No puede soportar de forma nativa múltiples redes, múltiples entradas/salidas o el acceso a capas ocultas, obligando a los usuarios a fusionar modelos artificialmente, lo que oscurece la relación entre los artefactos verificados y los modelos desplegados.
Ausencia de un Sistema de Tipos: No existe un mecanismo para especificar tipos numéricos (por ejemplo, punto flotante frente a valor real), lo que crea ambigüedad y una posible falta de solidez cuando los solucionadores tratan la aritmética de precisión finita como de valor real.
Falta de Semántica: El estándar carece de una semántica formal, lo que hace imposible probar formalmente la corrección de solucionadores, generadores de consultas o transformaciones, y obstaculiza el desarrollo de certificados de prueba.

Un desafío único para VNN-LIB, que lo distingue de estándares como SMT-LIB, es que las consultas no son autónomas; especifican propiedades de modelos de redes neuronales externos (típicamente en formato ONNX). Dado que ONNX en sí mismo carece de una semántica formal y continúa evolucionando, definir un estándar riguroso de VNN-LIB requiere desacoplar el lenguaje de consultas de versiones específicas de ONNX mientras se mantiene la compatibilidad.

Metodología

Los autores abordan estos desafíos desarrollando los fundamentos teóricos para VNN-LIB 2.0. La innovación metodológica central es la introducción de la Teoría de Redes ( $\Psi$ ).

1. Abstracción de la Teoría de Redes

Los autores definen una "teoría de redes" como una especificación abstracta que captura la sintaxis mínima, los juicios de tipado y la semántica requeridos de un formato de modelo de red neuronal para definir VNN-LIB.

Desacoplamiento: $\Psi$ actúa como una interfaz. Una implementación concreta de $\Psi$ (por ejemplo, para ONNX v1.20.0) proporciona definiciones específicas para tipos de elementos, representaciones de tensores, estructuras de modelos y referencias a salidas de nodos.
Modularidad: VNN-LIB 2.0 se define en relación con un $\Psi$ abstracto. Esto permite que el estándar permanezca estable incluso a medida que ONNX evoluciona; solo es necesario actualizar la instancia de $\Psi$ para nuevas versiones de ONNX, no el estándar VNN-LIB en sí mismo.
Formalización: Todo el estándar, incluida la sintaxis, el tipado y la semántica, se mecaniza en el demostrador de teoremas interactivo Agda para garantizar la consistencia interna y descartar ambigüedades.

2. Sintaxis Formal y Expresividad

Basándose en la teoría de redes, los autores definen una gramática formal para VNN-LIB 2.0 que extiende significativamente la expresividad:

Múltiples Redes: Las consultas pueden declarar múltiples redes, soportando escenarios como la verificación maestro-alumno o arquitecturas codificador-decodificador.
Equivalencia de Redes: El estándar introduce declaraciones equal-to (refiriéndose al mismo archivo de modelo exacto) e isomorphic-to (refiriéndose a modelos con la misma estructura de grafo pero potencialmente diferentes pesos). Esto permite a los solucionadores compartir deducciones (por ejemplo, límites de variables) entre copias de redes.
Nodos Ocultos: La construcción declare-hidden permite restricciones sobre las salidas de capas intermedias, esenciales para razonar sobre codificaciones o mecanismos de atención.
E/S Multidimensionales: Soporte para números arbitrarios de entradas y salidas, acomodando redes multimodales.

3. Sistema de Tipos y Semántica

Tipado: Un sistema de tipos formal impone la solidez numérica. Garantiza que las operaciones aritméticas y las comparaciones se realicen sobre tipos compatibles (por ejemplo, evitando mezclar float32 e int32 sin reglas de coerción explícitas). El sistema de tipos se basa en los juicios proporcionados por la teoría de redes subyacente $\Psi$ .
Semántica: La semántica de una consulta se define como un problema de satisfacibilidad matemático. Dado un conjunto de modelos $M$ (instanciados desde $\Psi$ ) y una asignación de entrada $X$ , la semántica determina si existe una asignación donde todas las aserciones se evalúan como verdaderas.
Consultas de Valor Real: Para acomodar solucionadores existentes que tratan los modelos como funciones sobre números reales ( $\mathbb{R}$ ), el estándar introduce un mecanismo para "consultas de valor real". Al utilizar un tipo distinguido real, el autor de la consulta autoriza explícitamente al solucionador a interpretar los modelos sobre $\mathbb{R}$ , reconociendo la posible falta de solidez debido a la imprecisión del punto flotante. Esto se logra construyendo una teoría de redes específica $\Psi_{\mathbb{R}}$ derivada de la teoría base.

Contribuciones Clave

Teoría de Redes ( $\Psi$ ): La introducción de una abstracción novedosa que define la interfaz semántica mínima requerida de un formato de modelo, permitiendo que VNN-LIB se defina independientemente de versiones específicas de ONNX.
Sintaxis y Gramática Formal: Una gramática libre de contexto precisa para VNN-LIB 2.0 que soporta múltiples redes, capas ocultas y estructuras complejas de entrada/salida.
Sistema de Tipos Formal: Un sistema de tipado que impone la solidez de los tipos numéricos en relación con la teoría de redes, abordando la ambigüedad en las representaciones numéricas.
Semántica Formal: Una definición matemática rigurosa de la semántica de consultas parametrizada por la teoría de redes, habilitando pruebas formales de corrección para herramientas que consumen o generan VNN-LIB.
Mecanización: El estándar completo se formaliza en Agda, proporcionando una implementación de referencia canónica y una base para pruebas verificadas por máquina.
Extensión de Valor Real: Un enfoque modular para soportar análisis de valor real mediante una teoría de redes derivada, equilibrando la necesidad de solidez con la realidad de las capacidades actuales de los solucionadores.

Resultados y Validación

Consistencia Interna: La formalización en Agda valida la consistencia interna de la sintaxis, el tipado y la semántica, asegurando que el estándar esté libre de las ambigüedades presentes en la Versión 1.0.
Demostración de Expresividad: El artículo demuestra cómo una transformación simple de la teoría de redes $\Psi$ produce una instancia completa para consultas de valor real, mostrando la flexibilidad de la abstracción.
Adopción Comunitaria: El estándar ha recibido retroalimentación positiva de la comunidad de verificación. Equipos líderes de solucionadores se han comprometido a apoyar VNN-LIB 2.0, y el nuevo estándar está programado para ser utilizado en la competición VNN-COMP 2026.
Soporte de Herramientas: Los autores han lanzado una biblioteca de alto rendimiento en C++ (con enlaces para Python y Julia) que implementa un analizador sintáctico y un verificador de tipos compatibles con el nuevo estándar, junto con la formalización en Agda.

Significado

El artículo afirma que VNN-LIB 2.0 proporciona fundamentos robustos y rigurosos para la verificación confiable de redes neuronales. Su significado radica en dos áreas complementarias:

Interoperabilidad Práctica: Al extender la expresividad (múltiples redes, nodos ocultos) y estandarizar la sintaxis, permite a la comunidad especificar y verificar propiedades más ricas de manera unificada, facilitando una mejor comparación de benchmarks y herramientas.
Rigor Teórico: Al proporcionar semántica formal y un sistema de tipos, establece un "contrato riguroso" entre herramientas y solucionadores. Esto permite la verificación formal de las propias herramientas (solucionadores, optimizadores, verificadores de pruebas) y resuelve problemas sutiles relacionados con la solidez numérica (por ejemplo, distinguir entre semántica de valor real y de punto flotante).

Los autores enfatizan que, aunque el trabajo es teórico, tiene consecuencias concretas: asegura una interpretación inequívoca de las consultas, proporciona el lenguaje para resolver problemas técnicos y sienta las bases para certificados de prueba formalmente verificados en el futuro.