Resumen Técnico: VASO – Habilidades Auto-evolutivas Formalmente Verificables para Agentes de IA Física

Declaración del Problema

Las habilidades robóticas reutilizables sirven como la interfaz entre los modelos fundacionales y el control físico, permitiendo que los agentes corporizados ejecuten tareas de largo horizonte bajo restricciones de seguridad. Si bien los modelos fundacionales han reducido el costo de generar estas habilidades a partir de lenguaje natural, no han resuelto el problema de la garantía de la habilidad (skill assurance). Los métodos de auto-evolución existentes dependen de señales de retroalimentación "suaves" —como resultados de ejecución, pruebas unitarias, recompensas del entorno o autocrítica de LLM—; estas señales proporcionan únicamente evidencia a nivel de traza, demostrando que una habilidad funcionó en ejecuciones muestreadas, pero sin garantizar que los planes inducidos por la habilidad satisfagan contratos de seguridad temporal bajo condiciones no probadas. En robótica, una única violación de seguridad rara pero severa (por ejemplo, un robot terrestre moviéndose tras detectar a una persona) es inaceptable, y sin embargo, la retroalimentación suave suele fallar al detectar estos casos límite.

El desafío central es cerrar el bucle entre la verificación formal y la evolución de habilidades sin limitarse a filtrar planes inseguros o ajustar los pesos del modelo. Existe la necesidad de una representación donde los contraejemplos formales puedan actualizar directamente los contratos de habilidades reutilizables, asegurando que las mejoras sean inspeccionables, reutilizables y verificables.

Metodología: Marco VASO

Los autores proponen VASO (Optimización de Habilidades Automatizada Guiada por Verificación), un marco de bucle cerrado para la auto-evolución de contratos de habilidades de robots generados por LLM. VASO opera tratando las habilidades como contratos semánticos que acoplan una interfaz formal con una interfaz orientada al planificador.

1. Representación de Habilidad Verificable

Una habilidad $sk$ se define como una tupla $(G, \psi_{sk}, C_{sk})$:

• $G$ (Especificaciones Globales): Un conjunto de fórmulas LTL que representan las restricciones de seguridad que deben cumplirse siempre.
• $\psi_{sk}$ (Regla Local): Una fórmula LTL que define la intención o el objetivo específico de la habilidad.
• $C_{sk}$ (Contrato Semántico): El componente central que consiste en:
  • $L_{sk}$ (Función de Etiquetado Alineada con Proposiciones): Una función que mapea estados robóticos de bajo nivel, observaciones y comandos de control a proposiciones lógicas atómicas. Esto cierra la brecha entre la ejecución física y la verificación de modelos simbólicos.
  • $C^p_{sk}$ (Plantilla de Plan Basada en Texto): Un sesgo conductual que guía al planificador en la generación de comandos ejecutables (por ejemplo, llamadas a API o trayectorias).

2. Bucle de Verificación de Dos Niveles

VASO emplea un proceso de verificación jerárquico para refinar las habilidades:

• Verificación a Nivel de Habilidad (Comprobación de Factibilidad): Antes de muestrear los planes, el marco verifica si la regla local $\psi_{sk}$ es lógicamente consistente con las especificaciones globales $G$. Se construye un sistema de transición universal para verificar la satisfacción. Si la regla local contradice la seguridad global (por ejemplo, una regla que ordena movimiento cuando se observa a una persona), la habilidad es rechazada y se consulta al modelo fundacional para refinar la regla local.
• Verificación a Nivel de Plan (Comprobación de Comportamiento): Una vez obtenida una habilidad factible, un planificador genera un plan ejecutable $\pi$. Este plan se compila en un sistema de transición simbólico (autómata) utilizando la función de etiquetado $L_{sk}$. Un verificador de modelos (NuSMV) verifica el plan contra $G \land \psi_{sk}$.

3. Optimización mediante Gradientes Textuales

Cuando la verificación falla, el verificador de modelos devuelve un traza de contraejemplo. VASO convierte esta traza en un gradiente textual (por ejemplo, "viola la especificación: $G(\text{persona\_observada} \to X \text{ detener})$"). Esta retroalimentación textual se introduce en el modelo fundacional para actualizar el contrato semántico $C_{sk}$ y la regla local $\psi_{sk}$.

• Restricción Clave: Los pesos del modelo fundacional permanecen congelados. La optimización ocurre enteramente a nivel de prompt/contrato, refinando el artefacto de la habilidad reutilizable en lugar de ajustar los parámetros del modelo o un único prompt de tarea.
• Proceso: El bucle alterna entre la generación hacia adelante (Contrato $\to$ Plan $\to$ Autómata) y el refinamiento hacia atrás (Autómata $\to$ Gradiente Textual $\to$ Contrato Actualizado).

Contribuciones Clave

1. Representación de Habilidad Auto-evolutiva Verificable: El artículo introduce una estructura de habilidad que conecta explícitamente las especificaciones de lógica temporal, la semántica robótica alineada con proposiciones y las plantillas orientadas al planificador. Esto permite que las habilidades generadas por LLM se utilicen para la planificación manteniendo la exposición a la verificación formal.
2. Contraejemplos Formales como Retroalimentación de Optimización: Los autores desarrollan un bucle de verificación de dos niveles donde las trazas de contraejemplos se convierten en gradientes textuales. Esto permite el refinamiento del propio contrato de la habilidad reutilizable, en lugar de simplemente rechazar un plan específico o ajustar un prompt.
3. Validación de Agente Físico: El marco es validado en plataformas robóticas reales (Clearpath Jackal y quadcopter PX4), demostrando que las habilidades optimizadas pueden lograr un alto cumplimiento de las especificaciones formales sin realizar el ajuste fino (fine-tuning) del modelo fundacional subyacente.

Resultados Empíricos

El marco fue evaluado en 11 especificaciones de lógica temporal a través de 400 planes generados en dos plataformas robóticas.

• Cumplimiento: VASO logró un 97.2% de cumplimiento de la especificación formal utilizando menos de 100 muestras de optimización (menos de 20 minutos por habilidad).
• Comparación: Superó a los baselines de cero disparos (zero-shot), a los métodos de optimización de prompts (como LAD-VF) y a los enfoques basados en ajuste fino (como RLVF). Notablemente, VASO alcanzó puntuaciones de seguridad más altas que los métodos de ajuste fino, requiriendo solo una fracción del costo y tiempo de entrenamiento.
• Generalización: Las habilidades optimizadas demostraron una fuerte generalización a prompts de tareas no vistas dentro de la misma familia de tareas, manteniendo altas tasas de seguridad y finalización de tareas sin refinamiento adicional.
• Alineación Automática: El estudio mostró que las funciones de etiquetado alineadas con proposiciones generadas automáticamente funcionaron al mismo nivel que los mapeos hechos a mano, eliminando la necesidad de experiencia manual en la definición de abstracciones simbólicas.

Significado y Reivindicaciones

El artículo afirma ser el primer marco que cierra el bucle entre la verificación formal y la evolución de habilidades generadas por LLM para agentes de IA física.

• Cambio de Paradigma: A diferencia de los procesos estándar de planificación verificada que utilizan la verificación meramente como un filtro de paso/fallo para planes únicos, VASO utiliza la razón del rechazo (el contraejemplo) para mejorar la fuente del plan (la habilidad reutilizable).
• Eficiencia y Seguridad: Al optimizar el contrato de la habilidad en lugar de los pesos del modelo, VASO proporciona un mecanismo para generar comportamientos más seguros y confiables que son inspeccionables y reutilizables en diversas tareas, abordando el cuello de botella crítico de la garantía de las habilidades en la IA física.
• Limitaciones: Los autores reconocen que las garantías formales son condicionales a la corrección de la función de etiquetado alineada con proposiciones generada por IA. Los errores en el mapeo de la dinámica de bajo nivel a proposiciones simbólicas podrían conducir a resultados de verificación espurios, aunque los datos empíricos sugieren que esto ocurre con poca frecuencia (<1% de degradación en las puntuaciones de seguridad). El marco actual también asume la ejecución secuencial, no concurrente.