Résumé Technique : MANTRA – Synthèse de Benchmarks de Conformité Validés par SMT

Énoncé du Problème

Les agents de modèles de langage (LLM) utilisant des outils sont de plus en plus déployés dans des domaines critiques tels que les opérations d'entreprise, la santé et la réservation de voyages, où leur comportement doit respecter des manuels procéduraux stricts. Un défi fondamental dans l'évaluation de ces agents réside dans le « décalage » entre l'entrée et la sortie : les règles procédurales sont généralement rédigées en langage naturel non structuré pour une interprétation humaine, tandis que le comportement de l'agent se manifeste sous la forme d'une séquence d'appels d'outils (traces d'exécution).

Les méthodes d'évaluation existantes souffrent de limitations significatives :

• Construction Manuelle : La création de benchmarks à la main est de haute qualité mais ne s'adapte pas à l'échelle de manuels complexes ou de nouveaux domaines.
• Juges basés sur les LLM : Bien que plus faciles à déployer, ces juges peinent à faire respecter de manière fiable des contraintes temporelles strictes, des préconditions et des actions interdites sur de longues traces d'exécution, conduisant à des évaluations peu fiables.
• Évaluation basée uniquement sur le résultat : De nombreux benchmarks ne vérifient que l'état final, échouant à détecter si un agent est parvenu au bon résultat via un chemin procédural non conforme.

Il manque une méthode évolutive et reproductible pour générer automatiquement des benchmarks de conformité au niveau des traces à partir de manuels en langage naturel, offrant un notation déterministe et vérifiable par machine.

Méthodologie : Le Cadre MANTRA

MANTRA (MANual-to-Test-tRAnslation) est un cadre conçu pour synthétiser automatiquement des benchmarks de conformité à partir de documents procéduraux en langage naturel et de schémas d'outils. Il fonctionne via un pipeline en trois étapes combinant la génération par LLM et la vérification formelle :

1. Ingestion de Documents et Génération de Scénarios

• Construction de Graphes de Dépendance : Le système ingère un manuel procédural ($D$) et construit un graphe de dépendance ($G_D$) où les nœuds représentent des fragments de contenu (par exemple, des paragraphes) et les arêtes représentent des relations hiérarchiques et de référence.
• Échantillonnage Piloté par la Couverture : Pour contrôler la complexité des tâches et assurer une large couverture, MANTRA échantillonne des sous-graphes ($G_{DS}$) à partir de $G_D$. De petits sous-graphes denses génèrent des scénarios simples ; des sous-graphes plus grands ou faiblement connectés induisent des scénarios complexes impliquant plusieurs règles.
• Pertinence des Outils et Synthèse de Scénarios : Pour chaque échantillon, un LLM identifie les outils pertinents ($T_S$) et génère des scénarios concrets ($\lambda$). Chaque scénario comprend une invite en langage naturel ($p_\lambda$) et une valuation de variables, y compris des variables d'état interne (par exemple, « la demande est en attente ») qui sont rendues explicites dans l'invite pour guider l'agent.

2. Génération de Vérifications et Création de Modèle du Monde

Pour évaluer la conformité de manière déterministe, MANTRA génère deux artefacts indépendants pour chaque scénario :

• Vérifications au Niveau des Traces ($C_\lambda$) : Un LLM génère un ensemble de vérifications booléennes spécifiant les appels d'outils requis, les appels interdits et l'ordre temporel (par exemple, check_inventory doit précéder assign_warehouse_picker). Ces vérifications sont ancrées avec des valeurs d'arguments concrètes.
• Modèle du Monde Symbolique ($W_S$) : Indépendamment, un LLM génère un modèle du monde représentant les règles procédurales comme un système de transition d'état. Ce modèle est exprimé dans un Langage Spécifique à un Domaine (DSL) typé définissant les variables d'état, les préconditions des outils et les postconditions. Cette abstraction permet une représentation compacte de logiques procédurales complexes.

3. Cross-Validation par Résolution SMT

L'innovation centrale de MANTRA réside dans l'utilisation de solveurs de Satisfiability Modulo Theories (SMT) (spécifiquement Z3) pour valider de manière croisée les vérifications générées et le modèle du monde.

• Vérification de Modèle Bornée : Tanto $C_\lambda$ que $W_S$ sont compilés en encodages SMT bornés ($b\Phi_h$) sur un horizon de trace $h$.
• Recherche de Conflits : Le système recherche deux types d'incohérences :
  1. Conflit Avant : Des traces qui satisfont les vérifications mais violent le modèle du monde (indiquant que les vérifications sont trop faibles ou le modèle trop restrictif).
  2. Conflit Arrière : Des traces qui satisfont le modèle du monde mais violent une vérification spécifique (indiquant que la vérification est trop restrictive).
• Boucle de Réparation Structurée : Lorsque des conflits sont détectés, MANTRA emploie une boucle de réparation :
  • Résolution du Modèle du Monde : Si plusieurs scénarios provenant du même échantillon partagent un conflit, un LLM propose une réparation partagée au modèle du monde (par exemple, l'ajout d'une précondition manquante).
  • Résolution des Vérifications : Si les conflits persistent, le système identifie et répare des vérifications spécifiques pour des scénarios individuels.
  • Éditions Déterministes : Les réparations sont appliquées via un langage d'édition typé pour garantir la bonne formation, suivies d'une recompilation et d'une revalidation.
• Humain dans la Boucle : Si les réparations automatisées échouent après un nombre défini d'itérations, le système signale le scénario pour un examen humain structuré, où un réviseur peut résoudre manuellement les ambiguïtés.

Contributions Clés

1. Pipeline Automatisé : Un pipeline entièrement automatisé pour convertir des manuels en langage naturel et des schémas d'outils en benchmarks vérifiables par machine, avec une difficulté de tâche contrôlable et une notation déterministe.
2. Formulation à Deux Artefacts : La séparation des vérifications au niveau des traces et des modèles du monde symboliques, qui sont validés de manière croisée par résolution SMT. Cela permet l'identification et la réparation automatiques des incohérences avant l'acceptation des benchmarks, minimisant l'intervention humaine.
3. Suite de Benchmarks : La création d'une nouvelle suite de benchmarks contenant 285 tâches diversifiées réparties sur 6 domaines (Opérations, Sneaky Sasquatch, Sécurité en Cabine, Vente au Détail, Compagnie Aérienne, Télécom). Ces tâches s'adaptent à des manuels procéduraux allant jusqu'à ~16 000 mots et 148 outils, avec un effort humain minimal.
4. Analyse Granulaire des Échecs : Le cadre fournit des vérifications au niveau des traces permettant un débogage détaillé des modes d'échec des agents, distinguant les appels manquants, les violations d'ordre et les actions interdites.

Résultats et Évaluation

Les auteurs ont évalué le cadre MANTRA et les benchmarks résultants en utilisant 6 agents LLM différents.

• Efficacité de Validation : La validation croisée basée sur SMT a validé avec succès une partie significative des cas de test générés automatiquement. Par exemple, dans le domaine « Opérations », 63 cas générés sur 66 ont été validés après des rounds d'affinement avant et arrière.
• Performance des Agents : L'évaluation a révélé que les agents LLM actuels peinent avec la conformité procédurale. Les taux de réussite variaient considérablement selon le domaine, les domaines « Vente au Détail » et « Compagnie Aérienne » (provenant de $\tau$-Bench) s'avérant particulièrement difficiles en raison de l'utilisation complexe des outils plutôt que de la longueur du document.
• Analyse des Modes d'Échec : L'analyse de 10 895 vérifications échouées a montré que 76 % des échecs étaient dus à un « Appel Requis Manquant » (saut d'un outil mandaté) ou à un « Ancrage Manquant » (échec à exécuter le prérequis d'une clause d'ordre).
  • Un motif d'échec dominant était l'« écriture prématurée », où les agents appelaient des outils de type écriture avant d'effectuer les recherches de type lecture nécessaires.
  • Le modèle Qwen3.6:36B a démontré une performance supérieure, en particulier dans les domaines des compagnies aériennes et de la vente au détail, en maintenant une habitude stricte de « lecture avant écriture », atteignant un taux d'écriture prématurée de 0 % dans ces domaines.
• Comparaison avec les Benchmarks Existants : Contrairement aux benchmarks existants qui reposent sur une construction manuelle ou des juges LLM, MANTRA fournit une évaluation déterministe au niveau des traces qui s'adapte à de grands documents non structurés et à de nouveaux domaines avec un effort humain minimal.

Importance et Revendications

L'article revendique que MANTRA démontre la viabilité de combiner la génération automatisée de benchmarks avec des méthodes de validation formellement fondées pour créer des benchmarks évolutifs et fiables pour les agents utilisant des outils.

• Fiabilité : En utilisant des solveurs SMT pour valider de manière croisée les vérifications contre un modèle du monde, MANTRA garantit que les benchmarks sont exempts d'incohérences logiques pouvant résulter d'hallucinations de LLM, offrant un degré de confiance plus élevé dans les résultats d'évaluation par rapport aux approches de type LLM-comme-juge.
• Évolutivité : Le cadre adresse le goulot d'étranglement de l'évolutivité de la création manuelle de benchmarks, permettant l'évaluation d'agents face à des manuels procéduraux complexes et réels (jusqu'à 50+ pages) dans des domaines arbitraires.
• Capacité de Débogage : La granularité des vérifications au niveau des traces permet aux chercheurs de dépasser les métriques simples de réussite/échec pour comprendre des défaillances structurelles spécifiques dans le raisonnement des agents, telles que la tendance à sauter les recherches de prérequis.

Les auteurs positionnent MANTRA non pas comme une garantie autonome de comportement sûr, mais comme un composant critique pour développer des systèmes d'IA plus dignes de confiance dans des contextes critiques pour la conformité, comblant le fossé entre l'apprentissage automatique et la vérification formelle.