Résumé Technique : VASO – Compétences Auto-Évolutives Formellement Vérifiables pour les Agents d'IA Physique

Énoncé du Problème

Les compétences robotiques réutilisables servent d'interface entre les modèles de fondation et le contrôle physique, permettant aux agents incarnés d'exécuter des tâches à long terme sous des contraintes de sécurité. Bien que les modèles de fondation aient réduit le coût de génération de ces compétences à partir du langage naturel, ils n'ont pas résolu le problème de l'assurance des compétences. Les méthodes d'auto-évolution existantes reposent sur des signaux de rétroaction « mous » (soft feedback) — tels que les résultats d'exécution, les tests unitaires, les récompenses de l'environnement ou l'auto-critique par LLM. Ces signaux ne fournissent que des preuves au niveau de la trace, démontrant qu'une compétence a fonctionné sur des exécutions échantillonnées, mais sans garantir que les plans induits par la compétence satisfont des contrats de sécurité temporelle dans des conditions non testées. En robotique, une seule violation de sécurité rare mais grave (par exemple, un robot terrestre se déplaçant après avoir détecté une personne) est inacceptable, pourtant le feedback mou échoue souvent à détecter ces cas limites.

Le défi central consiste à boucler la boucle entre la vérification formelle et l'évolution des compétences sans se contenter de filtrer les plans dangereux ou d'affiner les poids du modèle. Il existe un besoin pour une représentation où les contre-exemples formels peuvent directement mettre à jour les contrats de compétences réutilisables, garantissant que les améliorations sont inspectables, réutilisables et vérifiables.

Méthodologie : Cadre VASO

Les auteurs proposent VASO (Verification-Guided Automated Skill Optimization), un cadre en boucle fermée pour l'auto-évolution des contrats de compétences de robots générés par LLM. VASO opère en traitant les compétences comme des contrats sémantiques couplant une interface formelle avec une interface orientée vers le planificateur.

1. Représentation de Compétence Vérifiable

Une compétence $sk$ est définie par un tuple $(G, \psi_{sk}, C_{sk})$ :

• $G$ (Spécifications Globales) : Un ensemble de formules LTL représentant les contraintes de sécurité qui doivent toujours être respectées.
• $\psi_{sk}$ (Règle Locale) : Une formule LTL définissant l'intention spécifique ou l'objectif de la compétence.
• $C_{sk}$ (Contrat Sémantique) : La composante centrale consistant en :
  • $L_{sk}$ (Fonction d'Étiquetage Alignée sur les Propositions) : Une fonction qui mappe les états bas niveau du robot, les observations et les commandes de contrôle vers des propositions logiques atomiques. Cela comble le fossé entre l'exécution physique et la vérification de modèle symbolique.
  • $C^p_{sk}$ (Modèle de Plan Textuel) : Un a priori comportemental qui guide le planificateur dans la génération de commandes exécutables (par exemple, des appels d'API ou des trajectoires).

2. Boucle de Vérification à Deux Niveaux

VASO emploie un processus de vérification hiérarchique pour affiner les compétences :

• Vérification au Niveau de la Compétence (Vérification de Faisabilité) : Avant l'échantillonnage des plans, le cadre vérifie si la règle locale $\psi_{sk}$ est logiquement cohérente avec les spécifications globales $G$. Un système de transition universel est construit pour vérifier la satisfaisabilité. Si la règle locale contredit la sécurité globale (par exemple, une règle ordonnant un mouvement alors qu'une personne est observée), la compétence est rejetée, et le modèle de fondation est interrogé pour affiner la règle locale.
• Vérification au Niveau du Plan (Vérification Comportementale) : Une fois qu'une compétence faisable est obtenue, un planificateur génère un plan exécutable $\pi$. Ce plan est compilé en un système de transition symbolique (automate) en utilisant la fonction d'étiquetage $L_{sk}$. Un vérificateur de modèle (NuSMV) vérifie le plan par rapport à $G \land \psi_{sk}$.

3. Optimisation via des Gradients Textuels

Lorsque la vérification échoue, le vérificateur de modèle retourne une trace de contre-exemple. VASO convertit cette trace en un gradient textuel (par exemple, « violation de la spécification : $G(\text{person\_observed} \to X \text{ stop})$ »). Ce feedback textuel est réinjecté dans le modèle de fondation pour mettre à jour le contrat sémantique $C_{sk}$ et la règle locale $\psi_{sk}$.

• Contrainte Clé : Les poids du modèle de fondation restent gelés. L'optimisation se produit entièrement au niveau du prompt/contrat, affinant l'artefact de compétence réutilisable plutôt que de tuner les paramètres du modèle ou un simple prompt de tâche.
• Processus : La boucle alterne entre la génération directe (Contrat $\to$ Plan $\to$ Automate) et l'affinement inverse (Automate $\to$ Gradient Textuel $\to$ Contrat Mis à Jour).

Contributions Clés

1. Représentation de Compétence Auto-Évolutive Vérifiable : Le papier introduit une structure de compétence qui connecte explicitement les spécifications de logique temporelle, les sémantiques de robot alignées sur les propositions et les modèles orientés planificateur. Cela permet aux compétences générées par LLM d'être utilisées pour la planification tout en restant exposées à la vérification formelle.
2. Contre-exemples Formels comme Feedback d'Optimisation : Les auteurs développent une boucle de vérification à deux niveaux où les traces de contre-exemples sont converties en gradients textuels. Cela permet d'affiner le contrat de compétence réutilisable lui-même, plutôt que de simplement rejeter un plan spécifique ou de tuner un prompt.
3. Validation par Agent Physique : Le cadre est validé sur de véritables plateformes robotiques (Clearpath Jackal et quadricoptère PX4), démontrant que les compétences optimisées peuvent atteindre une haute conformité aux spécifications formelles sans ajustement fin (fine-tuning) du modèle de fondation sous-jacent.

Résultats Empiriques

Le cadre a été évalué sur 11 spécifications de logique temporelle à travers 400 plans générés sur deux plateformes robotiques.

• Conformité : VASO a atteint une conformité aux spécifications formelles de 97,2 % en utilisant moins de 100 échantillons d'optimisation (moins de 20 minutes par compétence).
• Comparaison : Il a surpassé les baselines zero-shot, les méthodes d'optimisation de prompt (comme LAD-VF) et les approches basées sur le fine-tuning (comme RLVF). Notamment, VASO a atteint des scores de sécurité plus élevés que les méthodes de fine-tuning tout en nécessitant une fraction du coût et du temps d'entraînement.
• Généralisation : Les compétences optimisées ont démontré une forte capacité de généralisation à des prompts de tâches inédites au sein de la même famille de tâches, maintenant des taux élevés de sécurité et d'achèvement de tâche sans optimisation supplémentaire.
• Alignement Automatique : L'étude a montré que les fonctions d'étiquetage générées automatiquement et alignées sur les propositions performaient au même niveau que les mappings faits à la main, éliminant ainsi le besoin d'expertise de domaine manuelle pour définir les abstractions symboliques.

Signification et Revendications

Le papier affirme être le premier cadre capable de boucler la boucle entre la vérification formelle et l'auto-évolution des compétences générées par LLM pour les agents d'IA physique.

• Changement de Paradigme : Contra\à la plupart des pipelines de planification vérifiée qui utilisent la vérification simplement comme un filtre passe/échoue pour des plans ponctuels, VASO utilise la raison du rejet (le contre-exemple) pour améliorer la source du plan (la compétence réutilisable).
• Efficacité et Sécurité : En optimisant le contrat de la compétence plutôt que les poids du modèle, VASO fournit un mécanisme pour générer des comportements plus sûrs et plus fiables, qui sont inspectables et réutilisables à travers différentes tâches, répondant ainsi au goulot d'étranglement critique de l'assurance des compétences en IA physique.
• Limites : Les auteurs reconnaissent que les garanties formelles sont conditionnées par la correction de la fonction d'étiquetage alignée sur les propositions générée par l'IA. Des erreurs dans le mapping des dynamiques bas niveau vers les propositions symboliques pourraient entraîner des résultats de vérification fallacieux, bien que les données empiriques suggèrent que cela se produit rarement (<1 % de dégradation des scores de sécurité). Le cadre actuel suppose également une exécution séquentielle et non concurrente.