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

This paper presents a neuro-symbolic framework that integrates a GLLM generator with a Separation Logic verifier to enable the self-correcting, collision-free production of G-code by translating logical proof failures into precise spatial directives for iterative refinement.

The Gist

Imagine you are trying to teach a very creative, imaginative artist (an AI) how to carve a statue out of a block of marble using a robotic arm. The artist is great at understanding your description ("Make a bird") and can write down the instructions for the robot. However, this artist has never actually seen the workshop. They don't know where the heavy clamps holding the marble are, or how big the robot's arm is. They might write instructions that look perfect on paper but would cause the robot to smash right into a clamp, breaking the machine.

This paper proposes a solution to that problem by teaming up the creative artist with a strict, mathematically perfect safety inspector.

Here is how their partnership works, broken down into simple steps:

1. The Two Partners

• The Artist (the AI): This is a Large Language Model called GLLM, brought in from earlier work. The GLLM is great at taking your natural-language request ("Carve a bird") and turning it into a list of robotic instructions (G-code). It handles the Retrieval-Augmented Generation (pulling in context about the machine and the task) and checks that the code is syntactically and semantically reasonable. What it does NOT do, and was never designed to do, is keep the robot from physically smashing into things — it has no built-in collision avoidance.
• The Inspector (the Safety Prover): This is a Separation Logic prover that the authors brought in from their own earlier work — specifically the paper Separation Logic for Verifying Physical Collisions of CNC Programs (arXiv:2605.10437), where the Spatial Heap model and the prover were first introduced. The Inspector's ONE job is to detect physical collisions — situations where the tool and an obstacle would try to occupy the same space at the same time. It is not a general-purpose code reviewer; it is not checking whether the code is "wrong" in some broad sense; it is purely a crash detector.

What this paper actually contributes is the wiring between these two existing tools — a neuro-symbolic feedback loop in which the Inspector's collision findings are translated back into structured guidance for the Artist.

2. The "Digital Sandbox" (The Spatial Heap)

To make the math work, the system turns the physical workshop into a giant 3D grid of tiny cubes (like a 3D version of Minecraft).

• Some cubes are marked as "Marble" (the material to be cut).
• Some are marked as "Clamps" (obstacles).
• Some are marked as "Empty Air" (safe space).
• The robot's tool is also a specific shape of cubes.

Importantly, the Inspector never actually watches the robot move and never runs a geometric simulation. It reads the G-code script directly, line by line, and works out which cubes each tool move would need to occupy. The rule it enforces is simple: the cubes claimed by the tool must not be already claimed by a clamp or any other obstacle.

3. The Safety Buffer (The "Fluffy Coat")

Robots aren't perfect. They might wobble slightly, or the tool might bend a tiny bit. To account for this, the system doesn't just check the tool's exact size. It gives the tool a "fluffy coat" (a mathematical safety margin) around it.

• If the tool is 5mm wide, the system pretends it is 7mm wide to be safe.
• The Inspector checks if this "fluffy tool" hits anything. If it does, the move is forbidden.

4. The "Data Race" (The Crash Alarm)

In computer science, a "data race" happens when two programs try to use the same memory at the same time. The authors call a physical crash a "Spatial Data Race."

When the Artist writes a move that would cause a crash:

1. The Inspector looks at the 3D grid.
2. It sees the "Tool Cubes" overlapping with the "Clamp Cubes."
3. The math proof fails. The Inspector screams, "STOP! You are trying to occupy the same space!"

5. The Feedback Loop (The "Don't Go There" Note)

In the past, if an AI made a mistake, you might just tell it, "Try again," and hope it gets lucky. That's inefficient.

This system is smarter. When the Inspector finds a crash, it doesn't just say "No." It pinpoints the exact location of the crash and draws a tiny, precise box around it.

• The Message: "You tried to move to coordinates X, Y, Z. There is a clamp inside this specific box. Do not go in this box."
• The Correction: This note is sent back to the Artist. The Artist reads the note, realizes the mistake, and rewrites the instructions to go around the box.

6. The Result: "Correct-by-Construction"

They keep doing this loop — Artist writes, Inspector checks, Inspector points out the crash, Artist fixes it — until the Inspector can mathematically prove that the tool is highly likely not to collide with anything in the current workspace as described to the prover.

Because the system only stops when this proof goes through, the final set of instructions is "Correct-by-Construction" for that workspace and that description of the obstacles. The guarantee is that, under the spatial model the Inspector was given, the toolpath does not produce a physical collision. (No proof can rule out collisions caused by changes to the workspace AFTER the code is generated — moved fixtures, new stock, an operator leaving a tool inside the cell — so this is a workspace-conditional guarantee, not an unconditional one.)

Summary

The paper describes a way to make AI-generated robot instructions safe by pairing a creative AI with a strict math-based safety checker. The checker turns the physical world into a grid, checks for overlaps (crashes), and sends precise "do not enter" warnings back to the AI until the instructions are mathematically verified against the current spatial model.

Technical Summary

Technical Summary: Correct-by-Construction G-Code Generation via Separation Logic

Problem Statement

The integration of Large Language Models (LLMs) into Computer Numerical Control (CNC) machining offers the potential to automate low-level machine instruction synthesis (G-code) from natural language. However, deploying generative models directly into cyber-physical systems introduces critical safety challenges. While LLMs like the GLLM framework can generate syntactically correct code that aligns semantically with target geometries, they lack inherent spatial awareness and deterministic safety guarantees.

A primary limitation is the "hallucination" of toolpaths that assume infinite, obstacle-free workspaces. Even logically sound toolpaths may result in physical collisions due to dynamic environmental variables (e.g., updated fixtures, stock dimensions) and mechanical realities (e.g., servo lag, spindle runout). Traditional safety mechanisms, such as geometric simulations or worst-case margin testing, are effective for visualization but lack the symbolic, mathematical proofs required to guarantee safety against continuous physical movements and corner-case collisions. Consequently, there is a need for an independent, deterministic verification mechanism that can mathematically guarantee spatial disjointness before code execution.

Methodology

The paper proposes a neuro-symbolic framework that bridges probabilistic AI generation with deterministic formal verification. The architecture consists of a unidirectional, iterative pipeline involving two primary agents: a Generator (LLM) and a Verifier (Separation Logic Prover).

Note: The Spatial Heap formalism and the SL prover used here were introduced in the authors' prior work (Lee, arXiv:2605.10437). The present paper integrates that existing prover with the GLLM in a closed-loop neuro-symbolic pipeline.

1. The Generator-Verifier Architecture

• Generator (GLLM): Utilizes a fine-tuned LLM (e.g., StarCoder-3B) enhanced with Retrieval-Augmented Generation (RAG). The RAG system injects static context (machine kinematic limits, workspace topography, tool geometry) and dynamic safety margins into the prompt. This constrains the LLM's initial generation to be physically grounded. Crucially, the GLLM is a previously published framework responsible solely for RAG-augmented G-code generation and semantic/syntactic correctness; collision avoidance was never part of its scope.
• Verifier (SL Prover): A domain-specific Separation Logic (SL) prover that treats the physical CNC workspace as a discrete "Spatial Heap." In this model, physical occupancy is managed as a logical resource, where coordinates in a discrete 3D integer lattice ($\mathbb{Z}^3$) map to states such as Tool, Environment, Stock, or Empty. This prover and the Spatial Heap model are existing components from the author's prior work, reused here without redefinition.

2. The Neuro-Symbolic Loop

The framework operates through a continuous iterative cycle:

1. Initialization & RAG: The user intent and workspace bounds are processed. The RAG system pre-computes expanded environmental bounds using a safety margin ($\epsilon$) and injects these constraints into the LLM's context.
2. Generation & Discretization (The Parser): The LLM synthesizes a draft G-code sequence. An intermediate Parser translates these continuous kinematic commands (floating-point $\mathbb{R}^3$) into discrete spatial logic ($\mathbb{Z}^3$). This process applies Minkowski sum dilations to the tool geometry to encapsulate physical uncertainties (e.g., servo lag), converting the trajectory into a finite set of spatial resource requests. The discretisation produces a finite set of spatial resource requests directly from the G-code; the SL Prover then verifies separation against the environment on these symbolic claims. No geometric simulation, swept-volume rendering, or kinematic playback is performed at any stage.
3. Formal Verification: The SL Prover evaluates the discretized path using Separation Logic Triples $\{P\}C\{Q\}$. It checks for the Separating Conjunction ($*$), which asserts that the tool's swept volume is strictly disjoint from environmental obstacles.
   • Success: If the conjunction holds, the move is mathematically proven safe.
   • Failure (Spatial Data Race): If the tool volume intersects with the environment, the separating conjunction fails. This specific logical contradiction is identified as a Spatial Data Race, representing a verified physical collision.
4. Feedback & Refinement: Upon failure, the system does not simply reject the code. Instead, it condenses the conflicting voxels into a minimal, axis-aligned bounding box ($B_{conflict}$). This mathematical failure is translated into a structured, natural language error signal containing the specific coordinates of the collision and a directive to bypass the restricted volume.
5. Self-Correction: The error signal is appended to the LLM's context window, guiding the model to refine the specific segment of the toolpath. The loop repeats until a formal proof of spatial disjointness is achieved.

Key Contributions

The paper outlines three primary contributions to the field of neuro-symbolic AI and manufacturing:

1. Generator-Verifier Neuro-Symbolic Architecture: A bipartite framework that decouples continuous physical kinematics from logical spatial evaluation by integrating two existing components: the GLLM for generation and the SL Prover for verification. The LLM acts as a creative generator, while the SL Prover acts as an unyielding, deterministic verifier, ensuring that the output is correct-by-construction.
2. Symbolic-to-Neural Translation via Spatial Data Races: A formal mechanism to communicate logical contradictions to the neural engine. By redefining physical collisions specifically as Spatial Data Races (violations of the separating conjunction in Separation Logic), the system translates geometric intersections into structured, machine-readable directives (bounding boxes) that constrain the LLM's generative process.
3. Deterministic, Automated Self-Correction: Unlike empirical approaches relying on human-in-the-loop validation or path-similarity metrics, this framework introduces a fully automated feedback loop. The SL Prover provides precise, zero-false-positive spatial feedback regarding physical collisions, allowing the LLM to autonomously refine trajectories until a formal safety proof is established.

Results and Claims

The paper establishes the theoretical feasibility and architectural design of this neuro-symbolic integration. It claims that by integrating the GLLM framework with the existing Spatial Heap model:

• The system successfully translates physical collisions into logical contradictions (Spatial Data Races) that can be formally verified.
• The use of Minkowski sums in the discretization phase allows the system to mathematically guarantee safety margins against mechanical uncertainties without complicating the discrete logic of the prover.
• The feedback mechanism effectively restricts the LLM's probabilistic search space, preventing repeated hallucinations and guiding the model toward mathematically verified, collision-free toolpaths.

The authors note that while the architecture is established, comprehensive experimental validation (e.g., benchmarking against traditional CAM tools like VERICUT on large-scale industrial sequences) remains an ongoing effort for future work.

Significance

The significance of this work lies in its shift from empirical safety to formal safety in AI-driven manufacturing. By conceptualizing the physical workspace as a managed logical resource, the framework enables the application of rigorous mathematical proofs to cyber-physical systems. This approach addresses the critical "intent gap" between human instructions and machine execution, offering a scalable path toward fully autonomous, zero-collision CNC manufacturing. It demonstrates that generative AI can be safely deployed in high-stakes physical environments when coupled with a deterministic, symbolic verification layer that treats safety as a logical necessity rather than a statistical probability. It is important to note that this formal-safety guarantee applies to the workspace as modelled in the Spatial Heap at the time of code generation and does not extend to post-generation environmental changes.