⚡ electrical engineering

Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis

Este artículo presenta RoVer-CoRe, un marco pionero basado en el análisis de alcanzabilidad de Hamilton-Jacobi que permite la verificación formal de la seguridad y el diseño robusto de controladores basados en percepción para sistemas autónomos, superando las limitaciones de incertidumbre perceptual y la complejidad de los controladores no lineales o de aprendizaje.

Autores originales: Albert Lin, Alessandro Pinto, Somil Bansal

Publicado 2026-04-16

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Albert Lin, Alessandro Pinto, Somil Bansal

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 construyendo un coche autónomo o un rover para Marte. Estos robots tienen "ojos" (cámaras) y un "cerebro" (una inteligencia artificial) que les dice cómo moverse. Pero, ¿qué pasa si esos ojos ven mal? ¿Qué pasa si la cámara está sucia, hay niebla, o la inteligencia artificial comete un error al interpretar lo que ve?

El problema es que, si el robot cree que está en un lugar seguro pero en realidad está a punto de chocar, podría tener un accidente. Verificar que estos robots son seguros es muy difícil porque sus "cerebros" son complejos y a veces funcionan como una "caja negra" (no sabemos exactamente cómo piensan).

Los autores de este paper (Lin, Pinto y Bansal) han creado una nueva herramienta llamada RoVer-CoRe. Vamos a explicarla con una analogía sencilla:

1. El Problema: El Robot con Gafas de Sol Sucias

Imagina que el robot es un conductor que lleva gafas de sol muy sucias.

La realidad: El coche está en la carretera.
Lo que ve el robot: Debido a las gafas sucias (incertidumbre perceptual), el robot cree que está un poco a la izquierda o a la derecha de donde realmente está.
El riesgo: Si el robot gira el volante basándose en esa visión borrosa, podría salirse de la carretera.

Antes, los ingenieros intentaban predecir todos los caminos posibles que podría tomar el robot usando métodos aproximados (como dibujar cajas grandes alrededor del coche). Pero estas cajas eran tan grandes y conservadoras que a menudo decían "¡Peligro!" incluso cuando el robot estaba seguro, o no podían garantizar nada en absoluto.

2. La Solución: RoVer-CoRe (El "Simulador de Pesadillas")

RoVer-CoRe es como un simulador de pesadillas extremadamente preciso. En lugar de dibujar cajas grandes, utiliza una técnica matemática avanzada llamada Análisis de Alcanzabilidad de Hamilton-Jacobi (HJ).

Aquí está la magia en tres pasos:

Paso A: Unir todo en una sola pieza

El equipo toma el "cerebro" del robot (el controlador), sus "ojos" (la cámara) y su "memoria" (el estimador de posición) y los pega juntos como si fueran un solo bloque.

Analogía: Imagina que en lugar de analizar por separado al conductor, sus gafas y el coche, analizas al "Conductor con Gafas Sucias conduciendo el Coche" como una sola entidad. Así, el único enemigo externo que queda es la "mala suerte" (el error de visión y el viento).

Paso B: El Juego del Peor Escenario

La herramienta hace una pregunta crucial: "¿Cuál es el peor error de visión posible que podría tener el robot y aún así sobrevivir?".

En lugar de adivinar, la herramienta calcula matemáticamente el límite exacto de seguridad.
Analogía: Es como si un entrenador de fútbol le dijera a su equipo: "Vamos a simular que el árbitro es injusto, que el campo está resbaladizo y que el viento sopla en contra. Si el equipo puede ganar en ese escenario, entonces ganará en cualquier otro".

Paso C: Dibujar el "Círculo de Seguridad"

La herramienta dibuja un mapa (llamado "Tubo de Alcanzabilidad Inversa" o BRT).

Dentro del círculo rojo: Si el robot empieza aquí, ¡está condenado a chocar si hay un error de visión!
Fuera del círculo rojo: Si el robot empieza aquí, ¡está 100% seguro, incluso si sus ojos fallan al máximo!

3. ¿Para qué sirve esto en la vida real?

El paper muestra dos ejemplos geniales:

Aviones que aterrizan solos:
Imagina un avión que aterriza usando solo una cámara en el ala. RoVer-CoRe pudo decir: "Si la cámara tiene un error de visión de hasta un 99%, este avión está seguro". Pero también encontró que, si el error es un poquito más grande, ¡se estrella! Esto ayudó a los ingenieros a ajustar los controles del avión para que fuera más robusto, como afinar los frenos de un coche para que no patine en la lluvia.
Rovers lunares (coches para la Luna):
Imagina un coche explorador en la Luna que usa luces de faro para ver. Si las luces se apagan para ahorrar batería, la oscuridad hace que sus "ojos" (cámaras) se vuelvan más borrosos con el tiempo.
- RoVer-CoRe calculó exactamente cuánto tiempo puede conducir el rover en la oscuridad antes de que el error sea demasiado grande y se estrelle contra una roca.
- Con esta información, crearon un "botón automático" que enciende las luces solo cuando es estrictamente necesario. ¡Ahorra energía y mantiene al rover seguro!

En Resumen

RoVer-CoRe es como un escudo matemático para los robots.

No se conforma con decir "probablemente esté bien".
Dice: "Aquí están los límites exactos. Si estás dentro de esta zona, puedes estar tranquilo incluso si todo sale mal".
Ayuda a los ingenieros a diseñar robots que no solo son inteligentes, sino que son imposibles de engañar por errores de visión, haciendo que el futuro de la automatización sea mucho más seguro.

Es la diferencia entre confiar en que "todo saldrá bien" y tener una garantía matemática de que, incluso en el peor de los casos, el robot no se estrellará.

1. Planteamiento del Problema

El artículo aborda el desafío crítico de verificar formalmente la seguridad y el rendimiento de controladores basados en percepción para sistemas autónomos, en presencia de incertidumbre perceptual.

Contexto: Los controladores modernos utilizan redes neuronales (NN) y sensores para interpretar el entorno. Sin embargo, estos sistemas sufren de ruido en los sensores, errores de aprendizaje y factores ambientales (ej. pérdida de señal GPS).
El Desafío: Verificar que un sistema no entrará en estados de fallo (ej. colisiones) es extremadamente difícil debido a la complejidad de los controladores (no lineales, no convexos, "cajas negras").
Limitaciones de trabajos previos:
- Los métodos de conjuntos alcanzables aproximados (usando hiperrectángulos, zonotopos, etc.) a menudo son demasiado conservadores, fallando en certificar la seguridad de sistemas que en realidad son seguros.
- Los métodos basados en funciones de barrera (CBF) enfrentan desafíos de factibilidad global y construcción de barreras.
- El análisis de alcanzabilidad Hamilton-Jacobi (HJ) tradicional asume que el controlador tiene acceso al estado verdadero del sistema, lo cual no es válido cuando existe incertidumbre en la percepción.

2. Metodología: RoVer-CoRe

Los autores proponen RoVer-CoRe (Robust Verification of Controllers via HJ Reachability), un marco de trabajo que adapta el análisis HJ para manejar controladores basados en percepción.

A. Abstracción del Sistema de Lazo Cerrado

La idea central es concatenar tres módulos en una sola dinámica de sistema:

Mapa de observación: $p(x)$ (ej. cámara).
Estimador de estado: $q(o, e)$ (ej. filtro o NN que produce $\hat{x}$ con error $e$ ).
Controlador: $\pi(\hat{x})$ que genera el comando $u$ .

Esto define una dinámica de lazo cerrado $h(x, d, e) = f(x, \pi(q(p(x), e)), d)$ , donde las únicas entradas externas son la perturbación del sistema $d$ y el error perceptual $e$ . Esto permite tratar la incertidumbre perceptual como una perturbación adversaria dentro del marco HJ estándar.

B. Cálculo y Acotación del Hamiltoniano

El principal obstáculo técnico es calcular el Hamiltoniano del lazo cerrado, que se vuelve no convexo debido a la complejidad de $\pi$ , $p$ y $q$ . RoVer-CoRe ofrece dos enfoques:

Cálculo Exacto: Para controladores simples o enumerables (ej. controladores lineales o basados en cuadrícula), se resuelve la optimización del Hamiltoniano exactamente. Esto proporciona garantías sin conservadurismo.
Acotación Inferior (Lower Bounding): Para controladores complejos (como NNs), se calculan límites inferiores y superiores del espacio de salida del controlador ( $\underline{U}(x)$ $\underline{U} (x)$ y $\overline{U}(x)$ $\overline{U} (x)$ ) bajo incertidumbre.
- Se utiliza herramientas de verificación de NN (como $\alpha,\beta$ -CROWN) para obtener estos límites.
- Se sustituye el controlador por un rango de controles posibles en la ecuación del Hamiltoniano.
- Resultado: Esto produce un análisis conservador pero sonoro (sound). Si el sistema es seguro bajo este límite inferior, es seguro en la realidad.

C. Diseño de Controladores Robustos

El marco no solo verifica, sino que guía el diseño. Se utiliza para la optimización de hiperparámetros orientada a la seguridad. Al evaluar la función de valor robusta sobre un rango de hiperparámetros, se pueden seleccionar aquellos que maximicen el margen de seguridad o el volumen del conjunto seguro.

3. Contribuciones Clave

RoVer-CoRe: El primer marco basado en HJ para verificar sistemas basados en percepción bajo incertidumbre perceptual.
Métodos de Verificación: Técnicas para calcular o acotar el Hamiltoniano del lazo cerrado, permitiendo manejar desde controladores lineales hasta redes neuronales profundas.
Diseño Robusto: Un enfoque para sintetizar controladores que sean intrínsecamente robustos a errores de percepción mediante la optimización de parámetros basada en la verificación.
Código Abierto: Disponibilidad del código y casos de estudio para reproducibilidad.

4. Resultados y Estudios de Caso

Los autores validaron el marco en dos escenarios:

A. Rodaje de Aviones (Taxiing)

Escenario: Un avión sigue una línea central usando una cámara y una NN para estimar errores de posición y rumbo.
Verificación: Se verificó la seguridad bajo peores errores perceptuales. RoVer-CoRe pudo certificar la seguridad hasta una cobertura de error del 99.68%.
Diseño: Se identificaron controladores inseguros (con ganancias excesivas) y se encontraron nuevos hiperparámetros (puntos naranjas en el espacio de diseño) que garantizan la seguridad incluso con errores adversos.
Hallazgo: El método expuso modos de fallo específicos, como la sobre-corrección debido a una mala percepción de la posición lateral.

B. Navegación de Rover Lunar (NN-Based)

Escenario: Un rover navega en la oscuridad (luz lunar) donde la odometría visual acumula errores con el tiempo. Se pueden encender luces para resetear el error, pero con costo energético.
Comparación: Se comparó un controlador MPC (basado en cuadrícula) con una NN que imita al MPC.
- RoVer-CoRe demostró que los límites de la NN son más "inflados" (conservadores) que los del MPC debido al error de imitación y a la holgura de la verificación de NN.
- Eficiencia: RoVer-CoRe identificó estados inseguros que un método de Monte Carlo (10,000 muestras) falló en detectar.
Política de Luces: Se diseñó una política que enciende las luces solo cuando la incertidumbre crece lo suficiente para amenazar la seguridad, garantizando la seguridad formal mientras se ahorra energía.

5. Significado e Impacto

Rigor vs. Conservadurismo: A diferencia de las herramientas de conjuntos aproximados (como NNV 2.0), que pueden ser excesivamente conservadoras y rechazar sistemas seguros, RoVer-CoRe ofrece garantías más ajustadas (menos conservadoras) al calcular conjuntos alcanzables óptimos.
Garantías Formales: Proporciona garantías matemáticas de que un sistema no entrará en zonas de fallo, incluso bajo los peores errores de percepción y perturbaciones del entorno.
Puente entre Percepción y Control: Unifica la verificación de componentes de percepción (NNs) y control en un solo marco matemático coherente, llenando una brecha importante en la seguridad de sistemas autónomos.
Escalabilidad: Aunque el cálculo exacto de HJ tiene limitaciones de dimensionalidad, el enfoque de acotación permite aplicar el método a sistemas con NNs complejas, ofreciendo una vía práctica para la certificación de sistemas de IA en seguridad crítica.

En resumen, RoVer-CoRe representa un avance significativo hacia la certificación formal de sistemas autónomos que dependen de la percepción, ofreciendo tanto herramientas de verificación rigurosa como metodologías para diseñar controladores más robustos.