Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
This paper presents a neuro-symbolic framework that integrates a GLLM generator with a Separation Logic verifier to enable the self-correcting, collision-free production of G-code by translating logical proof failures into precise spatial directives for iterative refinement.