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.

翻译：本文提出了一种面向G代码生成的神经符号框架，旨在将GLLM方法（Abdelaal等, 2025）的神经生成能力与基于分离逻辑（SL）证明器的形式化验证相结合。为建立可靠的物理基准，该框架利用OpenCASCADE框架从3D CAD模型（STEP文件）中提取确定性边界表示。提取的几何数据支撑起双组件架构：大语言模型（LLM）作为初始代码生成器，而采用空间堆模型的SL证明器则对输出进行评估。通过将物理碰撞概念化为逻辑上的空间数据竞争——即分离逻辑中分离合取关系的违反——本框架将证明失败转化为结构化的数学反馈。这些失败被压缩为边界框，作为LLM迭代自修正的指导指令。最终，本工作旨在构建一个减少人工监督需求的自修正系统，从而实现更安全、可验证的自主制造。