Paper E Experimental Task Book v2 : Vérification et correction d’erreurs Planification du langage UAV pour AAAI

Ce fichier utilise toujours le nom de fichier paper-e-vera-uav-experiment-taskbook-v1-20260517.md car ce tour nécessite une “modification directe sur la version V1”. Le texte, le titre et les notes de version ont tous été mis à niveau vers v2. Cet article n’est pas une ébauche finale, mais un énoncé de tâche expérimentale exécutable : clarifier le positionnement de recherche de l’article E, les documents réels citables, les solutions algorithmiques, la construction de données, les expériences comparatives, les expériences d’ablation, les indicateurs d’évaluation, les limites théoriques d’exhaustivité et les plans de promotion AAAI/T-ITS ultérieurs. L’accent supplémentaire sur le 19/05/2026 est : la prévention des fuites de données, la taxonomie des échecs, la budgétisation des paramètres, les formules d’indicateurs, la planification des graphiques et les risques de conformité AAAI.

---

1. Contexte et objectifs de la recherche

La planification des missions urbaines de drones à basse altitude passe des « itinéraires prédéfinis par l’ingénieur » à des « itinéraires axés sur la mission en langage naturel ». Dans les applications réelles, les opérateurs sont plus susceptibles de donner les instructions suivantes :

• “Vérifiez d’abord la façade est du bâtiment 3, puis rendez-vous au point d’atterrissage sur le toit et attendez.”
• “Évitez l’air au-dessus de l’hôpital et atteignez la zone d’accouchement temporaire dans les 30 secondes.”
• “Si le couloir sud est occupé, contourner le couloir ouest mais garder une distance de sécurité supérieure à 20 mètres partout.”

Ces instructions incluent simultanément la compréhension sémantique, l’ordre temporel, les contraintes spatiales, la sécurité continue de la trajectoire et les jugements d’accessibilité. Les grands modèles linguistiques (LLM) sont efficaces pour comprendre le langage naturel et générer des plans candidats, mais ils ne peuvent pas garantir que le plan de sortie soit exécutable dans l’espace physique, ni garantir que les contraintes de sécurité aérienne soient respectées. Les méthodes formelles sont efficaces pour donner une sémantique vérifiable, telle que la logique temporelle linéaire (LTL) et la logique temporelle du signal (STL), mais les spécifications manuscrites directes nécessitent des connaissances professionnelles et sont difficiles à servir aux opérateurs non experts.

Les travaux existants ont prouvé que la traduction du langage naturel vers LTL peut réduire considérablement le seuil d’écriture des spécifications des tâches du robot. Par exemple, Lang2LTL convertit les commandes de navigation complexes en LTL et effectue une évaluation de généralisation dans des environnements invisibles [1] ; NL2LTL fournit un package Python open source du langage naturel au LTL [2] ; LTLCodeGen utilise la génération de code pour améliorer l’exactitude grammaticale de LTL et l’intègre dans la planification du chemin du robot [3] ; ConformalNL2LTL tente en outre d’utiliser la prédiction conforme pour garantir l’exactitude de la traduction [4]. Ces travaux constituent une base importante pour cette étude.Mais pour les scénarios de drones à basse altitude, il ne suffit pas d’effectuer une simple conversion NL vers LTL. Les missions de drones ont trois exigences supplémentaires :

1. Contraintes de sécurité continues : Les contraintes telles que l’altitude de vol, la vitesse, la distance d’obstacle, la fenêtre temporelle, etc. sont naturellement des contraintes sur les signaux continus et sont plus adaptées pour être évaluées par la robustesse STL.
2. Boucle fermée de trajectoire exécutable : Des spécifications correctes ne signifient pas que la trajectoire est réalisable et doivent être vérifiées par des cartes, des dynamiques et des planificateurs.
3. Les erreurs peuvent être corrigées : les erreurs LLM doivent non seulement être jugées comme des erreurs, mais doivent être converties en contre-exemple ou en retour de robustesse par le vérificateur, puis conduire à la correction LLM.

Par conséquent, cet article propose VERA-UAV : un cadre de planification neuro-symbolique de vérification et de correction d’erreurs pour les tâches en langage naturel des drones. La version AAAI donne la priorité à la réponse à une question centrale :

Étant donné une mission de drone en langage naturel, comment un LLM open source natif peut-il générer des spécifications et des trajectoires de mission LTL/STL vérifiables, réparables et exécutables, plutôt que de simplement générer des plans textuels qui semblent raisonnables mais dont la sécurité n’est pas prouvée ?

La version principale de la conférence AAAI se concentre sur la planification de l’IA, la vérification neuro-symbolique et l’auto-réparation LLM. Le contenu au niveau du système tel qu’AirSim, la véritable logistique à basse altitude et le débit de l’espace aérien multi-UAV sera intégré dans les versions étendues ultérieures du T-ITS.

---

2. Définition du problème et hypothèses de base

2.1 Entrée et sortie

Étant donné une instance de tâche UAV :

Parmi eux, est l’instruction de tâche en langage naturel, est la carte urbaine à basse altitude avec annotation sémantique et est l’état initial du drone. La carte contient les bâtiments, les zones d’exclusion aérienne, l’espace aérien praticable, les points d’atterrissage, les cibles d’inspection, les obstacles dynamiques et les niveaux d’altitude.

Sortie système :

\varphi_{\text{LTL}} = G(\neg collision) \wedge F(reach(goal)) \wedge G(\neg enter(no_fly_zone))

\varphi_{\text{STL}} = G_{[0,T]}(d_{\text{obs}}(t) \ge d_{\min}) \coin G_{[0,T]}(h_{\min} \le h(t) \le h_{\max}) \coin F_{[0,30]}(atteindre(objectif))

Indique que la trajectoire satisfait la spécification ; si , le vérificateur renvoie la clause de violation, le temps de violation et la marge de sécurité minimale.

4.4 Réparation du pilote de contre-exemple

Au lieu de simplement renvoyer « réussite/échec », le validateur renvoie un diagnostic structuré :

{
  "status": "FAILED",
  "stage": "STL_ROBUSTNESS",
  "violated_clause": "G[0,T](distance_to_obstacle >= 10)",
  "counterexample_trace": [
    {"t": 14.2, "x": 38, "y": 51, "z": 30, "distance_to_obstacle": 6.4}
  ],
  "robustness": -3.6,
  "repair_hint": "Increase safety margin or route around building_7 west side."
}

L’invite de réparation de LLM ne nécessite pas de jeu libre, mais nécessite uniquement la modification des champs pertinents dans TaskIR :

你生成的 TaskIR 在 STL 验证中失败。
失败子句：G[0,T](distance_to_obstacle >= 10)
反例：t=14.2s 时距离 building_7 仅 6.4m。
请只修改 route constraint 或 safety margin，不要改变用户原始目标。
输出新的 TaskIR JSON。

L’objectif de cette conception est de réduire l’espace de recherche de LLM et de rendre le comportement de réparation explicable, enregistrable et reproductible.

Si la réparation LLM échoue après des tours consécutifs, le repli de l’énumération des symboles est entré. La portée de l’énumération est délimitée par la profondeur DSL de TaskIR, l’ensemble d’entités de carte, le modèle de contrainte autorisé et l’horizon de tâche maximal. L’enquêteur donne la priorité à l’expansion des champs les plus pertinents en fonction des résultats du diagnostic, tels que la distance de sécurité, le côté du détour, la fenêtre temporelle, la séquence cible et l’aire d’atterrissage de repli.

4.5 Génération de trajectoire

La version AAAI utilise un générateur de trajectoire léger et reproductible :

• Grille 2D A* : pour les tâches de base à éviter et séquentielles.
• Grille 3D A* : utilisée pour les niveaux d’altitude et les corridors urbains de basse altitude.
• RRT* : pour une vérification supplémentaire spatiale continue.
• MPC-lite/lissage de trajectoire : utilisé pour vérifier si le rayon de braquage, le changement de vitesse et le changement de hauteur satisfont aux contraintes dynamiques simplifiées.

Le générateur de trajectoire n’est pas l’innovation de cet article. Sa fonction est de faire progresser le problème de traduction des spécifications jusqu’au niveau de « si la piste exécutable existe réellement ».

---

5. Preuve des propriétés théoriques et de l’exhaustivité relative

La v1 indique uniquement que “la correction des erreurs de vérification peut améliorer la fiabilité”, mais il n’y a pas de limite mathématique. La v2 clarifie les propriétés algorithmiques : VERA-UAV ne prétend pas que le LLM lui-même est complet, mais prétend plutôt avoir une exhaustivité relative sous les hypothèses d’un DSL fini, d’un vérificateur décidable et d’un planificateur sous-jacent complet.

5.1 Cadre formel

Discrétiser la carte urbaine de basse altitude en une carte pondérée limitée :

\tau = (v_0, v_1, \ldots, v_T), \quad (v_t,v_{t+1})\in E.

\mathcal{D}_{H,D} = {\psi : \mathrm{profondeur}(\psi)\le D,\ \mathrm{horizon}(\psi)\le H,\ \mathrm{entities}(\psi)\subseteq \mathcal{E}(\mathcal{M})}.

C(\psi)=(\varphi_{\mathrm{LTL}},\varphi_{\mathrm{STL}}).

V(\tau, C(\psi)) = \begin{cas} \mathrm{PASS}, & \tau \models \varphi_{\mathrm{LTL}}\ \land\ \rho(\tau,\varphi_{\mathrm{STL}})>0,\ \mathrm{ÉCHEC}(\eta), & \text{sinon}, \fin{cas}

\tau \models \varphi_{\mathrm{LTL}} \quad \text{et} \quad \rho(\tau,\varphi_{\mathrm{STL}})>0.

\mathrm{FSR} = \frac{#{\mathrm{incertain\ mais\ renvoyé\ comme\ exécutable}}}{#{\mathrm{tous\ renvoyé\ exécutable}}}.

P = \frac{|\hat{\mathcal{C}}\cap \mathcal{C}^\star|}{|\hat{\mathcal{C}}|}, \quad R = \frac{|\hat{\mathcal{C}}\cap \mathcal{C}^\star|}{|\mathcal{C}^\star|}, \quad F1 = \frac{2PR}{P+R}.

\mathrm{SVR} = \frac{#{\tau : collision \lor nofly \lor altitude_violation \lor \rho(\tau,\varphi_{\mathrm{STL}})\le 0}} {#{\mathrm{trajectoires retournées}}}.

\mathrm{Gap}(\tau)=\frac{J(\tau)-J^\star}{\max(J^\star,\epsilon)}.

\mathrm{FailToPass} = \frac{#{\mathrm{initial\ échec,\ final\ réussite}}} {#{\mathrm{initial\ fail}}}, \quad \mathrm{Contribution de repli} = \frac{#{\mathrm{LLM\ réparation\ échec,\ symbolique\ secours\ réussite}}} {#{\mathrm{final\ pass}}}.