Immagina di dover insegnare a un artista molto creativo e immaginativo (un'intelligenza artificiale) come scolpire una statua da un blocco di marmo utilizzando un braccio robotico. L'artista è eccellente nel comprendere la tua descrizione ("Scolpisci un uccello") e può scrivere le istruzioni per il robot. Tuttavia, questo artista non ha mai visto effettivamente il laboratorio. Non sa dove si trovano le pesanti morse che tengono il marmo, né quanto sia grande il braccio del robot. Potrebbe scrivere istruzioni che sembrano perfette sulla carta, ma che causerebbero al robot di schiantarsi direttamente contro una morsa, rompendo la macchina.

Questo articolo propone una soluzione a tale problema unendo l'artista creativo a un ispettore di sicurezza rigoroso e matematicamente perfetto.

Ecco come funziona la loro partnership, suddivisa in passaggi semplici:

1. I Due Partner

L'Artista (l'IA): Si tratta di un Modello Linguistico di grandi dimensioni chiamato GLLM, portato da lavori precedenti. Il GLLM è eccellente nel prendere la tua richiesta in linguaggio naturale ("Scolpisci un uccello") e trasformarla in un elenco di istruzioni robotiche (G-code). Gestisce la generazione basata su contesto (RAG) e verifica che il codice sia sintatticamente e semanticamente ragionevole. Tuttavia, ciò che il GLLM non fa, e per cui non è mai stato progettato, è impedire al robot di schiantarsi fisicamente contro gli oggetti: non ha alcuna capacità di evitare collisioni integrata.
L'Ispettore (il Prover di Sicurezza): Si tratta di un prover basato sulla Logica di Separazione, portato dai lavori precedenti degli autori, in particolare dal paper Separation Logic for Verifying Physical Collisions of CNC Programs (arXiv:2605.10437), dove il modello "Spatial Heap" e il prover sono stati introdotti per la prima volta. Il compito unico dell'Ispettore è rilevare le collisioni fisiche — situazioni in cui l'utensile e un ostacolo cercherebbero di occupare lo stesso spazio nello stesso momento. Non è un revisore di codice generico; non verifica se il codice è "sbagliato" in senso ampio; è puramente un rilevatore di crash.

Ciò che questo articolo contribuisce effettivamente è il collegamento tra questi due strumenti esistenti — un ciclo di feedback neuro-simbolico in cui le rilevazioni di collisione dell'Ispettore vengono tradotte in una guida strutturata per l'Artista.

2. La "Sabbia Digitale" (L'Heap Spaziale)

Per far funzionare la matematica, il sistema trasforma il laboratorio fisico in una gigantesca griglia 3D di piccoli cubi (come una versione 3D di Minecraft).

Alcuni cubi sono contrassegnati come "Marmo" (il materiale da tagliare).
Alcuni sono contrassegnati come "Morse" (ostacoli).
Alcuni sono contrassegnati come "Aria Vuota" (spazio sicuro).
Anche l'utensile del robot è una forma specifica di cubi.

L'Ispettore non osserva il movimento del robot come un gioco di "musica delle sedie". Importante: l'Ispettore non guarda mai il robot muoversi e non esegue mai una simulazione geometrica. Legge direttamente lo script del G-code, riga per riga, e calcola quali cubi ogni movimento dell'utensile richiederebbe di occupare. La regola che applica è semplice: i cubi rivendicati dall'utensile non devono essere già rivendicati da una morsa o da qualsiasi altro ostacolo.

3. Il Buffer di Sicurezza (Il "Cappotto Fluffy")

I robot non sono perfetti. Potrebbero oscillare leggermente, o l'utensile potrebbe piegarsi di un minimo. Per tenerne conto, il sistema non controlla solo la dimensione esatta dell'utensile. Gli conferisce un "cappotto fluffy" (un margine di sicurezza matematico) intorno ad esso.

Se l'utensile è largo 5 mm, il sistema finge che sia largo 7 mm per essere sicuro.
L'Ispettore verifica se questo "utensile fluffy" colpisce qualcosa. Se lo fa, la mossa è vietata.

4. La "Corsa ai Dati" (L'Allarme di Incidente)

Nell'informatica, una "corsa ai dati" (data race) si verifica quando due programmi tentano di utilizzare la stessa memoria contemporaneamente. Gli autori definiscono un incidente fisico una "Corsa Spaziale ai Dati".

Quando l'Artista scrive una mossa che causerebbe un incidente:

L'Ispettore legge il codice e analizza la griglia 3D.
Vede i "Cubi Utensile" sovrapposti ai "Cubi Morsa".
La prova matematica fallisce. L'Ispettore urla: "STOP! Stai cercando di occupare lo stesso spazio!"

5. Il Ciclo di Feedback (La Nota "Non Andare Là")

In passato, se un'IA commetteva un errore, si poteva semplicemente dirle: "Riprova", sperando che avesse fortuna. Questo è inefficiente.

Questo sistema è più intelligente. Quando l'Ispettore rileva un incidente, non dice solo "No". Individua la posizione esatta dell'incidente e disegna intorno ad essa una piccola scatola precisa.

Il Messaggio: "Hai cercato di spostarti alle coordinate X, Y, Z. All'interno di questa specifica scatola c'è una morsa. Non entrare in questa scatola."
La Correzione: Questa nota viene inviata all'Artista. L'Artista legge la nota, realizza l'errore e riscrive le istruzioni per andare intorno alla scatola.

6. Il Risultato: "Corretto per Costruzione"

Continuano a eseguire questo ciclo: l'Artista scrive, l'Ispettore controlla, l'Ispettore segnala l'incidente, l'Artista lo corregge, finché l'Ispettore non può dimostrare matematicamente che l'utensile non colpirà quasi certamente nulla nel workspace corrente così come descritto al prover.

Poiché il sistema si ferma solo quando la prova matematica va a buon fine, l'insieme finale di istruzioni è "Corretto per Costruzione" per quel workspace e quella descrizione degli ostacoli. La garanzia è che, secondo il modello spaziale fornito all'Ispettore, il percorso dell'utensile non produce collisioni fisiche. (Nessuna prova può escludere collisioni causate da cambiamenti nel workspace dopo la generazione del codice — come fissaggi spostati, nuove materie prime o un operatore che lascia uno strumento all'interno della cella — quindi questa è una garanzia condizionata al workspace, non incondizionata).

Riassunto

L'articolo descrive un modo per rendere sicure le istruzioni robotiche generate dall'IA accoppiando un'IA creativa a un rigoroso controllore di sicurezza basato sulla matematica. Il controllore legge direttamente il codice G-code, trasforma il mondo fisico in una griglia, verifica le sovrapposizioni (incidenti) e invia all'IA avvisi precisi "non entrare" fino a quando le istruzioni non sono matematicamente verificate come prive di collisioni per il workspace così come è stato descritto al prover.

Riepilogo Tecnico: Generazione di Codice G Corretta per Costruzione tramite Logica di Separazione

Enunciato del Problema

L'integrazione di Modelli Linguistici di Grande Dimensione (LLM) nella lavorazione a Controllo Numerico Computerizzato (CNC) offre il potenziale per automatizzare la sintesi di istruzioni macchina a basso livello (codice G) a partire dal linguaggio naturale. Tuttavia, il dispiegamento diretto di modelli generativi in sistemi cyber-fisici introduce sfide critiche di sicurezza. Sebbene gli LLM, come il framework GLLM, possano generare codice sintatticamente corretto che si allinea semanticamente con le geometrie target, mancano di consapevolezza spaziale intrinseca e di garanzie di sicurezza deterministiche.

Un limite primario è l'"allucinazione" di percorsi utensile che presuppongono spazi di lavoro infiniti e privi di ostacoli. Anche percorsi utensile logicamente validi possono risultare in collisioni fisiche a causa di variabili ambientali dinamiche (ad esempio, fissaggi aggiornati, dimensioni del grezzo) e realtà meccaniche (ad esempio, ritardo del servomotore, gioco dell'asse). I meccanismi di sicurezza tradizionali, come le simulazioni geometriche o i test di margine nel caso peggiore, sono efficaci per la visualizzazione ma mancano delle prove simboliche e matematiche necessarie per garantire la sicurezza contro movimenti fisici continui e collisioni in casi limite. Di conseguenza, vi è la necessità di un meccanismo di verifica indipendente e deterministico in grado di garantire matematicamente la disgiunzione spaziale prima dell'esecuzione del codice.

Metodologia

Il documento propone un framework neuro-simbolico che colma il divario tra la generazione probabilistica dell'IA e la verifica formale deterministica. L'architettura consiste in una pipeline unidirezionale e iterativa che coinvolge due agenti principali: un Generatore (LLM) e un Verificatore (Prover di Logica di Separazione).

Nota: Il formalismo dell'Heap Spaziale e il prover SL utilizzati qui sono stati introdotti nel lavoro precedente degli autori (Lee, arXiv:2605.10437). Il presente lavoro integra tale prover esistente con il GLLM in una pipeline neuro-simbolica a ciclo chiuso.

1. L'Architettura Generatore-Verificatore

Generatore (GLLM): Utilizza un LLM fine-tuned (ad esempio, StarCoder-3B) potenziato con la Generazione Aumentata dal Recupero (RAG). Il sistema RAG inietta contesto statico (limiti cinematici della macchina, topografia dello spazio di lavoro, geometria dell'utensile) e margini di sicurezza dinamici nel prompt. Ciò vincola la generazione iniziale dell'LLM a essere fondata fisicamente. È fondamentale notare che il GLLM è un framework esistente il cui ruolo qui rimane invariato: generazione di G-code con RAG e correttezza semantica/sintattica. La evitamento delle collisioni non è mai stata parte dello scopo del GLLM.
Verificatore (Prover SL): Un prover di Logica di Separazione (SL) specifico per il dominio, introdotto nel lavoro precedente dell'autore, che tratta lo spazio di lavoro fisico CNC come un "Heap Spaziale" discreto. In questo modello, l'occupazione fisica è gestita come una risorsa logica, dove le coordinate in un reticolo intero 3D discreto ( $\mathbb{Z}^3$ ) mappano stati come Tool (Utensile), Environment (Ambiente), Stock (Grezzo) o Empty (Vuoto). Il presente documento riutilizza questo prover senza ridefinirlo.

Il contributo di questo lavoro risiede nell'integrazione neuro-simbolica iterativa tra questi due componenti esistenti: un ciclo di feedback che traduce le rilevazioni di collisioni (Spatial Data Races) del Verificatore in direttive strutturate e le reinvia nel contesto del Generatore.

2. Il Ciclo Neuro-Simbolico

Il framework opera attraverso un ciclo iterativo continuo:

Inizializzazione & RAG: L'intento dell'utente e i limiti dello spazio di lavoro vengono elaborati. Il sistema RAG pre-calcola i limiti ambientali espansi utilizzando un margine di sicurezza ( $\epsilon$ ) e inietta questi vincoli nel contesto dell'LLM.
Generazione e Discretizzazione (Il Parser): L'LLM sintetizza una sequenza di codice G bozza. Un Parser intermedio traduce questi comandi cinematici continui (punti floating-point $\mathbb{R}^3$ ) in logica spaziale discreta ( $\mathbb{Z}^3$ ). Questo processo applica dilatazioni tramite somma di Minkowski alla geometria dell'utensile per racchiudere le incertezze fisiche (ad esempio, ritardo del servomotore), convertendo la traiettoria in un insieme finito di richieste di risorse spaziali. La discretizzazione produce un insieme finito di richieste di risorse spaziali direttamente dal codice G; il Prover SL verifica quindi la separazione rispetto all'ambiente su queste affermazioni simboliche. Non viene eseguita alcuna simulazione geometrica, rendering di volumi spazzati o riproduzione cinematica in nessuna fase.
Verifica Formale: Il Prover SL valuta il percorso discretizzato utilizzando le Triple di Logica di Separazione $\{P\}C\{Q\}$ ${P} C {Q}$ . Verifica la Congiunzione Separante ( $*$ $*$ ), che afferma che il volume spazzato dall'utensile è strettamente disgiunto dagli ostacoli ambientali.
- Successo: Se la congiunzione vale, il movimento è matematicamente provato sicuro.
- Fallimento (Corsa ai Dati Spaziale): Se il volume dell'utensile interseca l'ambiente, la congiunzione separante fallisce. Questa contraddizione logica è identificata specificamente come una Corsa ai Dati Spaziale (Spatial Data Race), che rappresenta la formalizzazione matematica di una collisione fisica. Il Prover SL non verifica errori generici di codice; la correttezza semantica e sintattica è responsabilità del GLLM a monte.
Feedback e Raffinamento: In caso di fallimento, il sistema non rifiuta semplicemente il codice. Invece, condensa i voxel conflittuali in un bounding box (scatola delimitante) minimale e allineato agli assi ( $B_{conflict}$ ). Questo fallimento matematico viene tradotto in un segnale di errore strutturato in linguaggio naturale contenente le coordinate specifiche della collisione e una direttiva per aggirare il volume limitato.
Auto-correzione: Il segnale di errore viene aggiunto alla finestra del contesto dell'LLM, guidando il modello a rifinire il segmento specifico del percorso utensile. Il ciclo si ripete fino al raggiungimento di una prova formale di disgiunzione spaziale.

Contributi Chiave

Il documento delinea tre contributi primari al campo dell'IA neuro-simbolica e della manifattura:

Architettura Neuro-Simbolica Generatore-Verificatore: Un framework bipartito che disaccoppia la cinematica fisica continua dalla valutazione logica spaziale. L'LLM agisce come un generatore creativo (con responsabilità per la correttezza sintattica), mentre il Prover SL (riutilizzato da lavoro precedente) agisce come un verificatore deterministico inesorabile, garantendo che l'output sia corretto per costruzione rispetto alle collisioni fisiche.
Traduzione Simbolico-Neurale tramite Corse ai Dati Spaziali: Un meccanismo formale per comunicare contraddizioni logiche al motore neurale. Ridefinendo le collisioni fisiche come violazioni della congiunzione separante (nello specifico, Corse ai Dati Spaziali), il sistema traduce le intersezioni geometriche in direttive strutturate e leggibili dalla macchina (bounding box) che vincolano il processo generativo dell'LLM. Il termine "Corsa ai Dati Spaziali" è qui il nome formale specifico per una collisione fisica in questo framework.
Auto-correzione Automatica e Deterministica: A differenza degli approcci empirici che si basano sulla validazione umana nel ciclo o su metriche di similarità dei percorsi, questo framework introduce un ciclo di feedback completamente automatizzato. Il Prover SL fornisce un feedback spaziale preciso, a zero falsi positivi, permettendo all'LLM di rifinire autonomamente le traiettorie fino all'instaurazione di una prova formale di sicurezza.

Risultati e Affermazioni

Il documento stabilisce la fattibilità teorica e il design architetturale di questo approccio neuro-simbolico di integrazione. Afferma che, integrando il framework GLLM con il modello dell'Heap Spaziale esistente:

Il sistema traduce con successo le collisioni fisiche in contraddizioni logiche (Corse ai Dati Spaziali) che possono essere verificate formalmente.
L'uso delle somme di Minkowski nella fase di discretizzazione permette al sistema di garantire matematicamente i margini di sicurezza contro le incertezze meccaniche senza complicare la logica discreta del prover.
Il meccanismo di feedback limita efficacemente lo spazio di ricerca probabilistico dell'LLM, prevenendo allucinazioni ripetute e guidando il modello verso percorsi utensile privi di collisioni e verificati matematicamente.

Gli autori notano che, sebbene l'architettura sia stabilita, la validazione sperimentale completa (ad esempio, il confronto con strumenti CAM tradizionali come VERICUT su sequenze industriali su larga scala) rimane uno sforzo in corso per lavori futuri. La garanzia di sicurezza ottenuta è condizionata allo spazio di lavoro: la prova formale di disgiunzione spaziale vale all'interno del modello spaziale fornito al prover al momento della generazione del codice.

Significato

Il significato di questo lavoro risiede nel suo passaggio dalla sicurezza empirica alla sicurezza formale nella manifattura guidata dall'IA. Concettualizzando lo spazio di lavoro fisico come una risorsa logica gestita, il framework permette l'applicazione di rigorose prove matematiche ai sistemi cyber-fisici. Questo approccio affronta il critico "divario di intento" tra istruzioni umane ed esecuzione macchina, offrendo un percorso scalabile verso una manifattura CNC completamente autonoma e priva di collisioni. Dimostra che l'IA generativa può essere dispiegata in sicurezza in ambienti fisici ad alto rischio quando è accoppiata a un livello di verifica simbolica deterministico che tratta la sicurezza come una necessità logica piuttosto che come una probabilità statistica. È importante notare che la garanzia di sicurezza formale si applica allo spazio di lavoro così come modellato nell'Heap Spaziale al momento della generazione del codice e non si estende a cambiamenti ambientali successivi alla generazione.

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