Can LLMs Prove Robotic Path Planning Optimality? A Benchmark for Research-Level Algorithm Verification

Título: ¿Pueden los LLMs Demostrar la Optimalidad de la Planificación de Rutas Robóticas? Un Benchmark para la Verificación de Algoritmos a Nivel de Investigación

1. El Problema

La planificación de rutas robóticas es fundamentalmente un problema NP-duro. Las soluciones prácticas dependen de algoritmos de aproximación que ofrecen garantías de rendimiento (relación de aproximación) para casos generales. Sin embargo, mientras que diseñar estos algoritmos es complejo, demostrar formalmente su optimalidad de aproximación es una tarea aún más exigente.

Estas demostraciones requieren:

• Conocimiento geométrico específico del dominio.
• Razonamiento matemático de múltiples pasos sobre restricciones operativas complejas (presupuestos de energía, restricciones de terreno, etc.).
• La conexión de descripciones de tareas concretas con condiciones matemáticas abstractas.

A pesar del rendimiento superior de los Modelos de Lenguaje Grandes (LLMs) en benchmarks matemáticos generales (como MATH o GSM8K), su capacidad para asistir en demostraciones de optimalidad a nivel de investigación en planificación robótica ha estado poco explorada. El desafío radica en que estos problemas no son autocontenidos como los ejercicios de olimpiadas; requieren integrar definiciones de algoritmos, entornos y objetivos de optimalidad con teoremas y lemas específicos del dominio.

2. Metodología

Los autores introducen el primer benchmark diseñado específicamente para evaluar la capacidad de los LLMs en la generación de demostraciones de relación de aproximación para algoritmos de planificación de rutas.

• Construcción del Dataset:

  • Se recopilaron 34 tareas de demostración extraídas de 11 artículos revisados por pares en robótica.
  • Los problemas cubren áreas como navegación consciente de la energía, enrutamiento con restricciones de percepción, misiones críticas en tiempo y balanceo de carga multi-robot.
  • Cada tarea incluye: la formulación del problema ($T$), la descripción del algoritmo ($A$), y opcionalmente, un conjunto de lemas en contexto ($C$) y la relación de aproximación posterior ($\alpha$).
  • Anonimización: Se eliminaron los nombres de algoritmos y problemas clásicos (ej. TSP, k-TSP) para evitar que los modelos recurren a la memorización de datos contaminados en lugar de razonar genuinamente.

• Configuración Experimental:
  Se evaluaron modelos de vanguardia (GPT-5.2, Gemini 3 Pro, Grok 4.1, Qwen 3.5) bajo cuatro configuraciones de disponibilidad de información:

  1. Sin contexto: Solo la definición del problema y el algoritmo.
  2. Con contexto aumentado: Se añaden lemas clave extraídos de la demostración original.
  3. Con ratio posterior (Oracle): Se proporciona la relación de aproximación correcta ($\alpha$) sin lemas.
  4. Contexto + Ratio posterior: Combinación de ambos.

• Evaluación:
  Se utilizó un enfoque de "LLM como juez" (GPT-5.2) validado por humanos para puntuar las demostraciones generadas en tres dimensiones (escala 1-10):

  • Respuesta Final: Precisión de la relación de aproximación.
  • Corrección del Razonamiento: Validez lógica de los pasos, penalizando inferencias no justificadas o errores de desigualdad.
  • Relevancia de la Prueba: Grado en que la prueba se basa en el contexto proporcionado y evita alucinaciones.

3. Contribuciones Clave

1. Primer Benchmark de Nivel de Investigación: Creación de un conjunto de datos estandarizado de 34 problemas de demostración de optimalidad en robótica, superando la brecha entre benchmarks matemáticos generales y problemas de investigación específicos.
2. Análisis de la Necesidad de Conocimiento de Dominio: Demostración empírica de que los LLMs, incluso los más potentes, no pueden generar pruebas válidas sin conocimiento experto externo (lemas específicos).
3. Jerarquía de Técnicas de Prompting: Identificación de que los lemas en contexto son significativamente más efectivos que el Chain-of-Thought (CoT) genérico o la provisión de la respuesta correcta (ratio posterior) por sí sola.
4. Taxonomía de Errores Finos: Desarrollo de un análisis detallado que clasifica los fallos en errores lógicos (sobre-generalización, omisión de casos) y alucinaciones (asunciones no soportadas), y correlaciona la posición del primer error con la calidad general de la prueba.
5. Pipeline Automatizado: Liberación de una herramienta para extraer y formalizar algoritmos de planificación de rutas desde artículos científicos en formato estructurado.

4. Resultados Principales

• Dificultad sin Contexto: En la configuración sin contexto (Setting-1), incluso los modelos más avanzados fallaron masivamente. La tasa de éxito (puntuación $\ge$ 7 en respuesta y razonamiento) fue máxima del 26.47% (GPT-5.2), y muchos modelos obtuvieron puntuaciones muy bajas.
• Impacto de los Lemas en Contexto: Proporcionar lemas relevantes (Setting-2) mejoró drásticamente el rendimiento. El modelo de código abierto Qwen 3.5 superó a otros modelos propietarios cuando se le proporcionó contexto específico, alcanzando una tasa de éxito del 44.12%.
• Utilidad del Ratio Posterior: Proporcionar la respuesta correcta ($\alpha$) sin lemas (Setting-3) ayudó moderadamente, pero no fue suficiente para reconstruir la lógica de la prueba. Sin embargo, en combinación con los lemas (Setting-4), actuó como un "ancla de consistencia", mejorando aún más la corrección del razonamiento.
• Ineficacia del CoT Genérico: El Chain-of-Thought genérico, por sí solo, no redujo significativamente la dificultad de la tarea. Solo fue beneficioso cuando se combinó con conocimiento posterior correcto.
• Correlación de Errores: Se encontró una correlación negativa entre la puntuación de razonamiento y la posición del primer error. Los errores tempranos (al inicio de la prueba) se propagan y comparten, llevando a demostraciones inválidas. La provisión de lemas empuja la aparición del primer error más adelante en la cadena de razonamiento.

5. Significado e Implicaciones

Este trabajo establece que la capacidad de los LLMs para razonar sobre la optimalidad de algoritmos robóticos no es una habilidad intrínseca que se transfiera automáticamente desde benchmarks matemáticos generales.

• Validación Automatizada: Para que los LLMs sean útiles en la validación formal de algoritmos robóticos, es imperativo proporcionarles conocimiento estructurado del dominio (lemas, teoremas geométricos) en el contexto de la entrada.
• Futuro de la Investigación: Sugiere que el desarrollo de algoritmos de planificación asistidos por IA requerirá bibliotecas de conocimiento modular y reutilizable (lemas y esquemas de prueba) en lugar de depender únicamente de la capacidad de razonamiento puro del modelo.
• Direcciones Futuras: Los autores proponen integrar modelos de visión-idioma (VLMs) para verificar invariantes geométricas y desarrollar entornos de entrenamiento que castiguen específicamente las inferencias no soportadas y las alucinaciones de restricciones.

En resumen, el estudio demuestra que, aunque los LLMs actuales no pueden "descubrir" demostraciones de optimalidad complejas desde cero, pueden convertirse en herramientas poderosas de verificación y generación si se les dota de la estructura lógica y el conocimiento especializado adecuado.