Imaginez que vous essayez d'enseigner à un artiste très créatif et imaginatif (une IA) comment sculpter une statue dans un bloc de marbre à l'aide d'un bras robotique. L'artiste excelle à comprendre votre description (« Créez un oiseau ») et peut rédiger les instructions pour le robot. Cependant, cet artiste n'a jamais réellement vu l'atelier. Il ne sait pas où se trouvent les lourdes équerres maintenant le marbre, ni la taille du bras du robot. Il pourrait rédiger des instructions qui semblent parfaites sur papier mais qui pousseraient le robot à s'écraser directement contre une équerre, brisant la machine.

Ce papier propose une solution à ce problème en associant l'artiste créatif à un inspecteur de sécurité strict et mathématiquement parfait.

Voici comment fonctionne leur partenariat, décomposé en étapes simples :

1. Les Deux Partenaires

L'Artiste (L'IA) : Il s'agit d'un grand modèle de langage (spécifiquement un appelé GLLM), issu de travaux antérieurs. Il est excellent pour transformer votre requête en langage naturel (« Sculptez un oiseau ») en une liste d'instructions robotiques (G-code). Il gère l'infusion de contexte (RAG) pour intégrer les informations sur la machine et la tâche, et vérifie que le code est syntaxiquement et sémantiquement raisonnable. Ce qu'il ne fait pas, et pour quoi il n'a jamais été conçu, c'est empêcher le robot de s'écraser physiquement contre des objets ; il ne possède aucune détection de collision intégrée.
L'Inspecteur (Le Moteur Logique) : Il s'agit d'un prouveur basé sur la « Logique de Séparation », issu des travaux précédents des auteurs (notamment l'article Separation Logic for Verifying Physical Collisions of CNC Programs, arXiv:2605.10437), où le modèle du « Tas Spatial » et le prouveur ont été introduits. La seule tâche de l'Inspecteur est de détecter les collisions physiques — des situations où l'outil et un obstacle tenteraient d'occuper le même espace au même moment. Ce n'est pas un réviseur de code généraliste ; il ne vérifie pas si le code est « faux » dans un sens large, il est purement un détecteur de crash.

Ce papier apporte spécifiquement le câblage entre ces deux outils existants : une boucle de rétroaction neuro-symbolique où les résultats de collision de l'Inspecteur sont traduits en guidage structuré pour l'Artiste.

2. Le « Bac à Sable Numérique » (Le Tas Spatial)

Pour que les mathématiques fonctionnent, le système transforme l'atelier physique en une immense grille 3D de petits cubes (comme une version 3D de Minecraft).

Certains cubes sont marqués comme « Marbre » (le matériau à découper).
Certains sont marqués comme « Équerres » (obstacles).
Certains sont marqués comme « Air Vide » (espace sûr).
L'outil du robot est également une forme spécifique de cubes.

L'Inspecteur ne regarde pas le robot bouger et ne lance jamais de simulation géométrique. Il lit le script G-code directement, ligne par ligne, et calcule quels cubes chaque mouvement d'outil devrait occuper. La règle qu'il applique est simple : Les cubes revendiqués par l'outil ne doivent pas déjà être revendiqués par une équerre ou tout autre obstacle.

3. La Zone Tampon de Sécurité (Le « Manteau Fluffy »)

Les robots ne sont pas parfaits. Ils peuvent osciller légèrement, ou l'outil peut se plier un tout petit peu. Pour tenir compte de cela, le système ne vérifie pas uniquement la taille exacte de l'outil. Il donne à l'outil un « manteau fluffy » (une marge de sécurité mathématique) autour de lui.

Si l'outil fait 5 mm de large, le système fait comme s'il faisait 7 mm de large pour plus de sécurité.
L'Inspecteur vérifie si cet « outil fluffy » heurte quelque chose. Si c'est le cas, le mouvement est interdit.

4. La « Course aux Données » (L'Alarme de Collision)

En informatique, une « course aux données » se produit lorsque deux programmes tentent d'utiliser la même mémoire en même temps. Les auteurs appellent une collision physique une « Course aux Données Spatiale ».

Lorsque l'Artiste écrit un mouvement qui provoquerait une collision :

L'Inspecteur examine la grille 3D en lisant le code.
Il voit les « Cubes Outil » chevauchant les « Cubes Équerres ».
La preuve mathématique échoue. L'Inspecteur crie : « STOP ! Vous essayez d'occuper le même espace ! »

5. La Boucle de Rétroaction (La Note « N'y Allez Pas »)

Par le passé, si une IA faisait une erreur, on pouvait simplement lui dire : « Réessayez », et espérer qu'elle ait de la chance. Cela est inefficace.

Ce système est plus intelligent. Lorsque l'Inspecteur détecte une collision, il ne dit pas simplement « Non ». Il identifie l'emplacement exact de la collision et dessine une petite boîte précise autour d'elle.

Le Message : « Vous avez essayé de vous déplacer vers les coordonnées X, Y, Z. Il y a une équerre à l'intérieur de cette boîte spécifique. N'entrez pas dans cette boîte. »
La Correction : Cette note est renvoyée à l'Artiste. L'Artiste lit la note, réalise l'erreur, et réécrit les instructions pour passer autour de la boîte.

6. Le Résultat : « Correct par Construction »

Ils continuent cette boucle — l'Artiste écrit, l'Inspecteur vérifie, l'Inspecteur signale la collision, l'Artiste la corrige — jusqu'à ce que l'Inspecteur puisse prouver mathématiquement que l'outil est très peu susceptible de heurter quoi que ce soit dans l'espace de travail actuel tel qu'il a été décrit au prouveur.

Parce que le système ne s'arrête que lorsque cette preuve est validée, l'ensemble final d'instructions est « Correct par Construction » pour cet espace de travail et cette description des obstacles. La garantie est que, selon le modèle spatial fourni à l'Inspecteur, le chemin de l'outil ne produit pas de collision physique. (Aucune preuve ne peut exclure les collisions causées par des changements dans l'espace de travail après la génération du code — déplacement des fixations, nouvelle matière brute, ou un opérateur laissant un outil dans la cellule — il s'agit donc d'une garantie conditionnelle à l'espace de travail, et non d'une garantie absolue.)

Résumé

Le papier décrit une méthode pour rendre sûres les instructions robotiques générées par une IA en associant une IA créative (GLLM) à un vérificateur de sécurité strict basé sur les mathématiques (SL Prover). Le vérificateur transforme le monde physique en une grille, lit le code G-code pour détecter les chevauchements (collisions), et renvoie des avertissements précis « interdiction d'entrer » à l'IA jusqu'à ce que les instructions soient mathématiquement vérifiées comme étant sans collision pour le modèle spatial actuel.

Résumé Technique : Génération de G-Code Correct par Construction via la Logique de Séparation

Énoncé du Problème

L'intégration des Modèles de Langage à Grande Échelle (LLM) dans l'usinage à Commande Numérique (CNC) offre la possibilité d'automatiser la synthèse d'instructions machines de bas niveau (G-code) à partir du langage naturel. Cependant, le déploiement direct de modèles génératifs dans des systèmes cyber-physiques introduit des défis critiques de sécurité. Bien que des LLM comme le cadre GLLM puissent générer du code syntaxiquement correct et sémantiquement aligné avec les géométries cibles, ils manquent de conscience spatiale inhérente et de garanties de sécurité déterministes.

Une limitation majeure réside dans l'« hallucination » de trajectoires d'outil qui supposent des espaces de travail infinis et exempts d'obstacles. Même des trajectoires d'outil logiquement saines peuvent entraîner des collisions physiques en raison de variables environnementales dynamiques (par exemple, des dispositifs de fixation mis à jour, des dimensions de matière première) et de réalités mécaniques (par exemple, le retard de service, le jeu de broche). Les mécanismes de sécurité traditionnels, tels que les simulations géométriques ou les tests de marge au pire cas, sont efficaces pour la visualisation mais manquent des preuves symboliques et mathématiques requises pour garantir la sécurité contre les mouvements physiques continus et les collisions de cas limites. Par conséquent, il existe un besoin d'un mécanisme de vérification indépendant et déterministe capable de garantir mathématiquement la disjonction spatiale avant l'exécution du code.

Méthodologie

L'article propose un cadre neuro-symbolique qui fait le pont entre la génération probabiliste par IA et la vérification formelle déterministe. L'architecture consiste en un pipeline itératif unidirectionnel impliquant deux agents principaux : un Générateur (GLLM) et un Vérificateur (Preuveur de Logique de Séparation).

Note d'attribution : Le formalisme du Tas Spatial et le Preuveur SL utilisés ici ont été introduits dans les travaux antérieurs des auteurs (Lee, arXiv:2605.10437). Le présent article intègre ce preuveur existant avec le GLLM dans un pipeline neuro-symbolique en boucle fermée.

1. L'Architecture Générateur-Vérificateur

Générateur (GLLM) : Utilise un LLM finement ajusté (par exemple, StarCoder-3B) amélioré par une Génération Augmentée par Récupération (RAG). Le système RAG injecte un contexte statique (limites cinématiques de la machine, topographie de l'espace de travail, géométrie de l'outil) et des marges de sécurité dynamiques dans l'invite. Cela contraint la génération initiale du LLM à être ancrée physiquement. Il est crucial de noter que le GLLM est un travail existant dont le rôle ici est inchangé : il assure la génération de G-code et la correction sémantique/syntaxique, mais il ne gère pas l'évitement des collisions, qui n'a jamais fait partie de son périmètre.
Vérificateur (Preuveur SL) : Un preuveur de Logique de Séparation (SL) spécifique au domaine qui traite l'espace de travail physique CNC comme un « Tas Spatial » discret. Ce modèle et le preuveur sont réutilisés directement depuis les travaux précédents de l'auteur. Dans ce modèle, l'occupation physique est gérée comme une ressource logique, où les coordonnées d'un réseau entier 3D discret ( $\mathbb{Z}^3$ ) mappent vers des états tels que Outil, Environnement, Matière Première ou Vide.

2. La Boucle Neuro-Symbolique

Le cadre fonctionne par un cycle itératif continu :

Initialisation & RAG : L'intention de l'utilisateur et les limites de l'espace de travail sont traitées. Le système RAG précalcule des limites environnementales étendues en utilisant une marge de sécurité ( $\epsilon$ ) et injecte ces contraintes dans le contexte du LLM.
Génération & Discrétisation (Le Parseur) : Le LLM synthétise une séquence de G-code provisoire. Un Parseur intermédiaire traduit ces commandes cinématiques continues (flottant $\mathbb{R}^3$ ) en logique spatiale discrète ( $\mathbb{Z}^3$ ). Ce processus applique des dilatations par somme de Minkowski à la géométrie de l'outil pour encapsuler les incertitudes physiques (par exemple, le retard de service), convertissant la trajectoire en un ensemble fini de demandes de ressources spatiales. La discrétisation produit un ensemble fini de demandes de ressources spatiales directement à partir du G-code ; le Preuveur SL vérifie ensuite la séparation par rapport à l'environnement sur ces revendications symboliques. Aucune simulation géométrique, aucun rendu de volume balayé et aucune restitution cinématique ne sont effectués à aucun stade.
Vérification Formelle : Le Preuveur SL évalue le chemin discrétisé en utilisant des Triples de Logique de Séparation $\{P\}C\{Q\}$ ${P} C {Q}$ . Il vérifie la Conjonction Séparatrice ( $*$ $*$ ), qui affirme que le volume balayé par l'outil est strictement disjoint des obstacles environnementaux.
- Succès : Si la conjonction tient, le mouvement est mathématiquement prouvé sûr.
- Échec (Course aux Données Spatiales) : Si le volume de l'outil intersecte l'environnement, la conjonction séparatrice échoue. Cette contradiction logique est identifiée comme une Course aux Données Spatiales, qui est la formalisation mathématique d'une collision physique. Le Preuveur SL ne vérifie pas les erreurs de code générales ; la correction sémantique et syntaxique relève du GLLM en amont.
Rétroaction & Affinement : En cas d'échec, le système ne rejette pas simplement le code. Au lieu de cela, il condense les voxels conflictuels en une boîte englobante minimale et alignée sur les axes ( $B_{conflict}$ ). Cet échec mathématique est traduit en un signal d'erreur structuré en langage naturel contenant les coordonnées spécifiques de la collision et une directive pour contourner le volume restreint.
Auto-correction : Le signal d'erreur est ajouté à la fenêtre de contexte du LLM, guidant le modèle pour affiner le segment spécifique de la trajectoire d'outil. La boucle se répète jusqu'à ce qu'une preuve formelle de disjonction spatiale soit obtenue.

Contributions Clés

L'article expose trois contributions principales au domaine de l'IA neuro-symbolique et de la fabrication :

Architecture Neuro-Symbolique Générateur-Vérificateur : Un cadre bipartite qui découple la cinématique physique continue de l'évaluation logique spatiale. Le LLM agit comme un générateur créatif, tandis que le Preuveur SL (un composant existant) agit comme un vérificateur inébranlable et déterministe, garantissant que la sortie est correcte par construction.
Traduction Symbole-Neurone via les Courses aux Données Spatiales : Un mécanisme formel pour communiquer les contradictions logiques au moteur neuronal. En redéfinissant les collisions physiques comme des violations de la conjonction séparatrice (appelées Courses aux Données Spatiales), le système traduit les intersections géométriques en directives structurées et lisibles par machine (boîtes englobantes) qui contraignent le processus génératif du LLM.
Auto-correction Déterministe et Automatisée : Contrairement aux approches empiriques reposant sur la validation humaine en boucle ou sur des métriques de similarité de trajectoire, ce cadre introduit une boucle de rétroaction entièrement automatisée. Le Preuveur SL fournit une rétroaction spatiale précise, sans faux positifs, permettant au LLM d'affiner autonomement les trajectoires jusqu'à l'établissement d'une preuve formelle de sécurité.

Résultats et Revendications

L'article établit la faisabilité théorique et la conception architecturale de cette approche neuro-symbolique. Il revendique que, en intégrant le cadre GLLM avec le modèle de Tas Spatial :

Le système traduit avec succès les collisions physiques en contradictions logiques (Courses aux Données Spatiales) pouvant être vérifiées formellement.
L'utilisation des sommes de Minkowski dans la phase de discrétisation permet au système de garantir mathématiquement des marges de sécurité contre les incertitudes mécaniques sans compliquer la logique discrète du preuveur.
Le mécanisme de rétroaction restreint efficacement l'espace de recherche probabiliste du LLM, empêchant les hallucinations répétées et guidant le modèle vers des trajectoires d'outil vérifiées mathématiquement et exemptes de collisions.

Les auteurs notent que, bien que l'architecture soit établie, une validation expérimentale complète (par exemple, des tests de référence contre des outils CAM traditionnels comme VERICUT sur des séquences industrielles à grande échelle) reste un effort en cours pour les travaux futurs. La garantie de sécurité formelle obtenue est conditionnelle à l'espace de travail tel qu'il est modélisé dans le Tas Spatial au moment de la génération du code.

Importance

L'importance de ce travail réside dans son passage de la sécurité empirique à la sécurité formelle dans la fabrication pilotée par l'IA. En conceptualisant l'espace de travail physique comme une ressource logique gérée, le cadre permet l'application de preuves mathématiques rigoureuses aux systèmes cyber-physiques. Cette approche comble le « fossé d'intention » critique entre les instructions humaines et l'exécution machine, offrant un chemin évolutif vers une fabrication CNC entièrement autonome et exempte de collisions. Elle démontre que l'IA générative peut être déployée en toute sécurité dans des environnements physiques à haut risque lorsqu'elle est couplée à une couche de vérification symbolique et déterministe qui traite la sécurité comme une nécessité logique plutôt que comme une probabilité statistique. Il est important de noter que la garantie de sécurité formelle s'applique à l'espace de travail tel que modélisé dans le Tas Spatial au moment de la génération du code, et ne s'étend pas aux changements environnementaux post-génération.

Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic