ConformalNL2LTL: Translating Natural Language Instructions into Temporal Logic Formulas with Conformal Correctness Guarantees

Resumen Técnico: ConformalNL2LTL

1. Planteamiento del Problema

La Lógica Temporal Lineal (LTL) es un formalismo estándar para especificar misiones complejas en sistemas autónomos (como vigilancia, cobertura y recolección de datos), ofreciendo garantías de corrección y optimalidad. Sin embargo, definir tareas en LTL requiere un esfuerzo manual significativo y experiencia de dominio.

Para mitigar esto, se han propuesto métodos que traducen instrucciones en Lenguaje Natural (NL) a fórmulas LTL utilizando Modelos de Lenguaje Grandes (LLM). No obstante, estos enfoques existentes carecen de garantías de corrección: los LLMs pueden generar fórmulas incorrectas con alta confianza, lo que resulta en planes de robots que no cumplen con la intención original del usuario. El problema central es diseñar un algoritmo de traducción que garantice una tasa de éxito de traducción definida por el usuario (ej. 99%) en instrucciones no vistas, minimizando al mismo tiempo la intervención humana.

2. Metodología: ConformalNL2LTL

El artículo propone ConformalNL2LTL, un marco de trabajo que integra la Predicción Conformal (CP) con LLMs para traducir NL a LTL de manera iterativa y con garantías probabilísticas.

Componentes Clave:

• Traducción Iterativa como QA: El proceso de traducción se formula como una secuencia de tareas interdependientes de Preguntas y Respuestas (QA). En cada paso $k$, el sistema construye la fórmula LTL añadiendo un operador temporal/lógico o una proposición atómica (AP) basada en la instrucción NL y la fórmula parcial construida hasta ese momento.
• Arquitectura de Dos Modelos:
  • Modelo Principal ($\psi_p$): Genera respuestas iniciales.
  • Modelo Auxiliar ($\psi_{aux}$): Actúa como segundo nivel de verificación cuando el modelo principal tiene incertidumbre.
• Gestión de Incertidumbre mediante Predicción Conformal (CP):
  • En lugar de confiar en la respuesta más frecuente o en puntuaciones de confianza mal calibradas de los LLMs, el método utiliza CP.
  • Se consulta al modelo principal múltiples veces ($m$) para obtener una distribución empírica de respuestas.
  • Se calculan puntos de predicción (conjuntos de respuestas) que contienen la respuesta correcta con una probabilidad garantizada ($1-\alpha$).
  • Si el conjunto de predicción es un único elemento (singleton), se procede. Si es un conjunto grande (alta incertidumbre), se solicita ayuda.
• Mecanismo de Ayuda Jerárquico:
  1. Si el modelo principal tiene alta incertidumbre, se consulta al modelo auxiliar para generar su propio conjunto de predicción.
  2. Se calcula la intersección de los conjuntos de ambos modelos.
  3. Si la intersección es un singleton, se selecciona esa respuesta.
  4. Si la intersección sigue siendo ambigua o vacía, se solicita intervención humana (el usuario elige entre las opciones restantes o detiene el proceso si ninguna es correcta).
• Agnosticismo de Entorno: El algoritmo infiere las proposiciones atómicas (APs) directamente de la instrucción NL y el conjunto de habilidades del robot, sin requerir una lista predefinida de objetos o entornos.

3. Contribuciones Principales

1. Algoritmo con Garantías de Éxito: Es el primer algoritmo de traducción NL-to-LTL capaz de lograr tasas de éxito definidas por el usuario en instrucciones no vistas, basándose en la teoría de Predicción Conformal.
2. Aplicación de CP a LLMs Colaborativos: Extiende el uso de CP a escenarios donde dos LLMs (principal y auxiliar) trabajan juntos, y aplica esto tanto a modelos de código abierto como cerrado (donde no se tienen los logits).
3. Reducción de Intervención Humana: Demuestra teórica y empíricamente que el uso de un modelo auxiliar reduce drásticamente la necesidad de ayuda humana en comparación con métodos que dependen únicamente del usuario para resolver la incertidumbre.
4. Implementación y Datos: Se libera el código y se generan conjuntos de datos para calibración y prueba.

4. Resultados Experimentales

Los experimentos se realizaron en tareas de navegación y manipulación móvil, utilizando GPT-4o como modelo principal y Deepseek v3 como auxiliar.

• Tasas de Éxito vs. Ayuda:
  • Para un objetivo de éxito del 99% ($1-\alpha = 0.99$), el método logró una tasa de éxito empírica del 99.24%.
  • La tasa de ayuda humana fue extremadamente baja (0.378%), y solo el 4% de los escenarios requirieron ayuda humana al menos una vez.
• Impacto del Modelo Auxiliar:
  • Al eliminar el modelo auxiliar, la tasa de éxito se mantuvo teóricamente (98.2%), pero la tasa de ayuda humana se disparó al 7.43% y el 36.5% de los escenarios requirieron intervención humana. Esto confirma que el modelo auxiliar es crucial para mantener la autonomía.
• Comparación con Baselines:
  • ConformalNL2LTL superó a métodos existentes como Lang2LTL, nl2spec y una variante sin CP (UA-NL2LTL) en tasas de traducción, logrando los objetivos de confianza definidos por el usuario mientras que los baselines no ofrecían tales garantías.
• Robustez (Fuera de Distribución - OOD):
  • En escenarios con distribuciones desconocidas (OOD), las garantías teóricas no se mantienen estrictamente, pero el método sigue funcionando razonablemente bien (tasa de éxito ~80-84%) con una intervención humana mínima, superando a los enfoques directos de planificación.

5. Significado e Impacto

El trabajo de ConformalNL2LTL representa un avance significativo en la interacción humano-robot y la robótica basada en formalismos:

• Confianza Operativa: Permite desplegar robots autónomos que reciben instrucciones en lenguaje natural con la seguridad matemática de que la especificación de la tarea será correcta con una probabilidad predefinida.
• Eficiencia de Recursos: Minimiza la carga cognitiva sobre los operadores humanos al reducir drásticamente la necesidad de corregir errores de traducción, haciendo viable el uso de LLMs en sistemas críticos.
• Puente entre IA y Formalismo: Integra la flexibilidad de los LLMs con la rigurosidad de los métodos formales (LTL), permitiendo que los planificadores existentes operen sobre especificaciones generadas por IA con garantías de corrección.

En resumen, ConformalNL2LTL resuelve el problema de la "caja negra" en la traducción NL-LTL, ofreciendo un marco verificable, eficiente y robusto para la especificación de misiones robóticas complejas.