Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
For autonomous manufacturing, this work addresses the problem of generating safe, collision-free G-code without manual verification, though the approach is incremental as it builds on existing methods.
The paper presents a neuro-symbolic framework that combines a neural G-code generator (GLLM) with a Separation Logic verifier to produce correct-by-construction G-code, reducing manual oversight and enhancing safety in autonomous manufacturing.
This paper proposes a neuro-symbolic framework for G-code generation by integrating the GLLM neural method (Abdelaal et al., 2025) with our established Separation Logic (SL) verifier. We introduce a two-component architecture where GLLM serves as a creative generator and the SL Prover, utilizing the Spatial Heap model, acts as a deterministic verifier. By defining physical collisions as logical Spatial Data Races - violations of the separating conjunction in SL - the framework translates proof failures into structured mathematical feedback. These failures are condensed into minimal bounding boxes that act as precise spatial directives for GLLM's iterative self-correction. This synergy establishes a self-correcting generative cycle that reduces the need for manual oversight, supporting the production of verified G-code to enhance safety in autonomous manufacturing.