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

TL;DR

This paper introduces a neuro-symbolic framework combining neural G-code generation with formal verification using Separation Logic to enable self-correcting, verified autonomous manufacturing processes.

Contribution

It presents a novel integration of neural G-code generation with formal verification via Separation Logic, enabling self-correction and increased safety in manufacturing.

Findings

Framework successfully extracts geometric data from CAD models.

Logical violations are translated into feedback for self-correction.

Approach reduces human supervision in G-code generation.

Abstract

This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method (Abdelaal et al., 2025) with formal verification via a Separation Logic (SL) prover. To establish a reliable physical baseline, the framework extracts deterministic boundary representations from 3D CAD models (STEP files) using the OpenCASCADE framework. This extracted geometric data supports a two-component architecture: the LLM serves as an initial code generator, while the SL Prover, utilizing a Spatial Heap model, evaluates the output. By conceptualizing physical collisions as logical Spatial Data Races -- violations of the separating conjunction in SL -- our framework translates proof failures into structured mathematical feedback. These failures are condensed into bounding boxes that serve as directives for the LLM's iterative self-correction. Ultimately, this work aims to develop a self-correcting system that reduces the need for human supervision, leading to safer and verified autonomous manufacturing.