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.

翻译：本文提出了一种面向G代码生成的神经符号框架，通过整合GLLM神经方法（Abdelaal等，2025）与已建立的分离逻辑（SL）验证器。我们引入了一个双组件架构：GLLM作为创造性生成器，而利用空间堆模型的SL证明器则充当确定性验证器。通过将物理碰撞定义为逻辑空间数据竞争——即违反SL中的分离合取——该框架将证明失败转化为结构化的数学反馈。这些失败被压缩为最小边界框，作为GLLM迭代自校正的精确空间指导。这种协同机制构建了一个自校正生成循环，减少了人工监督需求，支持生成经过验证的G代码以增强自主制造的安全性。