Complete Abstractions of Monotone Control Systems: From Model-based to Data-Driven Systems

Imaginez que vous essayez d'apprendre à un robot comment conduire une voiture en toute sécurité dans une ville très fréquentée. Vous voulez être absolument certain qu'il ne causera jamais d'accident, qu'il ne grillera jamais un feu rouge et qu'il gardera toujours une distance de sécurité avec les autres voitures. C'est le monde de la théorie du contrôle, la science qui consiste à faire se comporter les machines comme nous le souhaitons. Mais les systèmes du monde réel sont désordonnés et complexes. Pour résoudre cela, les ingénieurs utilisent souvent un tour de passe-passe appelé abstraction : ils construisent une version simplifiée, une version « dessin animé », du système réel pour tester leurs idées. Si le dessin animé fonctionne, ils espèrent que le vrai système fonctionnera aussi. Cependant, il y a un piège. Parfois, ces dessins animés sont trop stricts, disant au robot « ne bouge pas ! » alors qu'il pourrait bouger en toute sécurité. D'autres fois, ils sont trop lâches, laissant le robot tenter des choses qui sont en réalité dangereuses. Le grand défi est de savoir exactement à quel point le dessin animé est proche de la réalité, et d'avoir un moyen de resserrer ou d'élargir cet écart chaque fois que nécessaire.

Ce document traite exactement ce problème, mais avec un accent particulier sur les systèmes qui ont un flux « à sens unique », comme l'eau qui descend une pente ou le trafic circulant dans une seule direction. Ce sont des systèmes monotones. Les auteurs, une équipe de chercheurs issus d'universités du Maroc, d'Allemagne, de France et des États-Unis, introduisent une nouvelle façon de construire ces dessins animés de vérification de sécurité. Au lieu de créer un seul modèle simplifié, ils construisent une paire de modèles : une version « super-sûre » qui est très stricte, et une version « super-permissive » qui est très lâche. Imaginez cela comme le tracé d'une zone de sécurité avec deux lignes : une ligne rouge qui dit « Vous ne pouvez absolument pas franchir ceci » et une ligne verte qui dit « Vous pouvez absolument franchir ceci ». Si le robot peut trouver un chemin entre ces lignes, les auteurs peuvent prouver que cela fonctionnera dans le monde réel. S'il ne peut pas trouver de chemin, même dans la version lâche, ils savent avec certitude que le vrai robot ne peut pas le faire non plus. Cette approche par « paire complète » résout un casse-tête de longue date où les ingénieurs restaient dans l'incertitude, ne sachant pas si un échec était dû à un mauvais robot ou simplement à une mauvaise carte.

Le nouveau « Sandwich de Sécurité »

Le cœur de ce papier est un nouvel outil mathématique appelé ASUAS (Approximate Strong Upper Alternating Simulation). En langage clair, il s'agit d'un carnet de règles pour comparer le vrai robot à sa version dessin animé. Les auteurs ont réalisé que pour les systèmes monotones, vous n'avez pas besoin que le dessin animé soit une copie parfaite du réel ; vous avez juste besoin de savoir quel sens est « haut » et quel sens est « bas ».

Ils utilisent ce carnet de règles pour construire leur « Sandwich de Sécurité » :

1. Le pain supérieur (Abstraction Upper-Sparse) : C'est le modèle strict, conservateur. C'est comme un garde de sécurité qui a peur de tout. Si ce modèle dit « Non, vous ne pouvez pas aller là », alors vous pouvez être sûr à 100 % que le vrai robot ne devrait pas non plus y aller. Si vous trouvez un contrôleur (un ensemble d'instructions) pour ce modèle strict, vous pouvez le traduire directement pour le vrai robot, et il sera sûr.
2. Le pain inférieur (Abstraction Lower-Sparse) : C'est le modèle lâche, optimiste. C'est comme un garde de sécurité qui pense que tout va bien. Si ce modèle dit « Non, vous ne pouvez pas aller là », alors le vrai robot ne peut effectivement pas y aller non plus. C'est la partie magique : si le modèle strict échoue mais que le modèle lâche échoue également, vous savez avec certitude qu'aucun contrôleur n'existe pour le vrai robot. Vous arrêtez de perdre votre temps à essayer de résoudre un problème impossible.

Les auteurs prouvent que ces deux modèles forment ensemble une paire d'abstraction complète. Cela signifie qu'ils couvrent tous les cas de figure. Vous n'êtes pas laissé dans le noir à vous demander : « Mon robot a-t-il échoué parce qu'il est cassé, ou parce que ma carte était trop stricte ? » Avec cette paire, vous savez exactement où vous en êtes.

Ajuster l'écart

L'une des caractéristiques les plus intéressantes de ce papier est que les auteurs montrent que vous pouvez ajuster l'écart entre les modèles stricts et lâches. Imaginez que l'espace entre les lignes rouges et vertes est une zone de brouillard où vous n'êtes pas sûr que le robot soit en sécurité. Les auteurs montrent qu'en rendant la « grille » de votre carte plus fine (comme passer d'une image pixélisée à basse résolution à une image haute définition), vous pouvez réduire cette zone de brouillard. Ils fournissent une formule mathématique qui vous indique exactement de quelle finesse votre grille a besoin pour obtenir un certain niveau de précision. Si vous voulez être super précis, vous utilisez simplement une grille plus fine. Cela transforme une supposition vague en un calcul garanti.

Apprendre des données, pas seulement des mathématiques

Le papier ne s'arrête pas à l'utilisation de modèles mathématiques parfaits. Les auteurs savent que dans le monde réel, nous n'avons souvent pas les équations parfaites décrivant le fonctionnement d'un système. Nous n'avons que des données — des journaux de ce que le robot a fait par le passé. Ainsi, ils étendent leur méthode aux systèmes pilotés par les données.

Au lieu d'utiliser les équations de la voiture, ils utilisent un ensemble de données de 10 000 points (dans leurs simulations) collectés à partir des mouvements de la voiture. Ils construisent les modèles stricts et lâches directement à partir de ces données.

• Ils montrent que si vous avez suffisamment de points de données, vous pouvez construire un « modèle strict piloté par les données » qui est tout aussi sûr que celui construit à partir de mathématiques parfaites.
• Ils ont même calculé combien de points de données vous avez besoin pour être confiant dans votre résultat. Pour leur exemple, ils ont trouvé qu'avec environ 517 939 échantillons aléatoires, vous avez une confiance de 90 % que votre carte pilotée par les données est assez précise pour remplacer la carte mathématique.

Le test de conduite de la voiture

Pour prouver que cela fonctionne, les auteurs ont réalisé des simulations avec un modèle de véhicule. Ils ont mis en place un scénario où une voiture (le suiveur) devait rester derrière une autre voiture (le leader) sans collision, tout en maintenant sa vitesse dans des limites sûres.

• Le Résultat : Ils ont construit les modèles stricts et lâches. Le modèle strict leur a donné une « zone de sécurité » plus petite que la zone de sécurité réelle de la voiture, mais ils savaient avec certitude que tout ce qui se trouvait dans cette zone était sûr. Le modèle lâche a donné une zone plus large.
• L'Écart : Lorsqu'ils ont utilisé une grille grossière (moins de points), il y avait un écart notable entre les deux modèles. Mais lorsqu'ils ont suivi leurs propres conseils en utilisant une grille plus fine (280 par 60 états au lieu de 20 par 14), l'écart s'est considérablement réduit. La zone de sécurité du modèle strict correspondait presque parfaitement à la zone de sécurité réelle de la voiture.
• Le Test des Données : Lorsqu'ils sont passés à l'utilisation de données uniquement (sans équations mathématiques), les résultats ont tenu bon. Le contrôleur construit à partir des données était au moins aussi conservateur que celui construit à partir des mathématiques, exactement comme la théorie le prédisait, prouvant que l'approche pilotée par les données est « correcte par construction ».

Ce que cela signifie

Ce papier ne se contente pas de suggérer une nouvelle idée ; il fournit un cadre prouvé avec des garanties mathématiques. Il élimine l'ancienne méthode consistant à deviner si un contrôleur existe ou non. En utilisant ce « Sandwich de Sécurité » de modèles stricts et lâches, les ingénieurs peuvent désormais :

1. Garantir la sécurité : Si le modèle strict fonctionne, le système réel fonctionne.
2. Prouver l'impossibilité : Si le modèle lâche échoue, le contrôle du système réel pour cette tâche est impossible.
3. Contrôler la précision : Ils peuvent ajuster la taille de la grille pour se rapprocher autant de la vérité qu'ils le souhaitent.

Les auteurs précisent toutefois que si cela fonctionne magnifiquement pour les systèmes monotones (comme le flux de trafic ou la signalisation biologique), il s'agit d'un type spécifique de système. Ils suggèrent que des travaux futurs pourraient tenter d'appliquer ces idées à des systèmes plus complexes et mixtes. Mais pour l'instant, ils ont remis aux ingénieurs un outil puissant pour construire des robots plus sûrs et plus intelligents sans avoir à chercher dans l'obscurité.