Resumen Técnico: MANTRA – Síntesis de Puntos de Referencia de Cumplimiento Validados por SMT

Declaración del Problema

Los agentes de Modelos de Lenguaje Grande (LLM) que utilizan herramientas se despliegan cada vez más en dominios críticos como operaciones empresariales, atención médica y reservas de viajes, donde su comportamiento debe adherirse a manuales procedimentales estrictos. Un desafío fundamental en la evaluación de estos agentes es la "desincronización" entre la entrada y la salida: las reglas procedimentales suelen escribirse como lenguaje natural no estructurado para la interpretación humana, mientras que el comportamiento del agente se manifiesta como una secuencia de llamadas a herramientas (rastros de ejecución).

Los métodos de evaluación existentes sufren limitaciones significativas:

• Construcción Manual: Crear puntos de referencia a mano es de alta calidad, pero no escala a manuales grandes y complejos o a nuevos dominios.
• Jueces Basados en LLM: Aunque son más fáciles de implementar, estos jueces luchan por hacer cumplir de manera confiable restricciones temporales estrictas, precondiciones y acciones prohibidas sobre rastros de ejecución largos, lo que lleva a evaluaciones poco fiables.
• Evaluación Solo por Resultado: Muchos puntos de referencia solo verifican el estado final, fallando en detectar si un agente llegó al resultado correcto a través de un camino procedimental incumplidor.

Existe una falta de un método escalable y reproducible para generar automáticamente puntos de referencia de cumplimiento a nivel de traza a partir de manuales en lenguaje natural que proporcionen una calificación determinista y verificable por máquina.

Metodología: El Marco MANTRA

MANTRA (MANual-to-Test-tRAnslation) es un marco diseñado para sintetizar automáticamente puntos de referencia de cumplimiento a partir de documentos procedimentales en lenguaje natural y esquemas de herramientas. Opera a través de una tubería de tres etapas que combina la generación por LLM con verificación formal:

1. Ingesta de Documentos y Generación de Escenarios

• Construcción de Gráfico de Dependencia: El sistema ingiere un manual procedimental ($D$) y construye un gráfico de dependencia ($G_D$) donde los nodos representan fragmentos de contenido (por ejemplo, párrafos) y las aristas representan relaciones jerárquicas y de referencia.
• Muestreo Impulsado por Cobertura: Para controlar la complejidad de la tarea y asegurar una amplia cobertura, MANTRA muestrea subgrafos ($G_{DS}$) de $G_D$. Los subgrafos pequeños y densos generan escenarios simples; los subgrafos más grandes o débilmente conectados inducen escenarios complejos que involucran múltiples reglas.
• Relevancia de Herramientas y Síntesis de Escenarios: Para cada muestra, un LLM identifica las herramientas relevantes ($T_S$) y genera escenarios concretos ($\lambda$). Cada escenario incluye un prompt en lenguaje natural ($p_\lambda$) y una valoración de variables, incluidas variables de estado interno (por ejemplo, "la solicitud está pendiente") que se hacen explícitas en el prompt para guiar al agente.

2. Generación de Verificaciones y Creación del Modelo del Mundo

Para evaluar el cumplimiento de manera determinista, MANTRA genera dos artefactos independientes para cada escenario:

• Verificaciones a Nivel de Traza ($C_\lambda$): Un LLM genera un conjunto de verificaciones booleanas que especifican llamadas a herramientas requeridas, llamadas prohibidas y ordenamiento temporal (por ejemplo, check_inventory debe preceder a assign_warehouse_picker). Estas verificaciones se anclan con valores de argumentos concretos.
• Modelo Simbólico del Mundo ($W_S$): Independientemente, un LLM genera un modelo del mundo que representa las reglas procedimentales como un sistema de transición de estados. Este modelo se expresa en un Lenguaje Específico de Dominio (DSL) tipado que define variables de estado, precondiciones de herramientas y postcondiciones. Esta abstracción permite una representación compacta de lógica procedimental compleja.

3. Validación Cruzada mediante Resolución SMT

La innovación central de MANTRA es el uso de solucionadores de Satisfacción Modulo Teorías (SMT) (específicamente Z3) para validar cruzadamente las verificaciones generadas y el modelo del mundo.

• Verificación de Modelo Acotado: Tanto $C_\lambda$ como $W_S$ se compilan en codificaciones SMT acotadas ($b\Phi_h$) sobre un horizonte de traza $h$.
• Búsqueda de Conflictos: El sistema busca dos tipos de inconsistencias:
  1. Conflicto Forward: Rastros que satisfacen las verificaciones pero violan el modelo del mundo (lo que indica que las verificaciones son demasiado débiles o el modelo es demasiado restrictivo).
  2. Conflicto Backward: Rastros que satisfacen el modelo del mundo pero violan una verificación específica (lo que indica que la verificación es demasiado restrictiva).
• Bucle Estructurado de Reparación: Cuando se encuentran conflictos, MANTRA emplea un bucle de reparación:
  • Resolución del Modelo del Mundo: Si múltiples escenarios de la misma muestra comparten un conflicto, un LLM propone una reparación compartida al modelo del mundo (por ejemplo, agregar una precondición faltante).
  • Resolución de Verificaciones: Si los conflictos persisten, el sistema identifica y repara verificaciones específicas para escenarios individuales.
  • Ediciones Deterministas: Las reparaciones se aplican mediante un lenguaje de edición tipado para asegurar la buena formación, seguido de recompilación y revalidación.
• Humano en el Bucle: Si las reparaciones automatizadas fallan después de un número establecido de iteraciones, el sistema marca el escenario para una revisión humana estructurada, donde un revisor puede resolver manualmente ambigüedades.

Contribuciones Clave

1. Tubería Automatizada: Una tubería completamente automatizada para convertir manuales en lenguaje natural y esquemas de herramientas en puntos de referencia verificables por máquina con dificultad de tarea controlable y calificación determinista.
2. Formulación de Dos Artefactos: La separación de verificaciones a nivel de traza y modelos simbólicos del mundo, que se validan cruzadamente mediante resolución SMT. Esto permite la identificación y reparación automática de inconsistencias antes de que se acepten los puntos de referencia, minimizando la intervención humana.
3. Suite de Puntos de Referencia: La creación de una nueva suite de puntos de referencia que contiene 285 tareas diversas en 6 dominios (Operaciones, Sneaky Sasquatch, Seguridad de Cabina, Retail, Aerolínea, Telecomunicaciones). Estas tareas escalan a manuales procedimentales de hasta ~16,000 palabras y 148 herramientas, con un esfuerzo humano mínimo.
4. Análisis Granular de Fallos: El marco proporciona verificaciones a nivel de traza que permiten una depuración detallada de los modos de fallo del agente, distinguiendo entre llamadas faltantes, violaciones de ordenamiento y acciones prohibidas.

Resultados y Evaluación

Los autores evaluaron el marco MANTRA y los puntos de referencia resultantes utilizando 6 agentes LLM diferentes.

• Eficiencia de Validación: La validación cruzada basada en SMT validó con éxito una parte significativa de los casos de prueba generados automáticamente. Por ejemplo, en el dominio "Operaciones", 63 de los 66 casos generados fueron validados después de rondas de refinamiento forward y backward.
• Rendimiento del Agente: La evaluación reveló que los agentes LLM actuales luchan con el cumplimiento procedimental. Las tasas de éxito variaron significativamente por dominio, siendo "Retail" y "Aerolínea" (de $\tau$-Bench) particularmente difíciles debido al uso complejo de herramientas más que a la longitud del documento.
• Análisis de Modos de Fallo: El análisis de 10,895 verificaciones fallidas mostró que el 76% de los fallos se debió a "Llamada Requerida Faltante" (saltarse una herramienta mandatoria) o "Anclaje Faltante" (fallar en ejecutar el prerrequisito para una cláusula de ordenamiento).
  • Un patrón de fallo dominante fue la "escritura prematura", donde los agentes llamaron a herramientas de estilo de escritura antes de realizar las búsquedas de estilo de lectura necesarias.
  • El modelo Qwen3.6:36B demostró un rendimiento superior, particularmente en los dominios de Aerolínea y Retail, al mantener un hábito estricto de "leer antes de escribir", logrando una tasa de escritura prematura del 0% en estos dominios.
• Comparación con Puntos de Referencia Existentes: A diferencia de los puntos de referencia existentes que dependen de la construcción manual o jueces LLM, MANTRA proporciona evaluación determinista a nivel de traza que escala a documentos no estructurados grandes y nuevos dominios con un esfuerzo humano mínimo.

Significado y Afirmaciones

El artículo afirma que MANTRA demuestra la viabilidad de combinar la generación automatizada de puntos de referencia con métodos de validación formalmente fundamentados para crear puntos de referencia escalables y confiables para agentes que utilizan herramientas.

• Fiabilidad: Al utilizar solucionadores SMT para validar cruzadamente las verificaciones contra un modelo del mundo, MANTRA asegura que los puntos de referencia estén libres de inconsistencias lógicas que podrían surgir de alucinaciones de LLM, proporcionando un mayor grado de confianza en los resultados de la evaluación en comparación con los enfoques de LLM como juez.
• Escalabilidad: El marco aborda el cuello de botella de escalabilidad de la creación manual de puntos de referencia, permitiendo la evaluación de agentes contra manuales procedimentales complejos y del mundo real (de hasta 50+ páginas) en dominios arbitrarios.
• Capacidad de Depuración: La granularidad de las verificaciones a nivel de traza permite a los investigadores ir más allá de las métricas simples de aprobado/reprobado para comprender fallos estructurales específicos en el razonamiento del agente, como la tendencia a saltarse las búsquedas de prerrequisitos.

Los autores posicionan a MANTRA no como una garantía independiente de comportamiento seguro, sino como un componente crítico para desarrollar sistemas de IA más confiables en entornos críticos para el cumplimiento, cerrando la brecha entre el aprendizaje automático y la verificación formal.