Stellen Sie sich vor, Sie versuchen, einem sehr kreativen, fantasievollen Künstler (einer KI) beizubringen, wie man mit einem Roboterarm eine Statue aus einem Marmorblock meißelt. Der Künstler versteht Ihre Beschreibung („Vogel formen") hervorragend und kann die Anweisungen für den Roboter aufschreiben. Dieser Künstler hat jedoch den Werkstattbereich noch nie wirklich gesehen. Er weiß nicht, wo die schweren Klemmen liegen, die den Marmor halten, oder wie groß der Arm des Roboters ist. Er könnte Anweisungen verfassen, die auf dem Papier perfekt aussehen, aber dazu führen würden, dass der Roboter direkt gegen eine Klemme kracht und die Maschine zerstört.

Dieser Artikel schlägt eine Lösung für dieses Problem vor, indem er den kreativen Künstler mit einem strengen, mathematisch perfekten Sicherheitsinspektor zusammenbringt.

So funktioniert ihre Partnerschaft, aufgeschlüsselt in einfache Schritte:

1. Die zwei Partner

Der Künstler (Die KI): Dies ist ein Large Language Model namens GLLM, das aus früheren Arbeiten übernommen wurde. Der GLLM ist hervorragend darin, Ihre Anfrage in natürlicher Sprache („Vogel meißeln") in eine Liste robotischer Anweisungen (G-Code) umzuwandeln. Er übernimmt das Retrieval-Augmented Generation (das Einbeziehen von Kontext über die Maschine und die Aufgabe) und prüft, ob der Code syntaktisch und semantisch sinnvoll ist. Was er jedoch nicht tut und wofür er nie entwickelt wurde, ist die Verhinderung physischer Zusammenstöße – er hat keine eingebaute Kollisionsvermeidung.
Der Inspektor (Die Logik-Engine): Dies ist ein Separation-Logic-Beweiser, den die Autoren aus ihrer eigenen früheren Arbeit übernommen haben – speziell aus dem Papier „Separation Logic for Verifying Physical Collisions of CNC Programs" (arXiv:2605.10437), in dem das räumliche Heap-Modell und der Beweiser erstmals vorgestellt wurden. Die einzige Aufgabe des Inspektors ist es, physische Kollisionen zu erkennen – Situationen, in denen Werkzeug und Hindernis versuchen würden, denselben Raum gleichzeitig einzunehmen. Er ist kein allgemeiner Code-Reviewer; er prüft nicht, ob der Code im weiteren Sinne „falsch" ist, sondern ist rein ein Crash-Detektor.

Was dieser Artikel tatsächlich beiträgt, ist die Verkabelung zwischen diesen beiden bestehenden Werkzeugen – eine neuro-symbolische Feedback-Schleife, in der die Kollisionsergebnisse des Inspektors in strukturierte Anweisungen für den Künstler zurückübersetzt werden.

2. Der „digitale Sandkasten" (Der räumliche Heap)

Damit die Mathematik funktioniert, verwandelt das System die physische Werkstatt in ein riesiges 3D-Raster aus winzigen Würfeln (wie eine 3D-Version von Minecraft).

Einige Würfel sind als „Marmor" markiert (das zu schneidende Material).
Einige sind als „Klemmen" markiert (Hindernisse).
Einige sind als „leere Luft" markiert (sicherer Raum).
Das Werkzeug des Roboters besteht ebenfalls aus einer spezifischen Form von Würfeln.

Der Inspektor behandelt die Bewegung des Roboters wie ein Spiel „Musikstühle" mit diesen Würfeln. Die Regel ist einfach: Die Würfel des Werkzeugs dürfen niemals die Würfel der Klemmen berühren.

Wichtig ist: Der Inspektor beobachtet den Roboter nicht in Bewegung und führt keine geometrische Simulation durch. Er liest den G-Code-Skript direkt Zeile für Zeile und berechnet, welche Würfel jeder Werkzeugbewegung beanspruchen würde. Die Regel, die er durchsetzt, ist einfach: Die vom Werkzeug beanspruchten Würfel dürfen nicht bereits von einer Klemme oder einem anderen Hindernis beansprucht sein.

3. Der Sicherheitspuffer (Der „flauschige Mantel")

Roboter sind nicht perfekt. Sie könnten leicht wackeln, oder das Werkzeug könnte sich minimal verbiegen. Um dies zu berücksichtigen, prüft das System nicht nur die exakte Größe des Werkzeugs. Es gibt dem Werkzeug einen „flauschigen Mantel" (einen mathematischen Sicherheitsabstand) darum herum.

Wenn das Werkzeug 5 mm breit ist, tut das System so, als wäre es aus Sicherheitsgründen 7 mm breit.
Der Inspektor prüft, ob dieser „flauschige Werkzeug" etwas trifft. Wenn ja, ist die Bewegung verboten.

4. Der „Data Race" (Der Crash-Alarm)

In der Informatik tritt ein „Data Race" auf, wenn zwei Programme versuchen, gleichzeitig denselben Speicher zu nutzen. Die Autoren bezeichnen einen physischen Zusammenstoß als „räumlichen Data Race".

Wenn der Künstler einen Zug schreibt, der einen Zusammenstoß verursachen würde:

Der Inspektor betrachtet das 3D-Raster.
Er sieht, dass sich die „Werkzeug-Würfel" mit den „Klemmen-Würfeln" überschneiden.
Der mathematische Beweis schlägt fehl. Der Inspektor schreit: „STOPP! Sie versuchen, denselben Raum einzunehmen!"

5. Die Feedback-Schleife (Die „Nicht dorthin gehen"-Notiz)

In der Vergangenheit, wenn eine KI einen Fehler machte, sagten Sie ihr vielleicht einfach: „Versuch es noch einmal", und hofften, dass sie Glück hat. Das ist ineffizient.

Dieses System ist intelligenter. Wenn der Inspektor einen Zusammenstoß findet, sagt er nicht nur „Nein". Er identifiziert den genauen Ort des Zusammenstoßes und zeichnet eine winzige, präzise Box darum herum.

Die Nachricht: „Sie haben versucht, zu den Koordinaten X, Y, Z zu bewegen. Innerhalb dieser spezifischen Box befindet sich eine Klemme. Gehen Sie nicht in diese Box."
Die Korrektur: Diese Notiz wird an den Künstler zurückgesendet. Der Künstler liest die Notiz, erkennt den Fehler und schreibt die Anweisungen so um, dass er um die Box herumführt.

6. Das Ergebnis: „Korrekt durch Konstruktion"

Sie wiederholen diese Schleife – Künstler schreibt, Inspektor prüft, Inspektor weist auf den Zusammenstoß hin, Künstler korrigiert – bis der Inspektor mathematisch beweisen kann, dass das Werkzeug mit hoher Wahrscheinlichkeit nichts in dem aktuellen Arbeitsbereich, wie er dem Beweiser beschrieben wurde, berühren wird.

Da das System nur anhält, wenn dieser Beweis durchgeht, ist der endgültige Anweisungssatz „korrekt durch Konstruktion" für diesen Arbeitsbereich und diese Beschreibung der Hindernisse. Die Garantie lautet, dass der Werkzeugpfad unter dem räumlichen Modell, das der Inspektor erhalten hat, keine physische Kollision erzeugt. (Kein Beweis kann Kollisionen ausschließen, die durch Änderungen am Arbeitsbereich nach der Code-Generierung verursacht werden – verschobene Vorrichtungen, neuer Rohling, ein Operator, der ein Werkzeug in der Zelle lässt – daher ist dies eine arbeitsbereichsbedingte Garantie und keine bedingungslose.)

Zusammenfassung

Der Artikel beschreibt eine Methode, um KI-generierte Roboteranweisungen sicher zu machen, indem eine kreative KI mit einem strengen, mathematikbasierten Sicherheitsprüfer gepaart wird. Der Prüfer verwandelt die physische Welt in ein Raster, prüft auf Überschneidungen (Zusammenstöße) und sendet präzise „Betreten verboten"-Warnungen an die KI zurück, bis die Anweisungen mathematisch für den Arbeitsbereich, wie er dem Beweiser beschrieben wurde, als kollisionsfrei verifiziert sind.

Technische Zusammenfassung: Korrekte G-Code-Generierung durch Konstruktion mittels Separation Logic

Problemstellung

Die Integration von Large Language Models (LLMs) in die computergestützte numerische Steuerung (CNC) von Werkzeugmaschinen bietet das Potenzial, die Synthese von niedrigen Maschinendefinitionen (G-Code) aus natürlicher Sprache zu automatisieren. Der direkte Einsatz generativer Modelle in cyber-physischen Systemen bringt jedoch kritische Sicherheits Herausforderungen mit sich. Während LLMs wie das GLLM-Framework syntaktisch korrekten Code generieren können, der semantisch mit Zielgeometrien übereinstimmt, fehlt ihnen ein inhärentes räumliches Bewusstsein und deterministische Sicherheitsgarantien.

Eine primäre Einschränkung ist die „Halluzination" von Werkzeugwegen, die von unendlichen, hindernisfreien Arbeitsräumen ausgehen. Selbst logisch fundierte Werkzeugwege können aufgrund dynamischer Umgebungsvariablen (z. B. aktualisierte Spanneinrichtungen, Rohlingsabmessungen) und mechanischer Realitäten (z. B. Servo-Nachlauf, Spindel-Laufunwucht) zu physischen Kollisionen führen. Traditionelle Sicherheitsmechanismen, wie geometrische Simulationen oder Worst-Case-Margentests, sind für die Visualisierung effektiv, fehlen jedoch die symbolischen, mathematischen Beweise, die erforderlich sind, um die Sicherheit gegenüber kontinuierlichen physischen Bewegungen und Kollisionen in Randfällen zu garantieren. Folglich besteht ein Bedarf nach einem unabhängigen, deterministischen Verifikationsmechanismus, der vor der Codeausführung mathematisch eine räumliche Disjunktheit garantieren kann.

Methodik

Die Arbeit schlägt ein neuro-symbolisches Framework vor, das die probabilistische KI-Generierung mit der deterministischen formalen Verifikation verbindet. Die Architektur besteht aus einer unidirektionalen, iterativen Pipeline, die zwei primäre Agenten umfasst: einen Generator (LLM) und einen Verifier (Separation Logic Prover).

Hinweis zur Herkunft der Komponenten: Die im Folgenden beschriebenen Komponenten basieren auf vorangegangenen Arbeiten. Der Spatial-Heap-Formalismus und der SL-Prover wurden in der früheren Arbeit der Autoren („Separation Logic for Verifying Physical Collisions of CNC Programs", arXiv:2605.10437) eingeführt. Das GLLM-Framework ist eine bestehende Lösung zur G-Code-Generierung. Die eigentliche Leistung dieser Arbeit liegt in der iterativen neuro-symbolischen Integration dieser beiden bestehenden Komponenten in einer geschlossenen Schleife, bei der die Kollisionsbefunde des Verifiers als strukturierte Direktiven zurück an den Generator übergeben werden.

1. Die Generator-Verifier-Architektur

Generator (GLLM): Nutzt ein feinabgestimmtes LLM (z. B. StarCoder-3B), das durch Retrieval-Augmented Generation (RAG) erweitert wird. Das RAG-System injiziert statischen Kontext (kinematische Grenzen der Maschine, Topografie des Arbeitsraums, Werkzeuggeometrie) und dynamische Sicherheitsmargen in den Prompt. Dies schränkt die initiale Generierung des LLM so ein, dass sie physikalisch fundiert ist. Wichtig: Das GLLM-Framework ist eine bestehende Arbeit, deren Aufgabe ausschließlich die semantische und syntaktische Korrektheit der G-Code-Generierung ist; Kollisionsvermeidung war und ist nicht Teil des GLLM-Scope.
Verifier (SL Prover): Ein domänenspezifischer Separation Logic (SL) Prover, der den physischen CNC-Arbeitsraum als diskreten „Spatial Heap" behandelt. In diesem Modell wird die physische Belegung als logische Ressource verwaltet, wobei Koordinaten in einem diskreten 3D-Ganzzahlgitter ( $\mathbb{Z}^3$ ) Zuständen wie Tool, Environment, Stock oder Empty zugeordnet sind. Dieser Verifier und das zugrundeliegende Heap-Modell stammen aus der bereits zitierten Vorarbeit (arXiv:2605.10437) und werden in dieser Arbeit wiederverwendet, nicht neu definiert.

2. Die Neuro-Symbolische Schleife

Das Framework arbeitet durch einen kontinuierlichen iterativen Zyklus:

Initialisierung & RAG: Die Benutzerabsicht und die Grenzen des Arbeitsraums werden verarbeitet. Das RAG-System berechnet erweiterte Umgebungs Grenzen unter Verwendung einer Sicherheitsmarge ( $\epsilon$ ) vor und injiziert diese Einschränkungen in den Kontext des LLM.
Generierung & Diskretisierung (Der Parser): Das LLM synthetisiert einen Entwurf einer G-Code-Sequenz. Ein intermediärer Parser übersetzt diese kontinuierlichen kinematischen Befehle (Gleitkomma $\mathbb{R}^3$ ) in diskrete räumliche Logik ( $\mathbb{Z}^3$ ). Dieser Prozess wendet Minkowski-Summen-Dilatationen auf die Werkzeuggeometrie an, um physikalische Unsicherheiten (z. B. Servo-Nachlauf) einzukapseln, und wandelt die Trajektorie in eine endliche Menge von räumlichen Ressourcenanforderungen um. Die Diskretisierung erzeugt direkt eine endliche Menge von räumlichen Ressourcenanforderungen aus dem G-Code; der SL-Prover verifiziert dann die Trennung gegenüber der Umgebung auf Basis dieser symbolischen Ansprüche. Es wird in keinem Stadium eine geometrische Simulation, eine swept-volume-Rendering oder eine kinematische Wiedergabe durchgeführt.
Formale Verifikation: Der SL Prover bewertet den diskretisierten Pfad unter Verwendung von Separation Logic Tripeln $\{P\}C\{Q\}$ ${P} C {Q}$ . Er prüft spezifisch auf PHYSISCHE KOLLISIONEN, die mathematisch als Spatial Data Races formalisiert werden (Verletzungen der separierenden Konjunktion).
- Erfolg: Wenn die separierende Konjunktion gilt, ist der Zug mathematisch bewiesen kollisionsfrei.
- Fehler (Spatial Data Race): Wenn das Werkzeugvolumen mit der Umgebung schneidet, schlägt die separierende Konjunktion fehl. Dieser logische Widerspruch wird explizit als Spatial Data Race (physische Kollision) identifiziert. Der Prover prüft keine allgemeinen logischen oder syntaktischen Fehler; diese liegen in der Verantwortung des GLLM.
Feedback & Verfeinerung: Bei einem Fehler lehnt das System den Code nicht einfach ab. Stattdessen kondensiert es die kollidierenden Voxeln zu einem minimalen, achsenausgerichteten Bounding Box ( $B_{conflict}$ ). Dieser mathematische Fehler wird in ein strukturiertes, natürliches Sprachfehler-Signal übersetzt, das die spezifischen Koordinaten der Kollision und eine Anweisung enthält, das eingeschränkte Volumen zu umgehen.
Selbstkorrektur: Das Fehlersignal wird an das Kontextfenster des LLM angehängt und leitet das Modell an, den spezifischen Abschnitt des Werkzeugwegs zu verfeinern. Die Schleife wiederholt sich, bis ein formaler Beweis der räumlichen Disjunktheit erreicht ist.

Hauptbeiträge

Die Arbeit skizziert drei primäre Beiträge zum Bereich des neuro-symbolischen KI und der Fertigung:

Generator-Verifier Neuro-Symbolische Architektur: Ein bipartites Framework, das kontinuierliche physikalische Kinematik von der logischen räumlichen Bewertung entkoppelt. Das LLM fungiert als kreativer Generator, während der SL Prover als unerbittlicher, deterministischer Verifier agiert und sicherstellt, dass das Ausgabeergebnis durch Konstruktion korrekt ist.
Symbolisch-zu-Neurale Übersetzung via Spatial Data Races: Ein formaler Mechanismus, um logische Widersprüche an die neuronale Engine zu kommunizieren. Indem physische Kollisionen als Verletzungen der separierenden Konjunktion neu definiert werden – unter dem spezifischen Begriff Spatial Data Race – übersetzt das System geometrische Schnittpunkte in strukturierte, maschinenlesbare Direktiven (Bounding Boxes), die den Generierungsprozess des LLM einschränken. Der Begriff „Spatial Data Race" bezeichnet hier explizit die physikalische Kollision, nicht eine generische logische Fehlerklasse.
Deterministische, automatisierte Selbstkorrektur: Im Gegensatz zu empirischen Ansätzen, die auf Validierung durch den Menschen im Kreislauf oder Pfad-Ähnlichkeitsmetriken basieren, führt dieses Framework einen vollständig automatisierten Feedback-Loop ein. Der SL Prover liefert präzises, falsch-positiv-freies räumliches Feedback, das es dem LLM ermöglicht, Trajektorien autonom zu verfeinern, bis ein formaler Sicherheitsbeweis etabliert ist.

Ergebnisse und Behauptungen

Die Arbeit etabliert die theoretische Machbarkeit und das architektonische Design dieses neuro-symbolischen Ansatzes. Sie behauptet, dass durch die Integration des GLLM-Frameworks mit dem Spatial-Heap-Modell:

Das System physische Kollisionen erfolgreich in logische Widersprüche übersetzt, die formal verifiziert werden können.
Die Verwendung von Minkowski-Summen in der Diskretisierungsphase es dem System ermöglicht, Sicherheitsmargen gegen mechanische Unsicherheiten mathematisch zu garantieren, ohne die diskrete Logik des Provers zu verkomplizieren.
Der Feedback-Mechanismus den probabilistischen Suchraum des LLM effektiv einschränkt, wiederholte Halluzinationen verhindert und das Modell zu mathematisch verifizierten, kollisionsfreien Werkzeugwegen führt.

Die Autoren stellen fest, dass die Sicherheitsgarantie raummodellabhängig ist: Der formale Beweis der räumlichen Disjunktheit gilt innerhalb des im Spatial Heap modellierten Arbeitsraums zum Zeitpunkt der Codegenerierung. Eine umfassende experimentelle Validierung (z. B. Benchmarking gegen traditionelle CAM-Tools wie VERICUT auf großskaligen industriellen Sequenzen) bleibt eine laufende Aufgabe für zukünftige Arbeiten.

Bedeutung

Die Bedeutung dieser Arbeit liegt in ihrem Wandel von empirischer Sicherheit zu formaler Sicherheit in der KI-gesteuerten Fertigung. Indem der physische Arbeitsraum als verwaltete logische Ressource konzeptualisiert wird, ermöglicht das Framework die Anwendung rigoroser mathematischer Beweise auf cyber-physische Systeme. Dieser Ansatz adressiert die kritische „Intent-Lücke" zwischen menschlichen Anweisungen und Maschinenausführung und bietet einen skalierbaren Weg hin zur vollständig autonomen, kollisionsfreien CNC-Fertigung. Es zeigt, dass generative KI sicher in hochriskanten physischen Umgebungen eingesetzt werden kann, wenn sie mit einer deterministischen, symbolischen Verifikationsschicht gekoppelt ist, die Sicherheit als logische Notwendigkeit und nicht als statistische Wahrscheinlichkeit behandelt. Wichtig: Die formale Sicherheitsgarantie gilt strikt für den Arbeitsraum, wie er im Spatial Heap zum Zeitpunkt der Generierung modelliert wurde, und erstreckt sich nicht auf Umgebungsänderungen, die nach der Codegenerierung auftreten.

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