🤖 AI

Lipschitz Optimization for Formal Verification of Homographies

Cet article présente un cadre de vérification formelle qui dérive des bornes linéaires serrées sur les valeurs de pixels sous des perturbations de mouvement de caméra 3D en exploitant l'optimisation de Lipschitz et la continuité par morceaux des homographies, permettant ainsi les premières garanties rigoureuses de robustesse pour les réseaux de neurones de vision dans des scènes planes sans recourir à des simulations complexes ou à des modèles de substitution.

Auteurs originaux : Jean-Guillaume Durand, Panagiotis Kouvaros, Maxime Gariel, Alessio Lomuscio

Publié 2026-05-25

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Jean-Guillaume Durand, Panagiotis Kouvaros, Maxime Gariel, Alessio Lomuscio

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 enseigniez à un robot à conduire une voiture ou à atterrir sur un avion. Vous lui avez donné un « cerveau » (un réseau de neurones) entraîné à reconnaître des éléments tels que des panneaux stop, des marquages au sol ou des pistes d'atterrissage. Mais il y a un problème : ces cerveaux sont fragiles. Si vous modifiez légèrement l'éclairage, la couleur ou l'angle de la photo, le robot pourrait soudainement penser qu'un panneau stop est un panneau de limitation de vitesse, ou qu'une piste d'atterrissage n'est que de l'herbe.

Pour garantir que ces robots sont sûrs, nous devons prouver mathématiquement qu'ils ne commettront pas d'erreurs, même lorsque les choses deviennent un peu instables. Cet article présente une nouvelle méthode, ultra-précise, pour effectuer cette preuve, spécifiquement lorsque la caméra se déplace dans l'espace tridimensionnel.

Voici la décomposition de leur travail à l'aide d'analogies simples :

1. Le Problème : La « Feuille de Caoutchouc » vs Le « Monde Réel »

La plupart des vérifications de sécurité actuelles pour l'IA sont comme étirer une feuille de caoutchouc sur une image. Elles supposent que si vous faites bouger légèrement les pixels (comme changer la luminosité ou ajouter du bruit statique), l'IA fonctionnera toujours. Cela s'appelle une vérification de « norme $\ell_p$ ».

Mais dans le monde réel, la caméra ne fait pas que faire bouger les pixels ; elle se déplace. Si vous tournez la tête (tangage), l'inclinez (roulis) ou avancez, l'image change d'une manière géométrique complexe.

L'Analogie de l'Article : Imaginez une feuille de papier plate avec un dessin dessus. Si vous ajoutez simplement du bruit, c'est comme saupoudrer du poivre sur le papier. Mais si vous déplacez la caméra, c'est comme regarder ce papier sous un angle différent. Le dessin se déforme, s'étire et s'écrase. Les anciennes vérifications de sécurité « feuille de caoutchouc » sont trop lâches ; elles tentent de couvrir cette déformation avec un nuage géant et flou qui inclut des images impossibles (comme un panneau stop se transformant en pizza). Cela rend la vérification de sécurité inutile car elle ne peut pas prouver que l'IA est sûre.

2. La Solution : La « Carte Magique » (Homographie)

Les auteurs ont réalisé que pour beaucoup de choses qui préoccupent les robots — comme les panneaux routiers plats, le sol ou une piste d'atterrissage — la déformation causée par le déplacement de la caméra suit une règle mathématique spécifique et prévisible appelée homographie.

L'Analogie : Considérez le déplacement de la caméra comme une carte magique. Si vous savez exactement comment la caméra s'est déplacée (par exemple, « tourné de 5 degrés vers la gauche »), vous pouvez tracer une carte parfaite et fermée qui vous indique exactement d'où provient chaque pixel de la nouvelle image dans l'ancienne image. Ce n'est pas une supposition ; c'est une recette géométrique précise.

3. La Méthode : « L'Optimisation de Lipschitz » (La Limite de Vitesse)

Maintenant qu'ils ont la carte magique, ils doivent prouver que l'IA ne sera pas confuse. Le défi est que la carte est non linéaire (elle courbe et tord), ce qui rend difficile le calcul des limites exactes.

Ils ont utilisé une technique appelée Optimisation de Lipschitz.

L'Analogie : Imaginez que vous grimpez une montagne (les valeurs des pixels) et que vous voulez connaître le point le plus élevé que vous pourriez atteindre dans une certaine zone. Vous n'avez pas besoin de grimper chaque centimètre. Au lieu de cela, vous savez que la montagne a une limite de vitesse (la constante de Lipschitz). Vous savez que peu importe à quel point le chemin est raide, vous ne pouvez pas grimper plus vite qu'un certain taux.
En échantillonnant quelques points sur la montagne et en connaissant la « limite de vitesse » du terrain, ils peuvent garantir mathématiquement que le sommet de la montagne (la valeur de pixel dans le pire des cas) ne peut pas dépasser une certaine hauteur. Cela leur permet de tracer un cadre étroit et précis autour de toutes les images déformées possibles.

4. Les Résultats : Plus Rapide et Plus Précis

L'équipe a créé un outil pour effectuer automatiquement ces calculs mathématiques.

Vitesse : Ils l'ont rendu 89 % plus rapide que les méthodes précédentes. C'est comme passer d'un vélo à une voiture de sport pour ces vérifications de sécurité.
Précision : Leur « cadre de sécurité » est 7 % plus serré. Cela signifie qu'ils ne perdent pas de temps à vérifier des scénarios impossibles. Ils vérifient exactement ce qui peut se produire.
Découverte : Lorsqu'ils ont testé cela sur des benchmarks standards d'IA (comme la reconnaissance de chiffres ou de panneaux de signalisation), ils ont découvert que de nombreux modèles d'IA sont très fragiles face aux mouvements de caméra en 3D. Par exemple, un modèle entraîné à reconnaître des panneaux de signalisation pourrait échouer complètement si la caméra s'incline légèrement, même s'il passe tous les anciens tests de « bruit ».

5. Test Réel : La Piste d'Atterrissage

Pour montrer que cela fonctionne dans une situation réelle critique pour la sécurité, ils l'ont testé sur un système conçu pour dire à un pilote si une piste d'atterrissage est visible.

Le Résultat : Le système s'est révélé très fragile. Sous de légers mouvements de caméra (comme un petit coup de bout ou un virage), le système ne pouvait pas garantir qu'il identifierait correctement la piste. Cela met en évidence une vulnérabilité réelle qui doit être corrigée avant qu'une telle IA ne puisse être certifiée pour une utilisation en aviation.

Résumé

En bref, cet article dit : « Arrêtez de deviner comment le mouvement de la caméra affecte l'IA. Nous avons trouvé une carte mathématique précise pour cela, et nous avons utilisé une règle de « limite de vitesse » pour prouver exactement à quel point une IA peut être confuse par des caméras en mouvement. Nous avons découvert que l'IA actuelle est beaucoup plus fragile face aux mouvements que nous ne le pensions, et nous avons construit un outil plus rapide et meilleur pour le prouver. »

Ce travail est une étape cruciale vers la certification de l'IA pour des emplois critiques pour la sécurité comme piloter des drones, conduire des voitures ou atterrir des avions, où une mauvaise supposition n'est pas seulement une erreur — c'est une catastrophe.

Résumé Technique : Optimisation Lipschitzienne pour la Vérification Formelle des Homographies

1. Énoncé du Problème

Le déploiement des réseaux de neurones profonds (DNN) dans des domaines critiques pour la sécurité, tels que la conduite autonome, l'aérospatiale et la santé, nécessite des garanties formelles de robustesse. Les méthodes actuelles de vérification formelle se concentrent principalement sur des perturbations bornées par la norme $\ell_p$ (par exemple, bruit, changements de contraste) agissant directement sur l'espace des pixels. Cependant, ces approches échouent à modéliser adéquatement les perturbations provenant du monde physique 3D, telles que le mouvement de la caméra, les changements de point de vue ou les déplacements de la géométrie de la scène.

Bien que les boules $\ell_p$ puissent théoriquement englober les images résultant de perturbations physiques, elles sur-approximent la véritable variété des images perturbées, conduisant à des bornes lâches et non informatives qui échouent souvent à prouver la robustesse du réseau. Les méthodes existantes pour la robustesse 3D se limitent à des approches statistiques (garanties plus faibles), à des transformations affines 2D (incapables de modéliser les effets de perspective) ou à des simulations complexes nécessitant des modèles de scène 3D explicites. Il existe un vide critique dans la vérification formelle des transformations de géométrie projective, spécifiquement les homographies, qui décrivent la mapping plan-à-plan entre différentes vues d'une surface plane sous un mouvement de caméra 3D.

2. Méthodologie

Les auteurs proposent un cadre de vérification formelle ciblant la robustesse face aux perturbations de mouvement 3D de la caméra de capture, spécifiquement pour des scènes présentant des structures principalement planes (par exemple, marquages au sol, panneaux de signalisation, plans de sol).

2.1. Déduction Analytique des Homographies

La méthode commence par établir une correspondance analytique entre les perturbations de pose de la caméra et les valeurs de pixels.

Modélisation Géométrique : En supposant un modèle de caméra à sténopé et une caractéristique de scène plane (par exemple, $z=0$ dans le repère mondial), les auteurs dérivent la matrice d'homographie $H(\kappa)$ induite par des perturbations de pose de caméra à 6 degrés de liberté (roulis, tangage, lacet et translation).
Paramétrisation : L'homographie est paramétrée par un vecteur $\kappa$ représentant le delta de pose par rapport à une caméra de référence. Pour des scénarios spécifiques (par exemple, rotation pure de lacet), les auteurs dérivent des expressions analytiques explicites pour $H(\kappa)$ et son inverse $H^{-1}(\kappa)$ .
Fonction de Valeur de Pixel : La valeur d'un pixel transformé $G(\kappa)$ est calculée en mapant les coordonnées transformées vers l'image originale via $T^{-1}(\kappa)$ et en appliquant une interpolation bilinéaire. Cela résulte en une fonction non linéaire $G(\kappa) = I \circ T^{-1}(\kappa)$ .

2.2. Approximation Linéaire par Morceaux (PWL) et Optimisation Lipschitzienne

Pour vérifier le réseau, la fonction non linéaire $G(\kappa)$ doit être sur-approximée par des bornes linéaires pouvant être propagées à travers le vérificateur.

Bornes Linéaires par Morceaux : L'espace des paramètres $B$ est partitionné en sous-domaines. Au sein de chaque sous-domaine, la fonction $G(\kappa)$ est approximée par des bornes linéaires ($LB$ et $UB$) dérivées de points échantillonnés, suivant l'approche de Batten et al. [7].
Continuité Lipschitzienne : Pour garantir que les bornes sont sûres (c'est-à-dire qu'elles contiennent strictement les vraies valeurs de la fonction), les auteurs analysent la continuité lipschitzienne de $G(\kappa)$ . Ils dérivent des bornes supérieures analytiques pour la constante de Lipschitz $L$ en calculant le gradient de la transformation inverse $T^{-1}(\kappa)$ .
Gestion des Discontinuités : Les auteurs traitent la non-continuité de l'inverse de l'homographie aux angles critiques (où le dénominateur tend vers zéro). Ils définissent le domaine de différentiabilité $Diff(B)$ et identifient les emplacements candidats pour les gradients maximaux (frontières et valeurs spécifiques d'arctangente) afin de calculer des constantes de Lipschitz valides.
Optimisation : En utilisant l'optimisation lipschitzienne, l'algorithme affine itérativement les bornes. Il évalue la fonction aux points d'échantillonnage et utilise la constante de Lipschitz pour borner le maximum global de la violation de borne. Si la violation de borne dépasse un seuil $\epsilon$ , le sous-domaine est divisé et le processus se répète jusqu'à convergence.

2.3. Implémentation

La méthode est implémentée comme un front-end générant des bornes linéaires pour tout vérificateur en aval. Les auteurs ont adapté le vérificateur VENUS pour gérer ces bornes linéaires par morceaux, renforçant son cadre de propagation de bornes pour dériver des bornes pré-activation à partir de contraintes d'entrée linéaires plutôt que d'intervalles fixes.

3. Contributions Clés

Vérification Formelle des Transformations Projectives : L'article dérive des homographies analytiques induites par des perturbations de pose à 6 degrés de liberté et démontre leur compatibilité avec les contraintes linéaires par morceaux et l'optimisation lipschitzienne. Cela permet d'obtenir des bornes prouvablement serrées sur les valeurs de pixels sous des transformations non affines (projectives).
Implémentation Efficace : Les auteurs fournissent une implémentation efficace qui améliore l'algorithme PWL existant [7]. Les améliorations incluent des corrections de demi-pixel pour des gradients exacts, l'inclusion de valeurs de paramètres omises dans l'ensemble des candidats de Lipschitz, une dichotomie sur l'espace des paramètres et une parallélisation au niveau du pixel.
Étalonnage et Étude de Cas : La méthode est évaluée sur les benchmarks VNN-COMP (MNIST, CIFAR-10, GTSRB) et un classifieur de visibilité de piste d'atterrissage réel.

4. Résultats

Améliorations de Performance : Par rapport à une réimplémentation de l'algorithme PWL [7], la méthode proposée atteint jusqu'à 89 % d'accélération dans le temps d'exécution et 7 % de bornes plus serrées sur des courbes de pixels complexes. Sur de petites transformations, les itérations Branch-and-Bound (BaB) ont été réduites de plus de 71 %.
Découverte de Vulnérabilités : L'évaluation sur les benchmarks VNN-COMP révèle que les réseaux entraînés avec des augmentations de données standard (incluant des attaques de norme $\ell_p$ ) présentent des faiblesses systématiques face aux perturbations géométriques 3D. Par exemple, les modèles GTSRB (conduite autonome) ont montré 0 % de robustesse certifiée face aux perturbations 3D (roulis, tangage, lacet et translation). Même les modèles MNIST et CIFAR ont montré une robustesse significativement plus faible face au tangage, au lacet et à la translation par rapport aux perturbations de norme $\ell_p$ .
Étude de Cas Réelle : Appliquée à un classifieur de visibilité de piste d'atterrissage entraîné sur le jeu de données LARD, la méthode a certifié la robustesse pour seulement 16 % des images de test sous des translations de 10 cm et 1 % sous des rotations de 1°, mettant en évidence des vulnérabilités pratiques dans les systèmes de perception critiques pour la sécurité.
Analyse de Sensibilité : L'étude confirme que la robustesse certifiée diminue à mesure que l'amplitude de la transformation augmente (par exemple, angle de lacet), un défi connu en vérification formelle qui nécessite un découpage du domaine.

5. Importance et Revendications

L'article revendique présenter le premier cadre de vérification formelle pour les transformations de géométrie projective qui ne repose pas sur des simulations complexes, des réseaux de substitution ou des modèles de formation d'image explicites. En tirant parti de la tratabilité analytique des homographies pour les scènes planes, les auteurs comblent le fossé entre la vérification affine 2D et la modélisation complète de la scène 3D.

L'importance réside dans :

Conformité Réglementaire : Fournir les garanties mathématiques requises pour la certification de l'IA dans les industries critiques pour la sécurité (aviation, véhicules autonomes) où le mouvement de la caméra est une source principale d'incertitude.
Avancement Méthodologique : Étendre l'optimisation lipschitzienne et les techniques PWL pour gérer des transformations non affines déformant la perspective, qui étaient auparavant considérées comme analytiquement intraitables pour la vérification formelle.
Insight Pratique : Démontrer que les réseaux actuels de l'état de l'art sont fragiles face aux perturbations 3D réalistes, suggérant que l'entraînement à la robustesse ou la vérification doit évoluer au-delà des contraintes de norme $\ell_p$ pour aborder les variations du monde physique.

Les auteurs maintiennent un ton modeste, reconnaissant que les grandes transformations exacerbent les non-linéarités et que la méthode est actuellement mieux adaptée aux scènes principalement planes avec un parallaxe et une occlusion limités. Ils positionnent leur travail comme un juste milieu principiste pour vérifier une vaste gamme de cas d'usage en robotique et en vision par ordinateur.