Stel je voor dat je probeert een zeer creatieve, fantasierijke kunstenaar (een AI) te leren hoe je een standbeeld uit een marmeren blok moet hakken met behulp van een robotarm. De kunstenaar is uitstekend in het begrijpen van je beschrijving ("Maak een vogel") en kan de instructies voor de robot opschrijven. Deze kunstenaar heeft echter de werkplaats nooit echt gezien. Ze weten niet waar de zware klemmen zitten die het marmer vasthouden, of hoe groot de arm van de robot is. Ze kunnen instructies schrijven die op papier perfect lijken, maar die ertoe leiden dat de robot direct tegen een klem botst, waardoor de machine kapotgaat.

Dit artikel stelt een oplossing voor dit probleem voor door de creatieve kunstenaar te koppelen aan een streng, wiskundig perfect veiligheidsinspecteur.

Hier is hoe hun partnerschap werkt, opgesplitst in eenvoudige stappen:

1. De Twee Partners

De Kunstenaar (De AI): Dit is een Large Language Model genaamd GLLM, overgenomen uit eerdere werken. De GLLM is uitstekend in het omzetten van je natuurlijke taalverzoek ("Hak een vogel") in een lijst met robotinstructies (G-code). Het zorgt voor Retrieval-Augmented Generation (het ophalen van context over de machine en de taak) en controleert of de code syntactisch en semantisch logisch is. Wat het niet doet, en waarvoor het nooit ontworpen is, is voorkomen dat de robot fysiek tegen dingen aanrijdt; het heeft geen ingebouwde botsingsvermijding.
De Inspecteur (De Veiligheidsbewijzer): Dit is een Separation Logic-bewijzer die de auteurs hebben overgenomen uit hun eigen eerdere werk — specifiek het artikel Separation Logic for Verifying Physical Collisions of CNC Programs (arXiv:2605.10437), waar het ruimtelijke heap-model en de bewijzer voor het eerst werden geïntroduceerd. De enige taak van de Inspecteur is het detecteren van fysieke botsingen — situaties waarin het gereedschap en een obstakel zouden proberen dezelfde ruimte tegelijkertijd in te nemen. Het is geen algemene code-reviewer; het controleert niet of de code op een bredere manier "fout" is; het is puur een crash-detecteur.

Wat dit artikel daadwerkelijk bijdraagt, is de bedrading tussen deze twee bestaande tools: een neuro-symbolische feedbacklus waarin de botsingsbevindingen van de Inspecteur worden vertaald naar gestructureerde begeleiding voor de Kunstenaar.

2. De "Digitale Zandbak" (De Ruimtelijke Heap)

Om de wiskunde te laten werken, zet het systeem de fysieke werkplaats om in een gigantisch 3D-rooster van kleine kubussen (zoals een 3D-versie van Minecraft).

Sommige kubussen zijn gemarkeerd als "Marmer" (het materiaal dat moet worden gesneden).
Sommige zijn gemarkeerd als "Klemmen" (obstakels).
Sommige zijn gemarkeerd als "Lege Lucht" (veilige ruimte).
Het gereedschap van de robot is ook een specifieke vorm van kubussen.

De Inspecteur behandelt de beweging van de robot als een spelletje "stoelenwippen" met deze kubussen. Belangrijk: De Inspecteur kijkt de robot nooit toe en voert geen geometrische simulatie uit. Het leest de G-code-script direct, regel voor regel, en werkt uit welke kubussen elke gereedschapsbeweging zou moeten bezetten. De regel die het afdwingt is simpel: de kubussen die door het gereedschap worden geclaimd, mogen niet al geclaimd zijn door een klem of een ander obstakel.

3. De Veiligheidsbuffer (De "Pluizige Mantel")

Roboten zijn niet perfect. Ze kunnen lichtjes trillen, of het gereedschap kan een klein beetje buigen. Om dit te compenseren, controleert het systeem niet alleen de exacte grootte van het gereedschap. Het geeft het gereedschap een "pluizige mantel" (een wiskundige veiligheidsmarge) eromheen.

Als het gereedschap 5 mm breed is, doet het systeem alsof het 7 mm breed is voor de zekerheid.
De Inspecteur controleert of deze "pluizige tool" ergens tegenaan botst. Als dat zo is, is de beweging verboden.

4. De "Data Race" (De Crash-alarm)

In de informatica treedt een "data race" op wanneer twee programma's tegelijkertijd hetzelfde geheugen proberen te gebruiken. De auteurs noemen een fysieke crash een "Ruimtelijke Data Race".

Wanneer de Kunstenaar een beweging schrijft die tot een crash zou leiden:

Kijkt de Inspecteur naar het 3D-rooster (gebaseerd op de G-code).
Ziet hij de "Tool Cubes" overlappen met de "Clamp Cubes".
Faalt het wiskundige bewijs. De Inspecteur schreeuwt: "STOP! Je probeert dezelfde ruimte in te nemen!"

5. De Feedbacklus (De "Ga daar niet heen"-Notitie)

In het verleden, als een AI een fout maakte, kon je het misschien gewoon zeggen: "Probeer het opnieuw", en hopen dat het geluk had. Dat is inefficiënt.

Dit systeem is slimmer. Wanneer de Inspecteur een crash vindt, zegt hij niet alleen "Nee". Hij pinpoint de exacte locatie van de crash en tekent een kleine, precieze doos eromheen.

De Boodschap: "Je probeerde naar coördinaten X, Y, Z te bewegen. Er zit een klem in deze specifieke doos. Ga niet in deze doos."
De Correctie: Deze notitie wordt teruggestuurd naar de Kunstenaar. De Kunstenaar leest de notitie, beseft de fout en herschrijft de instructies om om de doos heen te gaan.

6. Het Resultaat: "Correct-by-Construction"

Ze blijven deze lus uitvoeren – Kunstenaar schrijft, Inspecteur controleert, Inspecteur wijst de crash aan, Kunstenaar repareert het – totdat de Inspecteur wiskundig kan bewijzen dat het gereedschap zeer waarschijnlijk niet zal botsen met iets in de huidige werkruimte zoals die aan de bewijzer is beschreven.

Omdat het systeem pas stopt wanneer dit bewijs lukt, is de uiteindelijke set instructies "Correct-by-Construction" voor die werkruimte en die beschrijving van de obstakels. De garantie is dat, onder het ruimtelijke model dat de Inspecteur kreeg, het gereedschapspad geen fysieke botsing veroorzaakt. (Geen enkel bewijs kan botsingen uitsluiten die worden veroorzaakt door wijzigingen in de werkruimte na het genereren van de code — verplaatste bevestigingen, nieuwe voorraad, of een operator die een gereedschap in de cel laat — dus dit is een werkruimte-voorwaardelijke garantie, geen onvoorwaardelijke.)

Samenvatting

Het artikel beschrijft een manier om door AI gegenereerde robotinstructies veilig te maken door een creatieve AI te koppelen aan een strenge, op wiskunde gebaseerde veiligheidscontroleur. De controleur zet de fysieke wereld om in een rooster, controleert op overlappingen (crashes) en stuurt precieze "binnen niet toegestaan"-waarschuwingen terug naar de AI totdat de instructies wiskundig zijn geverifieerd tegen het huidige ruimtelijke model.

Technische Samenvatting: Correct-by-Construction G-Code Generatie via Scheidingslogica

Probleemstelling

De integratie van Large Language Models (LLM's) in Computer Numerical Control (CNC) bewerkingsmachines biedt het potentieel om de synthese van laag-niveau machine-instructies (G-code) vanuit natuurlijke taal te automatiseren. Het direct inzetten van generatieve modellen in cyber-fysieke systemen introduceert echter kritieke veiligheidsuitdagingen. Hoewel LLM's zoals het GLLM-framework syntactisch correcte code kunnen genereren die semantisch overeenkomt met de doelgeometrieën, missen ze inherent ruimtelijk bewustzijn en deterministische veiligheidsgaranties.

Een primaire beperking is de "hallucinatie" van gereedschapspaden die uitgaan van oneindige, obstakelvrije werkruimten. Zelfs logisch onderbouwde gereedschapspaden kunnen leiden tot fysieke botsingen door dynamische omgevingsvariabelen (bijvoorbeeld bijgewerkte klemmen, afmetingen van het grondstof) en mechanische realiteiten (bijvoorbeeld servo-traging, spindeluitloop). Traditionele veiligheidsmechanismen, zoals geometrische simulaties of testen met worst-case marges, zijn effectief voor visualisatie maar missen de symbolische, wiskundige bewijzen die nodig zijn om veiligheid te garanderen tegen continue fysieke bewegingen en botsingen in uitzonderlijke gevallen. Bijgevolg is er behoefte aan een onafhankelijk, deterministisch verificatiemechanisme dat wiskundig ruimtelijke disjunctie kan garanderen voordat de code wordt uitgevoerd.

Methodologie

Het artikel stelt een neuro-symbolisch framework voor dat probabilistische AI-generatie koppelt aan deterministische formele verificatie. De architectuur bestaat uit een unidirectionele, iteratieve pijplijn met twee primaire agenten: een Generator (GLLM) en een Verifier (Scheidingslogica Bewijzer).

Attributie: De Spatial Heap-formalisme en de SL-bewijzer die hier worden gebruikt, zijn eerder geïntroduceerd in het werk van de auteurs ("Separation Logic for Verifying Physical Collisions of CNC Programs", arXiv:2605.10437). Het huidige artikel integreert die bestaande bewijzer met de GLLM in een gesloten neuro-symbolische lus.

1. De Generator-Verifier Architectuur

Generator (GLLM): Dit is een eerder gepubliceerd LLM-framework (bijvoorbeeld StarCoder-3B) dat is versterkt met Retrieval-Augmented Generation (RAG). Het RAG-systeem injecteert statische context (kinematische limieten van de machine, topografie van de werkruimte, gereedschapsgeometrie) en dynamische veiligheidsmarges in de prompt. Het GLLM is verantwoordelijk voor de generatie van G-code met semantische en syntactische correctheid; expliciet valt botsingsvermijding buiten de oorspronkelijke scope van het GLLM-framework.
Verifier (SL Bewijzer): Dit is de bestaande, domeinspecifieke Scheidingslogica (SL) bewijzer uit het eerder genoemde werk. Deze behandelt de fysieke CNC-werkruimte als een discrete "Spatial Heap". In dit model wordt fysieke bezetting beheerd als een logische resource, waarbij coördinaten in een discrete 3D-integer rooster ( $\mathbb{Z}^3$ ) corresponderen met toestanden zoals Tool, Environment, Stock of Empty.

2. De Neuro-Symbolische Lus

Het framework werkt via een continue iteratieve cyclus:

Initialisatie & RAG: De gebruikersintentie en de grenzen van de werkruimte worden verwerkt. Het RAG-systeem berekent vooraf uitgebreide omgevingsgrenzen met behulp van een veiligheidsmarge ( $\epsilon$ ) en injecteert deze beperkingen in de context van de LLM.
Generatie & Discretisatie (De Parser): De LLM synthetiseert een concept G-code-sequentie. Een tussenliggende Parser vertaalt deze continue kinematische commando's (floating-point $\mathbb{R}^3$ ) naar discrete ruimtelijke logica ( $\mathbb{Z}^3$ ). Dit proces past Minkowski-sum dilaties toe op de gereedschapsgeometrie om fysieke onzekerheden (bijvoorbeeld servo-traging) te omvatten, waardoor de trajecten worden omgezet in een eindige set van ruimtelijke resource-aanvragen. De discretisatie produceert een eindige set van ruimtelijke resource-aanvragen direct vanuit de G-code; de SL-bewijzer verifieert vervolgens de scheiding tegen de omgeving op deze symbolische claims. Er wordt op geen enkel stadium geometrische simulatie, swept-volume rendering of kinematische playback uitgevoerd.
Formele Verificatie: De SL Bewijzer evalueert het gediscretiseerde pad met behulp van Scheidingslogica Triples $\{P\}C\{Q\}$ ${P} C {Q}$ . Het controleert op de Scheidende Conjunctie ( $*$ $*$ ), die stelt dat het door het gereedschap verzwomene volume strikt disjunct is van omgevingsobstakels.
- Succes: Als de conjunctie geldt, is de beweging wiskundig bewezen veilig.
- Falen (Ruimtelijke Data Race): Als het gereedschapsvolume intersecteert met de omgeving, faalt de scheidende conjunctie. Deze logische tegenstrijdigheid wordt geïdentificeerd als een Ruimtelijke Data Race, wat de wiskundige formalisatie is van een fysieke botsing binnen dit framework. De SL-bewijzer controleert specifiek op deze fysieke botsingen en niet op algemene logische codefouten.
Feedback & Verfijning: Bij falen verwierpt het systeem de code niet simpelweg. In plaats daarvan worden de conflicterende voxels samengevoegd tot een minimaal, as-georiënteerd omhullend vlak ( $B_{conflict}$ ). Dit wiskundige falen wordt vertaald naar een gestructureerd, natuurlijk taalgestuurd foutsignaal dat de specifieke coördinaten van de botsing bevat en een instructie om het beperkte volume te omzeilen.
Zelfcorrectie: Het foutsignaal wordt toegevoegd aan het contextvenster van de LLM, waardoor het model wordt geleid om het specifieke segment van het gereedschapspad te verfijnen. De lus herhaalt zich totdat een formeel bewijs van ruimtelijke disjunctie is bereikt.

Belangrijkste Bijdragen

Het artikel schetst drie primaire bijdragen aan het veld van neuro-symbolische AI en productie:

Neuro-Symbolische Integratie van Bestaande Componenten: De kernbijdrage van dit werk is de iteratieve integratie van het bestaande GLLM-framework met de bestaande SL-bewijzer. Hiermee wordt een gesloten lus gecreëerd waarin de Verifier botsingsbevindingen terugkoppelt naar de Generator, waardoor de output correct-by-construction wordt, zonder dat de onderliggende componenten zelf worden herdefinieerd.
Symbolisch-naar-Neurale Vertaling via Ruimtelijke Data Races: Een formeel mechanisme om logische tegenstrijdigheden aan de neurale engine te communiceren. Door fysieke botsingen te herdefiniëren als schendingen van de scheidende conjunctie (Ruimtelijke Data Races), vertaalt het systeem geometrische intersecties naar gestructureerde, machineleesbare instructies (omhullende vlakken) die het generatieve proces van de LLM beperken. De term "Ruimtelijke Data Race" verwijst hier specifiek naar een fysieke botsing, niet naar een generieke logische fout.
Deterministische, Geautomatiseerde Zelfcorrectie: In tegenstelling tot empirische benaderingen die vertrouwen op menselijke validatie in de lus of pad-相似heidsmetrieken, introduceert dit framework een volledig geautomatiseerde feedbacklus. De SL Bewijzer biedt nauwkeurige, nul-valse-positieve ruimtelijke feedback, waardoor de LLM autonoom trajecten kan verfijnen totdat een formeel veiligheidsbewijs is vastgesteld.

Resultaten en Beweringen

Het artikel vestigt de theoretische haalbaarheid en het architecturale ontwerp van deze neuro-symbolische aanpak. Het beweert dat door het GLLM-framework te integreren met het Spatial Heap-model:

Het systeem fysieke botsingen succesvol vertaalt naar logische tegenstrijdigheden die formeel kunnen worden geverifieerd.
Het gebruik van Minkowski-sums in de discretisatiefase het systeem in staat stelt om wiskundig veiligheidsmarges te garanderen tegen mechanische onzekerheden zonder de discrete logica van de bewijzer te compliceren.
Het feedbackmechanisme effectief de probabilistische zoekruimte van de LLM beperkt, herhaalde hallucinaties voorkomt en het model leidt naar wiskundig geverifieerde, botsingsvrije gereedschapspaden.

De auteurs merken op dat hoewel de architectuur is vastgesteld, omvattende experimentele validatie (bijvoorbeeld benchmarking tegen traditionele CAM-tools zoals VERICUT op grote industriële sequenties) een lopende inspanning blijft voor toekomstig werk. Het formele bewijs van ruimtelijke disjunctie geldt voorwaardelijk binnen de ruimtelijke modellen die aan de bewijzer zijn gegeven op het moment van codegeneratie.

Betekenis

De betekenis van dit werk ligt in de verschuiving van empirische veiligheid naar formele veiligheid in door AI aangedreven productie. Door de fysieke werkruimte te conceptualiseren als een beheerde logische resource, stelt het framework de toepassing van rigoureuze wiskundige bewijzen voor cyber-fysieke systemen mogelijk. Deze aanpak adresseert de kritieke "intent gap" tussen menselijke instructies en machine-uitvoering, en biedt een schaalbaar pad naar volledig autonome, botsingsvrije CNC-productie. Het demonstreert dat generatieve AI veilig kan worden ingezet in hoog-risico fysieke omgevingen wanneer deze wordt gekoppeld aan een deterministische, symbolische verificatielaag die veiligheid behandelt als een logische noodzaak in plaats van een statistische waarschijnlijkheid. Het is belangrijk op te merken dat deze formele veiligheidsgarantie specifiek van toepassing is op de werkruimte zoals gemodelleerd in de Spatial Heap op het moment van generatie, en niet uitbreidt tot post-generatie veranderingen in de fysieke omgeving.

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