Certifying Plans under Model Mismatch: A Trilemma for Reachability from Scarce Data

Resumen Técnico: Certificación de Planes bajo Desajuste de Modelo: Un Trilema para la Alcanzabilidad a partir de Datos Escasos

Planteamiento del Problema
El artículo aborda el desafío de certificar secuencias de control fijas (por ejemplo, fragmentos de acción de políticas aprendidas como Diffusion Policy o $\pi_0$) para su despliegue en sistemas robóticos del mundo real donde la dinámica difiere del modelo de simulación nominal. La dificultad central surge cuando el sistema objetivo proporciona únicamente un conjunto disperso de transiciones aisladas de un solo paso. En este escenario, un certificador debe determinar si una trayectoria planificada permanecerá segura (evitando un conjunto inseguro $O$) a pesar del error del modelo desconocido (residuo) entre la dinámica nominal $f_0$ y la verdadera dinámica objetivo $f^\star$.

Los autores identifican una limitación fundamental: lejos de los puntos de datos observados, el error del modelo puede variar arbitrariamente dentro de una pequeña vecindad sin contradecir las observaciones. Si el error del modelo no tiene restricciones, dos sistemas suaves objetivo que sean consistentes con los mismos datos dispersos pueden divergir arbitrariamente una vez que el plan entra en una región no observada. En consecuencia, cualquier certificador determinista que sea uniformemente sólido (garantizando la seguridad para todos los sistemas consistentes) debe o bien declinar la certificación o devolver un tubo alcanzable con un ancho proyectado arbitrariamente grande, lo que hace que el certificado carezca de información útil.

Metodología: ForeReach
Los autores proponen ForeReach, un certificador de pre-ejecución que navega esta limitación incorporando información lateral. El método opera bajo el siguiente marco:

1. Requisito de Información Lateral: ForeReach requiere un límite de Lipschitz componente a componente ($L$) suministrado sobre un dominio de certificación prescrito ($Z_{cert}$). Este límite debe establecerse independientemente de los datos dispersos (por ejemplo, mediante dinámica analítica con parámetros acotados o un modelo de residuo certificado por separado).
2. Prueba de Consistencia por Pares: Antes de la propagación, el método verifica si los pares de residuos observados contradicen el límite de Lipschitz suministrado. Si $|e_{r_i, k} - e_{r_j, k}| > \sum L_{k\ell}|z_{i,\ell} - z_{j,\ell}| + 2\sigma_k$, la declaración es rechazada y el certificador se abstiene.
3. Envolvente de Pertenencia de Conjunto: Condicionado a que el límite se cumpla, el método construye una envolvente de pertenencia de conjunto para el residuo en cada conjunto de estado-entrada consultado. Esta envolvente se deriva de la intersección de los límites por observación extendidos mediante la constante de Lipschitz (extensión de McShane) y los límites de ruido de observación.
4. Propagación Zonotópica: La incertidumbre se propaga hacia adelante utilizando el modelo nominal $f_0$. El conjunto alcanzable se representa como un zonotopo, incorporando el encierro del mapa nominal (usando límites de Hessiano de intervalo para términos de resto no lineales) y la envolvente del residuo.
5. Lógica de Certificación: El certificador emite un certificado de seguridad solo si:
   • La propagación permanece dentro del dominio de certificación ($Z_{cert}$).
   • Cada sección transversal proyectada del tubo alcanzable evita el conjunto inseguro ($O$).
   • El método distingue entre tres tipos de abstención: contradicción por pares ($\perp_F$), salida del dominio ($\perp_D$) y fallo de seguridad ($\perp_S$).

Contribuciones Clave

1. El Teorema del Trilema: Los autores demuestran un "trilema" para los certificadores deterministas utilizando datos finitos de un solo paso. Un certificador no puede ser simultáneamente:
   • Uniformemente sólido sobre una clase de residuo sin restricciones.
   • $\bar{\rho}$-informativo (devolviendo un tubo con un ancho proyectado finito).
   • Sin restricciones más allá de las observaciones.
     Además, derivan un límite inferior finito, dependiente del plan, sobre el ancho proyectado para clases de error de modelo con suavidad acotada, mostrando que incluso con restricciones de suavidad, un ancho no nulo es forzado por la brecha sin datos.
2. Algoritmo ForeReach: Un método práctico que combina límites de Lipschitz suministrados, comprobaciones de consistencia por pares y propagación zonotópica para proporcionar contención de trayectoria condicional a la validez de la declaración suministrada.
3. Validación Empírica: Experimentos en dos sistemas de referencia (una masa puntual afín y una bicicleta dinámica de seis estados) demuestran que ForeReach se abstiene correctamente cuando los planes entran en regiones no soportadas (asegurando la solidez) mientras recupera la certificación cuando hay datos relevantes del objetivo disponibles.

Resultados Experimentales

• Sistema de Masa Puntual: Las líneas base de calibración global certificaron planes no soportados pero fallaron en contener las trayectorias objetivo (0% de cobertura), resultando en altas tasas de falso-seguridad. ForeReach logró una cobertura completa del tubo en planes no soportados mediante la abstención, y un 99.8% de recuperación certificada en corredores soportados.
• Sistema de Bicicleta Dinámica: Se observaron tendencias similares. La calibración global y otras líneas base (procesos gaussianos, métodos conformes) produjeron tubos poco informativos o fallaron en contener trayectorias en regiones no soportadas. ForeReach mantuvo un 100% de cobertura en planes no soportados (mediante la abstención) y logró un 98.3% de recuperación certificada en corredores soportados con $N=400$ muestras.
• Fragmentos de Acción Aprendidos: Cuando se aplicó a planes generados por una política aprendida, la tasa de abstención se correlacionó fuertemente (Spearman $\rho=0.697$) con la distancia del despliegue nominal del plan al dato más cercano, rastreando efectivamente el "soporte" de los datos.
• Declaraciones Incorrectas: El estudio mostró que si el límite de Lipschitz suministrado es demasiado pequeño (subestimando la regularidad), la prueba por pares puede pasar (si no existe una contradicción local), pero el tubo resultante puede ser demasiado estrecho para contener la trayectoria real, lo que conduce a certificados falsos. Esto resalta que la solidez del método es condicional a la corrección de la declaración externa.

Significado y Reivindicaciones
El artículo sostiene que la limitación principal para certificar planes a partir de datos escasos no es la cantidad de datos, sino la falta de restricciones sobre el error del modelo en regiones no observadas. Los autores argumentan que un certificado utilizable requiere información estructural (como límites de Lipschitz) suministrada desde fuera de los datos. Si bien los datos pueden refutar una declaración incorrecta, no pueden confirmar una correcta en regiones no observadas.

La importancia del trabajo radica en:

• Formalizar los límites teóricos (el trilema) de la alcanzabilidad basada en datos con transiciones dispersas y aisladas.
• Proporcionar un método que intercambia explícitamente entre solidez e informatividad basándose en la validez de la información lateral, en lugar de asumir propiedades globales de la distribución de los datos.
• Demostrar que la "abstención" es un resultado necesario e informativo cuando un plan deja el soporte de los datos, contrastando con las líneas base que pueden producir certificados estrechos pero no sólidos.

Los autores enfatizan que su garantía es condicional: el certificado es válido solo si el límite de Lipschitz suministrado se cumple en todo el dominio de certificación. El método no aprende el límite a partir de los datos dispersos, sino que lo utiliza para construir una envolvente sólida.