⚡ electrical engineering

Learning Linear Temporal Specifications from Demonstrations with Uncertainty

Cet article présente un nouveau cadre pour l'apprentissage de spécifications de logique temporelle linéaire (LTL) minimales à partir de démonstrations incertaines en modélisant l'incertitude des traces via la distance de Hamming et en réduisant le problème à une optimisation pseudo-booléenne, surpassant ainsi les méthodes existantes dans la récupération de formules de vérité terrain sous des conditions de bruit.

Auteurs originaux : Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

Publié 2026-07-14

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Parastou Fahim, Constantino Lagoa, Rômulo Meira-G'oes

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez d'apprendre à un robot comment se comporter en lui montrant une vidéo d'une journée parfaite. Vous voulez que le robot apprenne la règle : « Si la pièce est chaude et occupée, allume la climatisation. » Mais voici le hic : la vidéo que vous avez enregistrée est défectueuse. Peut-être qu'un capteur a eu un raté, qu'une image a été corrompue ou qu'une mesure était légèrement erronée. Le robot voit une version de la journée qui est presque correcte, mais avec des parties floues et incertaines.

La plupart des méthodes existantes pour enseigner aux robots sont comme des professeurs stricts qui supposent que la vidéo est parfaite. Si la vidéo montre la climatisation s'allumer quand la pièce est froide, ces méthodes pourraient être confuses ou inventer des règles bizarres et compliquées pour expliquer l'erreur. Elles supposent que l'erreur est juste une confusion d'étiquetage (comme appeler un chat un chien), mais elles ne tiennent pas compte du fait que la vidéo elle-même puisse être floue ou incomplète.

Ce document présente une nouvelle approche plus indulgente appelée Apprentissage LTL Robuste. Au lieu d'exiger que la vidéo soit parfaite, cette méthode dit : « D'accord, cette vidéo est floue. Imaginons toutes les versions possibles de cette vidéo qui auraient pu causer ce bug. »

La bulle du « Et si ? »

Les auteurs utilisent un outil mathématique appelé distance de Hamming pour créer une « bulle » de possibilités autour de chaque vidéo défectueuse. Voyez cela comme un filet de sécurité. Si votre vidéo enregistrée montre la climatisation s'allumant à l'étape 3, mais que vous savez que le capteur peut être décalé d'une étape, la méthode ne regarde pas seulement l'étape 3. Elle regarde l'étape 2, l'étape 3 et l'étape 4. Elle crée un groupe d'« estimations de traces » : toutes les façons possibles dont la journée aurait réellement pu se dérouler dans cette petite marge d'erreur.

L'idée majeure est la suivante : Nous n'avons pas besoin de savoir exactement quelle version de la vidéo est la vraie. Nous avons seulement besoin de trouver une règle qui fonctionne pour au moins une version à l'intérieur de cette bulle.

La règle du « Groupe »

Dans l'ancienne méthode, si une vidéo était étiquetée « Bon Comportement », le robot devait suivre la règle parfaitement pour cette vidéo spécifique. Si la vidéo était bruitée, le robot échouait.

Dans cette nouvelle méthode, le robot examine l'ensemble du groupe de vidéos possibles. Il demande : « Existe-t-il une version de ce groupe où la règle est respectée ? » Si la réponse est oui, le robot l'accepte. C'est comme un détective qui sait qu'un témoin pourrait être légèrement confus sur l'heure. Au lieu de rejeter le témoin, le détective dit : « Tant que le suspect était dans le bâtiment à un moment donné durant la fenêtre de temps mentionnée par le témoin, l'alibi tient. »

Les résultats : Un examen attentif

Les auteurs ont testé cette idée en utilisant un système de chauffage, ventilation et climatisation (CVC). Ils ont mis en place une règle de vérité terrain : « Toujours, si la pièce est chaude et occupée, alors la climatisation doit s'allumer à l'étape suivante. »

Ils ont ensuite pris cette règle parfaite et ont intentionnellement perturbé les données pour simuler des erreurs de capteurs, créant des fenêtres d'incertitude où les variables étaient modifiées. Ils ont comparé leur méthode à deux autres approches :

Flie : Une méthode standard qui ne gère pas bien l'incertitude.
Flie Modifié : Une version retouchée qui tente de corriger certains problèmes mais suppose toujours que les données sont principalement correctes.

Qu'est-ce qui s'est passé ?

Flie a souvent abandonné complètement les règles temporelles complexes pour apprendre des motifs simples mais erronés comme « Si ce n'est pas chaud, alors il fera chaud plus tard » (ce qui n'a aucun sens).
Flie Modifié a fait mieux, capturant parfois des parties de la règle, mais il inversait souvent la cause et l'effet. Il apprendrait que « Si la climatisation est allumée, alors la pièce est occupée », ce qui est l'inverse de la vérité.
La Méthode Robuste (la nouvelle approche des auteurs) a réussi à récupérer la structure temporelle correcte dans la plupart des cas, mais elle a encore fréquemment inversé la direction causale par rapport à la vérité terrain. Par exemple, alors que la vraie règle est « Occupation + Chaleur $\rightarrow$ Climatisation », la méthode robuste apprend souvent « Climatisation $\rightarrow$ Occupation ». Cependant, malgré cette inversion, elle était bien plus proche du comportement prévu du système que les autres méthodes car elle a réussi à préserver les relations de temps critiques (comme « l'étape suivante ») que les autres avaient manquées.

Cependant, il y a un compromis. Le document note que cette nouvelle méthode prend plus de temps à calculer. Dans les tests CVC, alors que les autres méthodes prenaient environ 0,8 à 4,4 secondes, la méthode robuste a pris entre 6,5 et 73,1 secondes selon la complexité. C'est comme si le robot prenait une grande inspiration et réfléchissait plus intensément pour s'assurer qu'il réussit, plutôt que de simplement deviner rapidement.

Ce que cela signifie (et ce que cela ne signifie pas)

Le document exclut explicitement l'idée que nous puissions simplement ignorer le bruit ou supposer que les données sont parfaites. Il soutient que les méthodes précédentes échouent parce qu'elles traitent les données incertaines comme une simple erreur d'étiquetage, plutôt que comme un signal corrompu.

Les auteurs suggèrent que leur méthode est une direction plus prometteuse pour les applications du monde réel où les capteurs tombent en panne. Ils montrent, par des simulations (en utilisant des données synthétiques et l'exemple du CVC), que leur méthode récupère des formules qui sont « plus étroitement alignées » avec la vérité que les méthodes de pointe actuelles, même si la logique n'est pas toujours parfaite.

Ils ne prétendent pas avoir résolu le problème complètement. En fait, ils admettent que leurs résultats sont « préliminaires ». Ils n'ont pas prouvé que cela fonctionne sur tous les robots possibles ou dans tous les scénarios de catastrophe du monde réel. Ils ont simplement montré que, dans ces tests spécifiques, regarder la « bulle » de possibilités aide le robot à apprendre de meilleures règles que de regarder la vidéo floue seule.

Ainsi, si vous êtes un adolescent curieux construisant un robot qui doit faire face à des capteurs défectueux, ce document suggère : ne vous fiez pas seulement à la vidéo. Imaginez toutes les façons dont elle aurait pu être différente, trouvez une règle qui correspond à au moins une de ces possibilités, et votre robot sera beaucoup moins susceptible de percuter un mur à cause d'un seul pixel défectueux.

Résumé technique : Apprentissage de spécifications temporelles linéaires à partir de démonstrations avec incertitude

Énoncé du problème

Le document traite du défi de l'inférence de spécifications de logique temporelle linéaire (LTL) à partir de démonstrations de systèmes dans des domaines critiques pour la sécurité (par exemple, la robotique, les véhicules autonomes). Alors que les approches existantes pour l'apprentissage de la LTL à partir de traces positives et négatives supposent que les traces elles-mêmes sont correctement capturées et ne tiennent compte que des erreurs de classification d'étiquettes, les données réelles souffrent souvent d'une incertitude de trace. Cette incertitude provient de défaillances de capteurs, d'erreurs de mesure, de pertes de données ou de délais de communication, entraînant des traces corrompues, incomplètes ou incohérentes.

Les méthodes actuelles, qui traitent les traces observées comme étant la vérité de terrain, échouent à récupérer des spécifications précises lorsque le contenu même de la trace est incertain. Les auteurs définissent le Problème d'Apprentissage LTL Robuste : trouver une formule LTL minimale qui explique le comportement du système malgré une incertitude bornée dans les traces observées, plutôt que de supposer que les traces sont parfaitement exactes.

Méthodologie

Le cadre proposé modélise l'incertitude des traces et l'intègre dans un problème d'optimisation pseudo-booléenne. La méthodologie suit les étapes suivantes :

1. Modélisation de l'incertitude des traces

Les auteurs quantifient l'incertitude en utilisant la distance de Hamming entre une trace observée et des traces potentiellement « correctes ».

Groupe d'estimation de trace ( $C^k_{tr}$ ) : Étant donné une trace observée $tr$ et une borne d'incertitude $k$ , l'ensemble des estimations de traces comprend toutes les traces se trouvant à une distance de Hamming de $k$ par rapport à $tr$.
Hypothèse : On suppose que le véritable comportement du système est l'une des traces au sein de ce groupe d'incertitude, et non nécessairement la trace observée elle-même.

2. Formulation de l'apprentissage robuste

Le problème d'apprentissage est reformulé pour gérer ces groupes plutôt que des traces individuelles :

Erreur de classification de groupe : Au lieu d'exiger que chaque trace observée satisfasse la formule, le cadre exige qu'au moins une trace de chaque groupe d'incertitude (pour les traces positives) satisfasse la formule, et qu'au moins une trace de chaque groupe d'incertitude négatif ne la satisfasse pas.
Fonction de perte : Une fonction de perte d'erreur de classification de groupe, $\ell_g$ , est définie. Elle pénalise les cas où aucune trace d'un groupe d'incertitude n'est cohérente avec la formule apprise.

3. Implémentation algorithmique (Optimisation Pseudo-Booléenne)

Le problème est encodé dans une formule propositionnelle $\Phi$ et résolu à l'aide de Max-SMT (spécifiquement l'optimisation pseudo-booléenne). La formule se compose de quatre catégories de contraintes :

Contraintes de syntaxe ( $\Phi_{syn}$ ) : Garantit que la formule apprise respecte une grammaire LTL valide (représentée par un arbre syntaxique).
Contraintes sémantiques ( $\Phi_{sem}$ ) : Encode la relation de satisfaction entre les traces et la formule LTL.
Contraintes de sélection ( $\Phi_{sel}$ ) : Introduit des variables binaires $z_{tr}$ pour sélectionner quelle estimation de trace spécifique d'un groupe d'incertitude est utilisée pour l'apprentissage. Si une trace est sélectionnée ( $z_{tr}=1$ ), elle doit satisfaire (ou ne pas satisfaire) la formule.
Contraintes de groupe ( $\Phi_{grp}$ ) : Une contrainte souple imposant que pour chaque trace observée, au moins une estimation de trace de son groupe d'incertitude soit sélectionnée ( $z_{tr'}=1$ ).

L'objectif est de minimiser la perte d'erreur de classification de groupe (pondérée par le nombre de traces) tout en satisfaisant toutes les contraintes strictes. Cela est résolu en minimisant une fonction d'objectif pseudo-booléenne.

Principales contributions

Nouvelle formulation du problème : Le papier introduit le « Problème d'Apprentissage LTL Robuste », traitant explicitement l'incertitude du contenu des traces (corruption/incomplétude) plutôt que seulement le bruit d'étiquetage.
Modélisation de l'incertitude : L'utilisation de la distance de Hamming pour définir des groupes d'estimation de traces permet au système de considérer une gamme de comportements possibles pour toute observation donnée.
Contraintes basées sur les groupes : Le cadre impose qu'au moins une trace par groupe d'incertitude soit cohérente avec la formule apprise, empêissant l'algorithme d'apprentissage d'être induit en erreur par des points de données corrompus.
Approche d'optimisation : La réduction du problème d'apprentissage robuste à un problème d'optimisation pseudo-booléenne équivalent, soluble via des solveurs SMT (par exemple, Z3).

Résultats expérimentaux

Les auteurs ont évalué leur méthode par rapport aux approches d'apprentissage basées sur SAT de pointe (spécifiquement l'algorithme « Flie » et une variante de « Flie Modifié » qui intègre les contraintes de l'utilisateur) en utilisant deux bancs d'essai :

Système de contrôle CVC (HVAC) : Un scénario réel avec des propositions atomiques pour la température, l'occupation et l'état de la climatisation.
Motifs LTLf synthétiques : Expériences utilisant diverses formules LTL de vérité de terrain avec injection d'incertitude.

Résultats :

Précision : La méthode d'apprentissage robuste proposée a récupéré des spécifications qui étaient plus proches des formules de vérité de terrain par rapport aux méthodes existantes.
Relations temporelles : Alors que les méthodes standards (Flie) échouaient souvent à capturer les dépendances temporelles ou apprenaient des relations spécieuses sous incertitude, et que le Flie Modifié récupérait partiellement les relations mais inversait souvent les directions causales, la méthode robuste a systématiquement préservé les structures temporelles critiques (par exemple, les conditions globales et les dépendances immédiates).
Coût computationnel : La méthode robuste a nécessité plus de temps de calcul que les bases de référence. Les auteurs attribuent cela à la complexité accrue de l'optimisation pseudo-booléenne par rapport au Max-SAT standard.

Signification et affirmations

Le papier affirme que son cadre comble le fossé entre l'apprentissage théorique de la LTL et les scénarios pratiques où les données sont imparfaites. En capturant efficacement l'incertitude lors du processus d'apprentissage des spécifications, la méthode permet l'inférence de formules LTL minimales et interprétables qui reflètent les véritables comportements du système, même lorsque les traces d'entrée sont bruitées ou incomplètes.

Les auteurs positionnent ce travail comme une étape vers une vérification formelle et une synthèse de contrôleurs plus robustes dans les systèmes critiques pour la sécurité. Ils notent modestement que, bien que les résultats soient préliminaires, l'approche offre une direction « plus fondée et prometteuse » par rapport aux méthodes de pointe actuelles qui supposent l'intégrité des traces. Les travaux futurs identifiés concernent le développement de métriques de distance formelles pour comparer quantitativement les spécifications apprises par rapport à la vérité de terrain.