Resumen Técnico: Una Encuesta sobre la Verificación de Políticas de Aprendizaje por Refuerzo

1. Planteamiento del Problema

El Aprendizaje por Refuerzo (RL) se despliega cada vez más en dominios críticos para la seguridad, como la conducción autónoma y los sistemas energéticos. Sin embargo, el despliegue de agentes de RL en entornos de alto riesgo se ve obstaculizado por la falta de garantías de comportamiento rigurosas. Las políticas de RL se implementan típicamente como Redes Neuronales Profundas (DNN) con fronteras de decisión complejas y no lineales que pueden exhibir comportos inseguros bajo condiciones raras, cambios de distribución o efectos de interacción.

A diferencia del aprendizaje supervisado, donde la corrección se define por la robustez de entrada-salida en distribuciones fijas, la corrección en RL depende fundamentalmente de la interacción, la retroalimentación y el cambio de distribución durante la ejecución. Una política de RL moldea activamente la distribución de estados que encuentra a través del control de bucle cerrado. Esto conduce a la acumulación de errores, fallos de eventos raros y violaciones de seguridad que pueden manifestarse solo tras largos horizontes (por ejemplo, una política que es robusta en cada paso de tiempo individual puede aun así fallar debido a la acumulación de errores). En consecuencia, los objetivos de verificación en RL no pueden reducirse a un análisis estático de entrada-salida; deben dar cuenta de la dependencia temporal, el acoplamiento política-entorno y la incertidumbre en el momento del despliegue.

La literatura sobre la verificación de RL está actualmente conceptualmente fragmentada. Los métodos se desarrollan bajo supuestos variables, apuntan a distintas nociones de corrección y operan sobre diferentes alcances temporales, lo que dificulta la comparación de enfoques o la comprensión de sus relaciones fundamentales.

2. Metodología y Taxonomía

El artículo introduce una taxonomía unificada para organizar los métodos de verificación post-entrenamiento existentes para políticas basadas en redes neuronales. La taxonomía clasifica los enfoques a lo largo de tres ejes primarios:

1. Paradigma de Verificación: Distingue entre métodos Formales (que proporcionan garantías deterministas y sólidas mediante satisfacción o alcanzabilidad) y métodos Probabilísticos (que cuantifican el riesgo y proporcionan garantías de alta confianza en entornos estocásticos).
2. Alcance Temporal:
   • Paso a paso (Step-wise): Analiza una única decisión de la política en un estado dado, abstrayendo la dinámica futura. Esta es la clase de herramientas más madura.
   • Multipaso (Multi-step): Razona sobre el comportamiento a nivel de trayectoria o de bucle cerrado sobre horizontes finitos o infinitos, capturando la interacción entre la política y el entorno.
3. Fuerza de las Garantías: Varía desde Sólido y Completo (verificación exacta) hasta Sólido (sobre-aproximaciones) y Probabilístico (límites estadísticos).

La taxonomía también incluye un eje de "Preparación para RL" (RL Readiness), que indica si un método puede aplicarse directamente a políticas de RL entrenadas sin una abstracción o reformulación sustancial.

Formulaciones Clave de Verificación

• Verificación Paso a Paso: Se formula como la comprobación de si una política selecciona una acción insegura dentro de una región de entrada local $X$. Esto se mapea frecuentemente a problemas de Verificación de Redes Neuronales usando:
  • Satisfacibilidad (SAT): Búsqueda de un contraejemplo de entrada (NP-duro).
  • Alcanzabilidad (Reachability): Computación de sobre-aproximaciones de conjuntos de salida alcanzables (por ejemplo, mediante Interpretación Abstracta o Relajación Lineal).
  • Probabilística: Estimación de la probabilidad de acciones inseguras sin asumir modelos de ruido específicos (por ejemplo, PT-LiRPA).
• Verificación de Multipaso: Se formula como la determinación de si cualquier trayectoria de bucle cerrado alcanza un estado inseguro. Los enfoques incluyen:
  • MDPs Etiquetados y Lógica Temporal: Uso de Lógica Temporal Lineal (LTL) para especificar propiedades de trayectoria, verificadas sobre el producto del MDP inducido por la política y un autómata.
  • Certificados Neuro-Simbólicos: Combinación de políticas aprendidas con certificados de la teoría de control (por ejemplo, Funciones de Barrera de Control, funciones de Lyapunov) para imponer seguridad en tiempo de ejecución.
  • Probabilística de Multipaso: Estimación de la probabilidad de satisfacer propiedades temporales sobre trayectorias mediante muestreo o propagación de límites probabilísticos.
• Verificación basada en Enumeración: Un paradigma emergente que computa el conjunto de todas las entradas que conducen a acciones inseguras (la preimagen). Esto proporciona información a nivel de región para la depuración y la evaluación de riesgos, aunque la enumeración exacta es #P-dura.

3. Contribuciones Clave

1. Taxonomía Unificada: El artículo proporciona la primera organización exhaustiva de los métodos de verificación de RL a lo largo de los ejes de paradigma, alcance temporal y fuerza de garantía, aclarando los compromisos entre expresividad y escalabilidad.
2. Formalización: Unifica los fundamentos teóricos de los problemas de verificación de RL utilizando una notación consistente, haciendo explícitos los supuestos implícitos y las limitaciones.
3. Análisis Crítico: El estudio analiza las limitaciones de los métodos existentes, particularmente los cuellos de botella de escalabilidad en la verificación de multipaso y los desafíos de aplicar herramientas de paso a paso a sistemas recurrentes o multi-agente.
4. Benchmarking de Herramientas: Proporciona una comparación empírica de herramientas de verificación (incluyendo participantes de VNN-COMP y métodos de aproximación de preimágenes) en benchmarks de RL (ACAS Xu, CartPole, LunarLander, Dubin's Rejoin), resaltando que, si bien los métodos de propagación de límites escalan bien para tareas de paso a paso, la verificación de multipaso sigue siendo un cuello de botella significativo debido a la explosión del espacio de estados.

4. Resultados y Observaciones

• Escalabilidad vs. Precisión: Existe un compromiso fundamental. Los métodos exactos (SAT, enumeración exhaustiva) suelen ser intratables para redes grandes o horizontes largos. La sobre-aproximación y los métodos probabilísticos ofrecen mejor escalabilidad pero pueden generar garantías conservadoras o probabilísticas en lugar de seguridad absoluta.
• Madurez del Paso a Paso: La verificación paso a paso es el área más madura, con herramientas como $\alpha,\beta$-CROWN y NNV 2.0 mostrando una escalabilidad prometedora. Sin embargo, estos métodos no pueden razonar sobre la ejecución de bucle cerrado o los efectos de largo horizonte.
• Desafíos de Multipaso: La verificación de multipaso está limitada por la "maldición de la dimensionalidad" al modelar la dinámica y las especificaciones temporales. Los enfoques neuro-simbólicos ofrecen fuertes garantías pero dependen de supuestos de modelado adicionales (por ejemplo, dinámica conocida o certificados aprendibles) que restringen la generalidad.
• Utilidad de la Enumeración: Los enfoques basados en la enumeración, aunque computacionalmente costosos, aportan un valor único para la depuración de políticas, la recolección de datos dirigida y la cuantificación de la severidad del riesgo residual mediante la caracterización de regiones inseguras del espacio de estados.

5. Desafíos Abiertos y Direcciones Futuras

El artículo identifica varias brechas críticas entre la verificación clásica de redes neuronales y los sistemas modernos de RL:

• Políticas Recurrentes (RNNs): La verificación de políticas dependientes de la historia en entornos parcialmente observables es desafiante porque la seguridad depende de trayectorias de estados ocultos factibles. Los métodos actuales a menudo fallan al distinguir entre estados ocultos realizables y espurios, lo que conduce a garantías excesivamente conservadoras o contraejemplos espurios.
• Aprendizaje por Refuerzo Multi-Agente (MARL): La seguridad en MARL emerge de las interacciones. Verificar políticas descentralizadas requiere razonar sobre espacios conjuntos de estado-acción y coordinación implícita, lo que introduce una complejidad exponencial y nuevos desafíos semánticos respecto a la seguridad por agente frente a la seguridad de equipo.
• Incertidumbre del Entorno: La mayoría de los métodos asumen dinámicas conocidas o aproximadas con precisión. Los sistemas del mundo real enfrentan desajustes de modelo y no estacionariedad, lo que plantea interrogantes sobre cómo proporcionar garantías tratables para el sistema de bucle cerrado bajo incertidumbre.
• Arquitecturas Modernas: Verificar Transformers y modelos basados en atención es difícil porque los mecanismos de atención violan los supuestos de linealidad por partes, y estos modelos razonan sobre historias de longitud variable, complicando la abstracción temporal.

6. Significado

El artículo argumenta que la verificación de RL no es meramente un problema de escalabilidad, sino un problema conceptual. La corrección en RL debe definirse en términos de interacciones, dependencia temporal y decisiones descentralizadas, en lugar de robustez estática de entrada-salida. La taxonomía propuesta sirve como una perspectiva unificadora para navegar la literatura fragmentada, ayudando a los profesionales a seleccionar las herramientas apropiadas basadas en sus objetivos de verificación específicos (por ejemplo, robustez local frente a seguridad de largo horizonte) y las restricciones estructurales de sus sistemas de RL. Los autores enfatizan que el progreso futuro requiere marcos que alineen mejor la ejecución de RL con la semántica de la misma, equilibrando la solidez y la escalabilidad.