Résumé Technique : LAD-VF

Énoncé du Problème

Les modèles de langage de grande taille (LLM) offrent une interface flexible pour traduire des instructions en langage naturel en plans d'action exécutables pour la robotique et les systèmes autonomes. Cependant, le déploiement de ces modèles dans des environnements physiques présente un défi critique de sécurité : les LLM souffrent souvent d'hallucinations ou d'un alignement faible, conduisant à des plans qui violent des contraintes physiques ou des spécifications réglementaires.

Les solutions existantes font face à des limitations significatives :

• Alignement basé sur les données (par exemple, DPO, RLHF) : Ces méthodes reposent sur un étiquetage humain coûteux pour créer des ensembles de données de préférence, ce qui les rend difficiles à mettre à l'échelle et moins adaptées aux tâches critiques pour la sécurité où le feedback humain subjectif peut être insuffisant.
• Feedback formel avec ajustement fin (Fine-Tuning) : Les approches récentes utilisent des méthodes formelles (par exemple, la vérification de modèles) pour vérifier les sorties des LLM par rapport à des spécifications logiques. Bien que cela élimine le besoin d'étiquettes humaines, ces méthodes nécessitent généralement l'ajustement des paramètres du modèle. Ce processus est gourmand en ressources, exige d'énormes quantités de données d'entraînement pour la convergence de la perte, et traite le modèle comme une « boîte noire », limitant ainsi l'évolutivité et l'interprétabilité.

Méthodologie : LAD-VF

L'article propose LAD-VF (LLM-Automatic Differentiation Enables Fine-Tuning-Free Robot Planning from Formal Methods Feedback), un cadre qui optimise le comportement des LLM grâce à l'ingénierie de prompts automatique plutôt que par des mises à jour de paramètres.

Cadre Central

LAD-VF fonctionne comme un système en boucle fermée intégrant la vérification formelle à un pipeline d'optimisation de prompts auto-différentiable :

1. Génération de Plan : Le LLM reçoit une description de tâche en langage naturel et un ensemble de prompts ($P$) pour générer un plan exécutable par le robot. Ce plan est converti en un automate formel (spécifiquement dans NuSMV).
2. Vérification Formelle : Un vérificateur de modèles vérifie l'automate généré par rapport à un ensemble de spécifications de sécurité en logique temporelle définies par l'utilisateur ($\Phi$).
3. Calcul de la Perte : Le système calcule une perte quantitative basée sur le résultat de la vérification. La perte ($L$) est définie comme le rapport entre les spécifications violées ($n_f$) et le nombre total de spécifications ($n_{total}$) : $L = n_f / n_{total}$.
4. Optimisation LLM-AutoDiff : Au lieu de rétropropager des gradients à travers les poids neuronaux, LAD-VF traite l'ensemble du pipeline comme un graphe orienté où les nœuds sont des modules LLM ou des modules fonctionnels (comme le vérificateur).
   • Gradients Textuels : La perte est convertie en « gradients textuels » — un feedback en langage naturel décrivant comment améliorer le prompt.
   • Passage Arrière : Un LLM « arrière » analyse l'échec et le contexte du gradient pour générer des modifications textuelles spécifiques du prompt.
   • Passage Avant : Le prompt mis à jour est utilisé pour générer un nouveau plan, itérant jusqu'à ce que le taux de violation soit minimisé.

Le cadre utilise Adalflow pour gérer des flux de travail complexes et séquentiels. Cela permet :

• Gradients de passage : Propager le feedback depuis les nœuds fonctionnels non-LLM (le vérificateur) vers les prompts en amont.
• Gradients séquentiels temporels : S'assurer que les mises à jour respectent l'ordre chronologique des tâches de planification multi-étapes.

Stratégies de Prompting

L'article évalue trois stratégies de prompting au sein de ce cadre :

• Itération unique : Génération directe de l'automate.
• Double itération : Décomposition en étapes en langage naturel avant la génération de l'automate.
• Multi-itération : Génération séquentielle de prédictions partielles, développant le plan étape par étape. Les auteurs constatent que cette stratégie est la plus efficace pour capturer les dépendances séquentielles.

Contributions Clés

1. Adaptation sans Ajustement Fin : LAD-VF élimine le besoin de mises à jour de paramètres coûteuses, permettant une adaptation évolutive des LLM à de nouveaux domaines critiques pour la sécurité sans réentraîner le modèle de base.
2. Perte Textuelle Informée par la Vérification Formelle : L'article introduit une méthode novatrice pour intégrer directement les résultats de la vérification formelle dans la boucle d'optimisation des prompts, convertissant des signaux de réussite/échec épars en gradients textuels exploitables.
3. Compatibilité Modulaire et Interprétabilité : L'approche est compatible avec des architectures de LLM modulaires et offre une haute interprétabilité. Puisque les améliorations sont apportées via des raffinements de prompts auditable plutôt que par des modifications de poids cachées, le processus d'optimisation est transparent.
4. Cadre d'Optimisation Unifié : En étendant l'Ingénierie Automatique de Prompts (APE) à un cadre entièrement auto-différentiable (LLM-AutoDiff), la méthode prend en charge des graphes de calcul complexes et cycliques impliquant à la fois des LLM et des vérificateurs formels.

Résultats Expérimentaux

Les auteurs ont évalué LAD-VF sur des tâches de navigation robotique (robot terrestre Jackal) et de manipulation, en le comparant à des lignes de base incluant des variantes d'Optimisation de Préférence Directe (DPO) (RLVF), un prompting simple (Prompt+Spec), l'apprentissage en contexte (ICL) et TextGrad.

• Performance : LAD-VF a considérablement amélioré la conformité aux spécifications, augmentant les taux de réussite d'environ 60 % à plus de 90 % dans des tâches spécifiques.
• Comparaison avec l'Ajustement Fin : Bien que la ligne de base d'ajustement fin (RLVF) ait obtenu des scores élevés, LAD-VF a atteint des niveaux de performance comparables (par exemple, 0,860 contre 0,978 pour les scores de sécurité dans des configurations spécifiques, et 0,950 lorsqu'il est combiné avec ICL) sans mettre à jour les paramètres du modèle.
• Efficacité : LAD-VF a démontré une efficacité supérieure en termes de données et de calcul, atteignant des scores de sécurité élevés avec moins de la moitié des échantillons d'entraînement requis par les méthodes d'ajustement fin.
• Généralisation : Les prompts optimisés pour des tâches de navigation se sont généralisés avec succès à des tâches hors domaine (livraison intérieure et manipulation de bras robotique) sans ré-optimisation, à condition que seules les descriptions de tâches et les contraintes soient mises à jour.
• Ablation : LAD-VF basé sur Adalflow a systématiquement surpassé TextGrad, en particulier dans les scénarios de prompting multi-itération où les dépendances séquentielles sont critiques.

Signification et Revendications

L'article revendique que LAD-VF présente une voie évolutive et interprétable vers des systèmes de contrôle pilotés par des LLM vérifiés formellement et dignes de confiance. En déplaçant l'objectif d'optimisation des poids du modèle vers les prompts, la méthode répond aux goulots d'étranglement de l'évolutivité de l'ajustement fin tout en maintenant les garanties de sécurité rigoureuses des méthodes formelles. Les auteurs affirment que cette approche permet l'évolution autonome des agents IA dans des domaines critiques pour la sécurité, sans les coûts prohibitifs de l'étiquetage humain ou des ressources informatiques massives, offrant une alternative pratique aux techniques d'alignement traditionnelles.