Les machines modernes prennent de plus en plus leurs propres décisions dans le monde réel, des voitures autonomes naviguant dans des rues animées aux drones livrant des colis. Ces systèmes reposent souvent sur des programmes informatiques complexes, incluant l'intelligence artificielle, qui agissent comme des « boîtes noires ». Nous savons qu'ils fonctionnent, mais nous ne pouvons pas toujours voir exactement comment ils réfléchissent ou prédire chaque mouvement possible qu'ils pourraient faire. Pour garantir la sécurité de ces machines, les ingénieurs utilisent une technique appelée abstraction. Ils remplacent la réalité complexe et continue d'un objet en mouvement par un modèle simplifié, étape par étape, composé de blocs distincts. Cela leur permet de vérifier si la machine va s'écraser ou échouer avant même qu'elle ne quitte le laboratoire. Cependant, il y a un piège. Pour être sûrs, ces modèles simplifiés doivent être conservateurs ; ils doivent supposer le pire scénario pour chaque mouvement. S'ils sont trop conservateurs, ils deviennent encombrés de dangers imaginaires et impossibles qui n'arrivent jamais en réalité. Ce problème de « fausse alerte » rend les modèles si volumineux et désordonnés que les ordinateurs ne peuvent pas les analyser à temps, laissant les ingénieurs incapables de certifier la sécurité des systèmes mêmes qu'ils ont conçus.

Une équipe de chercheurs de l'Université de Floride a développé une nouvelle méthode pour résoudre cet équilibre délicat. Ils ont créé un outil appelé S3, qui agit comme un guide fluide pour affiner ces modèles simplifiés. Au lieu de deviner comment disposer les blocs du modèle, les chercheurs ont construit un objectif mathématique qui peut être ajusté et amélioré à l'aide de techniques d'optimisation standard. Cet outil permet d'ajuster automatiquement la taille et la forme des blocs du modèle afin d'éliminer les dangers imaginaires inutiles tout en maintenant la sécurité du modèle. En testant cette approche sur trois scénarios différents — un système spiralé, un robot de type unicycle et une voiture simulée grimpant une colline — ils ont constaté que leur méthode produit des modèles bien plus précis et beaucoup plus rapides à calculer que les techniques précédentes. Le résultat est un moyen de vérifier la sécurité de machines complexes et intelligentes sans se laisser accaparer par des avertissements excessifs et irréalistes.

Le défi central de la vérification de ces machines réside dans la tension entre la sécurité et la praticité. Lorsque les ingénieurs construisent un modèle simplifié d'un système en mouvement, ils doivent s'assurer que chaque mouvement réel est couvert par le modèle. Si le modèle manque un chemin réel, il est dangereux. Pour garantir cela, le modèle inclut souvent des chemins supplémentaires que la machine réelle ne pourrait jamais prendre. Ces chemins supplémentaires sont les comportements « spécieux » mentionnés précédemment. C'est comme dessiner une carte qui inclut toutes les routes possibles, y compris celles qui sont bloquées par des murs ou qui mènent au bord d'une falaise, juste pour être sûr de ne pas manquer une voie valide. Bien que cela garantisse que vous ne manquerez pas un danger réel, cela crée une carte si encombrée de cul-de-sac qu'elle devient inutile pour planifier un voyage. Les chercheurs avaient besoin d'un moyen d'élaguer ces cul-de-sac sans couper de vraies routes.

Pour y parvenir, l'équipe s'est concentrée sur un type spécifique de relation mathématique appelée simulation. Dans ce contexte, une simulation est une façon de vérifier si le modèle simplifié peut imiter le comportement du système réel. Si le modèle est « sain » (sound), cela signifie que le système réel ne peut jamais faire quelque chose que le modèle ne permet pas. Les chercheurs voulaient minimiser l'erreur de « simulation inverse », qui mesure à quel point le modèle surestime les possibilités du système. Une erreur élevée signifie que le modèle est trop conservateur, rempli de trop de chemins fictifs. Le problème était que la méthode standard pour mesurer cette erreur était trop lente et trop accidentée pour être améliorée automatiquement. C'était comme essayer de lisser une feuille de papier froissée à la main, un petit pli à la fois, sans outil pour guider vos doigts.

La percée des chercheurs a été de créer un « substitut » (surrogate), un substitut fluide et facile à calculer pour la mesure d'erreur difficile. Ils ont dérivé une nouvelle fonction objectif qui approxime l'erreur dans le pire des cas mais qui se comporte de manière fluide, permettant l'utilisation de l'optimisation basée sur le gradient. Imaginez cela comme le remplacement d'un sentier de montagne escarpé et rocailleux par une colline douce et vallonnée qui mène au même sommet. En suivant la pente de cette colline douce, l'ordinateur peut rapidement trouver la meilleure disposition des blocs du modèle. Ce processus implique d'ajuster les écarts entre les blocs, en les rendant plus larges ou plus étroits selon les zones où le système se déplace de la manière la plus imprévisible. La méthode garantit que le modèle résultant reste sûr par construction, ce qui signifie qu'il ne manque jamais un chemin réel, mais qu'il élimine agressivement les chemins fictifs.

L'équipe a testé cette approche sur trois systèmes distincts pour voir si elle fonctionnait en pratique. Le premier était un système bidimensionnel simple qui spiralait vers une cible. Le second était un robot unicycle tridimensionnel qui devait naviguer autour d'un obstacle pour atteindre un but. Le troisième était une simulation d'une voiture tentant de grimper une colline escarpée, un défi classique en robotique où la voiture doit accumuler de l'élan pour atteindre le sommet. Dans chaque cas, ils ont comparé leur nouvelle méthode à deux stratégies établies : une qui affine le modèle uniquement lorsqu'elle trouve une erreur spécifique, et une autre qui tente d'optimiser la taille de la grille à l'aide d'une forme fixe. Les résultats ont montré que la nouvelle méthode était nettement plus rapide. Pour le robot unicycle, la nouvelle approche a pris environ 140 secondes pour construire et vérifier le modèle, tandis que l'ancienne méthode de raffinement a pris plus de 1 900 secondes. Pour la voiture grimpant la colline, la nouvelle méthode a pris environ 12 secondes contre près de 100 secondes pour l'ancienne méthode.

Au-delà de la vitesse, la qualité des modèles s'est améliorée. Les chercheurs ont mesuré la capacité des nouveaux modèles à prédire le comportement du système et ont constaté qu'ils étaient beaucoup moins conservateurs. Dans le test de l'unicycle, la nouvelle méthode a réduit l'erreur moyenne de manière significative, ce qui signifie que le modèle contenait beaucoup moins de chemins impossibles. Pour la voiture sur la colline, la nouvelle méthode a permis au modèle de vérifier une plus grande partie des positions de départ qui mèneraient réellement au succès. Cela est crucial car un modèle trop conservateur pourrait dire à un ingénieur qu'une voiture ne peut pas grimper la colline depuis un certain point, alors qu'elle le peut réellement. En réduisant ce faux conservatisme, la nouvelle méthode donne aux ingénieurs plus de confiance dans le fait que leurs systèmes fonctionneront comme prévu.

L'étude a également révélé comment le nouvel outil se comporte sous différentes configurations. Les chercheurs ont découvert qu'ils pouvaient régler l'outil pour qu'il se concentre soit sur le pire scénario, soit sur le comportement moyen du système. Si l'objectif est d'assurer une sécurité absolue contre les possibilités les plus extrêmes, l'outil peut être paramétré pour donner la priorité à l'erreur du pire cas. Si l'objectif est d'obtenir une meilleure image globale de la manière dont le système se comporte habituellement, l'outil peut être ajusté pour se concentrer sur la moyenne. Cette flexibilité permet aux ingénieurs de choisir le bon équilibre pour leurs besoins spécifiques. L'équipe a également observé que l'outil apprenait naturellement à rendre les blocs du modèle plus petits dans les zones où le système se déplace rapidement ou change de direction brusquement, et plus grands là où le mouvement est régulier. Cette granularité adaptative est exactement ce qui est nécessaire pour créer des modèles efficaces sans gaspiller de puissance de calcul dans des zones faciles à prédire.

Les implications de ce travail s'étendent au-delà de ces trois exemples. La méthode fournit un cadre général pour rendre la vérification des systèmes complexes et intelligents plus pratique. À mesure que les machines deviennent plus autonomes et sont déployées dans des environnements critiques pour la sécurité, la capacité de vérifier rapidement et précisément leur sécurité est primordiale. Le nouvel outil ne nécessite pas que les ingénieurs connaissent exactement le contrôleur utilisé par la machine ; il fonctionne avec la dynamique connue du système et le comportement du contrôleur. Cela le rend applicable à un large éventail de scénarios, des robots industriels aux véhicules autonomes. Les chercheurs ont mis leur code à la disposition du public, invitant d'autres personnes à construire sur cette base.

En fin de compte, ce travail démontre qu'il est possible d'avoir à la fois la sécurité et l'efficacité dans la vérification de systèmes complexes. En remplaçant une mesure difficile et accidentée par un guide fluide et optimisable, les chercheurs ont ouvert une nouvelle voie aux ingénieurs pour concevoir et certifier la prochaine génération de machines intelligentes. La méthode ne promet pas de résoudre tous les problèmes de l'intelligence artificielle, mais elle offre un moyen concret et fiable de garantir que les systèmes sur lesquels nous comptons sont non seulement intelligents, mais aussi sûrs. La capacité d'éliminer le bruit des fausses alertes pour se concentrer sur les risques réels est une étape importante dans le domaine de l'ingénierie de confiance.