Aller au contenu principal
VeriGraph : graphes de scène pour la vérification de plans de robots
RecherchearXiv cs.RO 

VeriGraph : graphes de scène pour la vérification de plans de robots

1 source couvre ce sujet·Source originale ↗·
Résumé IASource uniqueImpact UE

Des chercheurs ont publié VeriGraph (arXiv:2411.10446v3), un système de planification robotique qui combine des modèles vision-langage (VLM) avec un mécanisme de vérification formelle des actions. Le principe central repose sur l'utilisation de graphes de scène comme représentation intermédiaire : à partir d'images en entrée, le système construit un graphe capturant les objets présents et leurs relations spatiales, puis s'en sert pour valider et corriger en boucle les séquences d'actions générées par un planificateur LLM. Les gains rapportés sur des tâches de manipulation sont significatifs : +58 % de taux de complétion sur les tâches guidées par langage, +56 % sur des puzzles tangram, et +30 % sur les tâches guidées par image, par rapport aux méthodes de référence testées.

Ce résultat pointe un problème structurel bien documenté dans le domaine : les VLM et LLM génèrent des plans plausibles en surface mais géométriquement ou physiquement incorrects, un objet posé sur une surface inexistante, une saisie dans un ordre impossible. VeriGraph traite ce gap en introduisant une couche de vérification symbolique ancrée dans l'état réel de la scène, ce qui réduit les hallucinations de planification sans nécessiter de fine-tuning du modèle sous-jacent. Pour les intégrateurs industriels et les équipes robotique, cela suggère une voie pragmatique : greffer un vérificateur léger sur des LLM généralistes plutôt que de tout réentraîner, ce qui abaisse potentiellement le coût d'adaptation à de nouveaux environnements.

VeriGraph s'inscrit dans un courant de recherche actif autour des architectures hybrides neuro-symboliques pour la robotique, où des travaux comme SayPlan (Rana et al.), LLMTAMP ou les approches PDDL-guided cherchent tous à contraindre la génération de plans par des vérificateurs formels ou géométriques. La nouveauté ici réside dans l'usage du graphe de scène comme interface universelle entre perception et planification. Les auteurs publient le code sur un site dédié, ce qui facilite la reproductibilité, mais les expériences restent en environnement simulé ou de laboratoire contrôlé, aucun déploiement en conditions industrielles réelles n'est mentionné à ce stade.

Dans nos dossiers

À lire aussi

1arXiv cs.RO 

Vérification en temps réel de modèles pour la planification réactive en boucle fermée de robots

Une équipe de recherche a publié une version mise à jour (v2) sur arXiv (2508.19186) d'un article intitulé « Real-Time Model Checking for Closed-Loop Robot Reactive Planning », qui propose une méthode de vérification de modèles (model checking) pour la planification réactive multi-étapes d'un robot autonome. Le constat de départ : les méthodes classiques d'évitement d'obstacles ne raisonnent qu'un pas en avant et se retrouvent souvent piégées dans des minima locaux, par exemple face à une impasse (cul-de-sac) ou un obstacle isolé. Les auteurs ont conçu un petit algorithme de model checking, exécuté directement dans le code du robot, qui génère des plans en temps réel sur un appareil à faible puissance de calcul, sans données pré-calculées ni entraînement préalable. La méthode s'appuie sur des systèmes de contrôle temporaires, activés en chaîne pour contrer les perturbations locales qui écartent le robot de son comportement ou état de repos préféré, et limite l'explosion combinatoire de l'espace d'états en ne travaillant que sur des instantanés temporaires de l'environnement immédiat. La planification multi-étapes repose sur des contre-exemples générés par recherche en profondeur d'abord (depth-first search) et une propriété de chemin en logique temporelle linéaire (LTL) négée. L'intérêt pratique tient à la promesse d'un raisonnement multi-étapes low-cost, sans base de données ni apprentissage profond, embarquable sur du matériel modeste : un argument qui tranche avec la tendance dominante des approches de navigation gourmandes en données et en puissance de calcul. Pour les intégrateurs de robots mobiles critiques (véhicules autonomes, robots de mission), cela ouvre une piste de navigation sûre et déterministe, avec des garanties formelles issues du monde de la vérification logicielle plutôt que des heuristiques d'apprentissage. Les auteurs revendiquent des gains de performance mesurables face à un agent purement réactif limité à un seul pas de raisonnement. Le model checking est historiquement une technique de vérification formelle de logiciels et de systèmes critiques, ici détournée vers la planification de trajectoire en temps réel plutôt que vers l'analyse a posteriori. L'article, positionné comme une étude de cas pédagogique, ne revendique pas de déploiement industriel ni de produit commercialisé : il s'agit de résultats empiriques et de preuves informelles sur deux scénarios contrôlés (impasse et obstacle isolé), présentés comme base pour des travaux futurs en navigation embarquée sûre, notamment pour les véhicules autonomes et la robotique mobile mission-critique.

RecherchePaper
1 source
Modèles fondation vérifiables pour la sécurité des robots
2arXiv cs.RO 

Modèles fondation vérifiables pour la sécurité des robots

Une équipe de chercheurs présente FEARL (Foundation-Enabled Assured Robot Learning), un cadre publié en juin 2026 sur arXiv (2606.23754), conçu pour rendre les modèles de fondation utilisés en robotique formellement vérifiables. L'architecture repose sur une décomposition en deux modules : un grand Contrôleur (C) qui gère la perception haute dimension et le raisonnement sur les tâches, et un petit module de Sécurité (S) alimenté par des capteurs dédiés basse dimension et un embedding contextuel borné fourni par C, qui produit l'action finale. La vérification formelle s'applique uniquement à S, un composant compact dont les contraintes de sécurité, évitement de collision, limites d'espace de travail, peuvent s'exprimer sur des observations de faible dimension. Le cadre a été évalué sur trois domaines robotiques simulés, en intégrant des VLA (Vision-Language-Action) pré-entraînés disponibles sur étagère, et le transfert vers un robot physique a été validé. Ce découplage répond à un blocage concret pour les intégrateurs et équipes de certification industrielle. Des VLA comme Pi-0 (Physical Intelligence), GR00T N2 (NVIDIA) ou OpenVLA sont performants mais formellement opaques, ce qui les rend incompatibles avec les outils de vérification existants et freine leur déploiement dans des environnements à risque. FEARL propose un compromis : le Contrôleur conserve sa pleine expressivité pour le raisonnement, tandis que S reste vérifiable. Le transfert sim-to-real réussi indique que l'interface basse dimension ne dégrade pas les performances réelles, ce qui nuance l'hypothèse selon laquelle la richesse sensorielle serait indispensable à un contrôle fiable. Les approches antérieures pour sécuriser les politiques robotiques reposaient sur le reinforcement learning contraint ou des moniteurs d'exécution superposés, sans garanties formelles sur l'ensemble du pipeline. FEARL s'inscrit dans le champ de l'assured autonomy et constitue l'une des premières architectures à intégrer des VLA pré-entraînés dans une boucle vérifiable. Des acteurs comme Enchanted Tools (France) ou Wandercraft, qui développent des systèmes embarqués à contraintes de sécurité fortes, pourraient directement bénéficier de ce type d'approche. Les prochaines étapes naturelles seraient une validation sur des benchmarks de safety formels (IEC 61508, DO-178C) et des tests sur des manipulateurs industriels en environnement non structuré.

UEEnchanted Tools et Wandercraft, acteurs français développant des robots à fortes contraintes de sécurité embarquée, sont explicitement identifiés comme bénéficiaires directs de cette architecture de vérification formelle des VLA.

RecherchePaper
1 source
Structure de prédiction latente 4D pour la planification robotique
3arXiv cs.RO 

Structure de prédiction latente 4D pour la planification robotique

Structured 4D Latent Predictive Model : un système de prédiction spatiale en 3D pour la planification robotique Une équipe de recherche publie sur arXiv (identifiant 2607.01166v1) un nouveau modèle baptisé « Structured 4D Latent Predictive Model », conçu pour la planification de tâches robotiques. Contrairement aux modèles prédictifs vidéo classiques, qui travaillent sur des séquences 2D, ce système prédit l'évolution de la structure 3D d'une scène dans un espace latent structuré, à partir d'observations visuelles et d'instructions textuelles. Cette représentation peut être décodée vers plusieurs formats 3D, offrant une compréhension plus complète et géométriquement cohérente de la scène. Le modèle sert de planificateur : il génère des scènes futures qui sont ensuite converties en actions exécutables par un module de dynamique inverse conditionné par l'objectif. Selon les auteurs, les expériences montrent une qualité visuelle élevée et une cohérence 3D et multi-vues nettement supérieure aux meilleurs planificateurs vidéo existants, avec de meilleures performances sur des tâches de manipulation complexes, une bonne généralisation à des conditions visuelles inédites, et une validation sur plateformes robotiques réelles. Un site dédié (structured-4d-model.github.io) présente le projet. L'enjeu dépasse la seule prouesse technique. Les modèles vidéo 2D dominent actuellement l'approche « world model » en robotique, notamment dans les architectures VLA (vision-language-action) qui inspirent des systèmes comme Pi-0 ou GR00T N2. Or ces approches peinent souvent à garantir une cohérence physique et spatiale suffisante pour une manipulation fine. En injectant explicitement une structure 3D dans l'espace latent, ce travail répond directement à une limite identifiée du secteur : le fossé entre démonstrations vidéo impressionnantes et exécution fiable sur du matériel réel, un problème central pour les intégrateurs industriels qui cherchent des systèmes robustes plutôt que des démonstrations sélectionnées. Il s'agit toutefois d'une publication académique à ce stade, sans laboratoire ni entreprise identifiés dans le résumé, et sans date de déploiement annoncée. Elle s'inscrit dans une compétition de recherche intense autour des modèles prédictifs pour la robotique, où plusieurs équipes explorent en parallèle des représentations 3D ou 4D pour dépasser les limites du tout-vidéo. Les prochaines étapes dépendront de la publication du code et de tests indépendants sur des plateformes tierces.

RecherchePaper
1 source
TACO : un cadre de test et vérification pour l'optimisation robuste de graphe de poses
4arXiv cs.RO 

TACO : un cadre de test et vérification pour l'optimisation robuste de graphe de poses

Des chercheurs ont publié TACO (Test And Check Optimization), un framework open-source dédié à la robustification de l'optimisation de graphes de poses (PGO), pierre angulaire des systèmes SLAM (Simultaneous Localization and Mapping). Présenté dans un preprint arXiv (2606.29851), le système adresse un problème concret : les mesures aberrantes (outliers) issues d'associations incorrectes de reconnaissance de lieux, phénomène classique en environnements répétitifs (couloirs, entrepôts). TACO repose sur deux composants complémentaires. Le premier, IPC (Incremental Probabilistic Consensus), évalue en ligne la cohérence de chaque fermeture de boucle entrant dans le graphe. Le second, Switchable Outlier Sanitization, s'appuie sur les Switchable Constraints existantes pour purger périodiquement les mesures incohérentes qu'IPC aurait à tort intégrées. Sur des benchmarks 2D et 3D, TACO atteint un taux de succès supérieur à 90 % en 2D et 83 % en 3D, même avec un taux d'outliers pouvant atteindre 50 %, avec des temps de convergence moyens de 45 ms en 2D et 100 ms en 3D. Ces performances positionnent TACO comme une alternative crédible aux méthodes offline état de l'art, tout en restant déployable en temps réel, ce qui est rare dans ce segment. Pour les intégrateurs de robots mobiles (AMR, AGV) et les équipes SLAM embarqué, c'est un signal important : un pipeline PGO robuste aux outliers avec une latence inférieure à 100 ms ouvre la voie à des localisations fiables dans des environnements industriels mal contraints, sans nécessiter de post-traitement offline coûteux. Le fait que la robustesse soit atteinte sans modélisation explicite inlier/outlier simplifie aussi le tuning en production. Le PGO robuste est un champ actif depuis plus d'une décennie, avec des approches comme DCS (Dynamic Covariance Scaling), les Switchable Constraints de Sünderhauf, ou encore les méthodes basées M-estimateurs. TACO s'inscrit dans cette lignée en combinant une évaluation incrémentale probabiliste à une sanitisation rétrospective, là où la plupart des méthodes temps réel font l'un ou l'autre. Les concurrents directs incluent ROBIN, Graduated Non-Convexity (GNC) et ORB-SLAM3 pour le SLAM visuel 3D. Le code est publié en open source, ce qui facilitera l'intégration dans des stacks ROS existants et permettra à la communauté de valider les performances sur des jeux de données propriétaires.

UEFramework open-source intégrable dans les stacks ROS des intégrateurs AMR/AGV européens, sans impact institutionnel direct sur la France/UE.

RecherchePaper
1 source