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.

翻译：暂无翻译