Resumen Técnico: Entrenamiento con Restricciones Duras: Aprendizaje de Certificados y Controladores Neuronales para EDEs

1. Planteamiento del Problema

El trabajo aborda el desafío de garantizar el cumplimiento estricto de restricciones de seguridad en sistemas dinámicos continuos gobernados por Ecuaciones Diferenciales Estocásticas (EDEs). Específicamente, se centra en problemas de control de "alcanzar-evitar" (reach-avoid), donde el objetivo es que el sistema llegue a un conjunto objetivo ($X_g$) evitando un conjunto inseguro ($X_u$) con una probabilidad mínima garantizada.

• El Reto: Los métodos existentes para generar certificados de estabilidad (funciones tipo Lyapunov o supermartingalas) utilizando Redes Neuronales (RN) a menudo dependen de verificación posterior o penalizaciones suaves durante el entrenamiento. Esto no ofrece garantías formales de que las restricciones se cumplan en todo el dominio continuo, especialmente en sistemas de alta dimensión.
• Objetivo: Desarrollar marcos de entrenamiento que incorporen las restricciones duras directamente en el proceso de optimización, garantizando la validez del certificado (y del controlador) al finalizar el entrenamiento, sin sacrificar la escalabilidad.

2. Metodología Propuesta

Los autores proponen dos enfoques complementarios para entrenar RNs bajo restricciones duras:

A. Entrenamiento Basado en Límites (Bound-Training) con Garantías Duras

Este enfoque está diseñado para sistemas de dimensión moderada (hasta 5D en los experimentos).

• Mecanismo: Divide el dominio del estado en una partición de celdas compactas. Utiliza aritmética de intervalos (como auto-LiRPA) para calcular límites superiores e inferiores analíticos de la función de certificado $V_\theta$ y de su generador infinitesimal $G[V_\theta]$ dentro de cada celda.
• Función de Pérdida: Define una pérdida basada en límites ($L_{bound}$) que cuantifica la violación de las desigualdades del certificado (no negatividad, condiciones en conjuntos inicial/objetivo/inseguro y decrecimiento esperado) en el peor caso de cada celda.
• Garantía: Si la pérdida se reduce a cero, se garantiza matemáticamente que el certificado es válido en todo el dominio.
• Estrategias de Escalabilidad: Para evitar la explosión combinatoria de celdas en dimensiones altas, implementan:
  • Refinamiento Adaptativo: Dividen solo las celdas donde se violan las restricciones.
  • Fusión (Merging): Combinan celdas adyacentes que ya satisfacen las restricciones con un margen de seguridad.
• Síntesis Conjunta: Extiende el método para entrenar simultáneamente un controlador neuronal ($\pi$) y un certificado ($V$), propagando los gradientes a través del grafo computacional derivado de la dinámica de la EDE cerrada.

B. Entrenamiento Basado en Escenarios con Garantías PAC

Este enfoque se dirige a sistemas de alta dimensión (hasta 10D y más) donde la partición del espacio es prohibitiva.

• Mecanismo: Evita la partición del espacio. En su lugar, muestrea un conjunto finito de estados y optimiza los parámetros de la última capa de la red neuronal (y el parámetro $\beta$) mediante un Programa Lineal (LP).
• Fundamento Teórico: Se basa en la teoría de optimización convexa de escenarios (Campi et al., 2009).
• Garantía PAC (Probablemente Aproximadamente Correcto): Proporciona garantías estadísticas: con una confianza alta ($1-\delta$), el certificado satisface las restricciones en todo el espacio de estados, excepto en un conjunto de medida pequeña ($\epsilon$) que disminuye a medida que aumenta el número de muestras ($N$).
• Ventaja: La complejidad de la muestra necesaria es independiente de la dimensión del estado, permitiendo escalar a sistemas de 10 dimensiones o más.

3. Contribuciones Clave

1. Marco de Entrenamiento con Garantías Duras: Presentación de un método de entrenamiento basado en límites que garantiza la satisfacción de restricciones de certificados de supermartingala para EDEs una vez que la pérdida es cero.
2. Síntesis Conjunta Controlador-Certificado: Extensión del marco para aprender simultáneamente políticas de control neuronales y certificados, guiando al controlador no solo hacia el rendimiento de la tarea, sino también hacia la verificabilidad formal.
3. Método Escalable con Garantías PAC: Introducción de un método de entrenamiento sin partición que utiliza optimización de escenarios para ofrecer garantías PAC arbitrariamente ajustables en sistemas de alta dimensión.
4. Validación Empírica: Demostración de escalabilidad superior frente al estado del arte en múltiples benchmarks, incluyendo sistemas de hasta 5D con garantías duras y 10D con garantías PAC.

4. Resultados Experimentales

Los autores evaluaron sus métodos en varios casos de estudio, incluyendo un péndulo invertido estocástico, Movimiento Browniano Geométrico (GBM) en dimensiones 2 a 10, el sistema de Lorenz estocástico y la dinámica longitudinal de un avión XV-15.

• Verificación (Problema 1):

  • El método Hard-SAT (basado en límites) superó al estado del arte (Neustroev et al., 2025) en eficiencia y escalabilidad, logrando certificados válidos hasta 5D, mientras que el método comparado falló en dimensiones superiores.
  • El método Basado en Escenarios escaló exitosamente hasta 10D, alcanzando probabilidades de alcanzar-evitar ($p_{RA}$) cercanas a 1.0 con una confianza de $1-10^{-9}$.
  • Se demostró que el entrenamiento "suave" (pre-entrenamiento) por sí solo no genera certificados válidos; la optimización específica de la capa final es crucial.

• Síntesis de Control (Problema 2):

  • El algoritmo Hard-SAT logró sintetizar controladores y certificados conjuntamente para sistemas complejos como el péndulo invertido y el XV-15.
  • Las simulaciones de Monte Carlo mostraron una probabilidad empírica de éxito del 100% para todos los sistemas cerrados sintetizados.
  • En el caso del XV-15, el controlador sintetizado estabilizó la trayectoria y alcanzó el objetivo de manera segura, superando a estrategias de control constante o controladores pre-entrenados solo con muestreo.

5. Significado e Impacto

Este trabajo representa un avance significativo en la intersección del aprendizaje profundo y el control formal.

• Superación de Limitaciones: Aborda la brecha entre la expresividad de las redes neuronales y la necesidad de garantías formales en sistemas estocásticos, un problema que los métodos tradicionales (como la programación de sumas de cuadrados) no pueden resolver a escalas prácticas.
• Seguridad Crítica: Al proporcionar garantías de "restricciones duras" (en lugar de suaves o probabilísticas sin acotación), el método es aplicable a sistemas de seguridad crítica donde el fallo no es una opción.
• Escalabilidad: La combinación de un enfoque determinista (para dimensiones moderadas) y un enfoque estadístico (para dimensiones altas) ofrece una solución práctica para una amplia gama de sistemas dinámicos complejos, abriendo la puerta a la verificación y síntesis de controladores neuronales en aplicaciones del mundo real como la aviación y la robótica.

En resumen, el paper establece un nuevo estándar para el entrenamiento de redes neuronales con garantías formales en entornos estocásticos, demostrando que es posible lograr tanto alta dimensionalidad como cumplimiento estricto de especificaciones de seguridad.