Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
TLDR
This paper introduces a neuro-symbolic framework for correct-by-construction G-code generation, using a neural generator and a logic verifier for self-correction.
Key contributions
- Integrates the GLLM neural method with a Separation Logic verifier for G-code generation.
- Models physical collisions as "Spatial Data Races" within the Separation Logic framework.
- Converts proof failures into precise spatial directives (bounding boxes) for neural self-correction.
- Establishes a self-correcting generative cycle to produce verified G-code, reducing manual oversight.
Why it matters
This paper significantly enhances safety in autonomous manufacturing by ensuring G-code correctness. It reduces the need for manual oversight, making the generation process more reliable and efficient. This neuro-symbolic approach offers a robust path towards verified automated production.
Original Abstract
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.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.