用大模型生成G代码，语法正确、几何也对，仍然可能在机床上撞刀。原因不在模型“不会写”，而在它缺少对当前夹具、毛坯尺寸、伺服滞后与主轴跳动的确定认知。GLLM一类工作已经用微调模型、RAG与“生成器—评估器”回路把自然语言变成RS-274指令；这篇论文进一步加了一层确定性的形式化验证器，让刀路在进入物理世界之前先过一道数学证明。
生成器与证明器分工
架构是二分结构：GLLM作为生成器，负责把非正式加工意图翻译成初始刀路；分离逻辑（Separation Logic）证明器作为验证器，判定刀路扫掠体与受限环境是否空间互斥。生成端保留概率性与创造性，验证端只做确定性的“是/否”，两者之间用解析器（Parser）做握手。
解析器先把连续的运动学离散化：把G代码坐标、刀具几何、夹具与毛坯包围盒映射到整数格点，并用离散闵可夫斯基和把伺服误差、主轴跳动等物理不确定性膨胀成一个安全包络。这样证明器只需要处理有限的空间文字，而不必在浮点连续域里做几何计算。
把碰撞写成“空间数据竞争”
论文把CNC工作空间建模为“空间堆”（Spatial Heap）：每个离散坐标对应一种占用状态——刀具、环境、毛坯或空。G00快移要求整个扫掠体只经过已验证的空域；G01切削则把经过的毛坯状态改为空、释放刀具尾部体积、再分配新的刀具位置。碰撞不再是一个几何报警，而是分离合取（separating conjunction）无法成立：当刀具请求的坐标集合与环境或毛坯的坐标集合相交，证明失败，系统将其判定为“空间数据竞争”。
关键在失败之后做什么。系统不会简单丢弃代码让模型“再试一次”，而是把冲突体素压缩成一个最小包围盒，连同“哪条指令、边界在哪、该怎么改”一起写成结构化的自然语言误差信号，回灌到模型上下文。模型据此做定向修正，例如在横向进入夹具前插入Z轴抬刀。循环持续到分离合取成立、输出安全证明为止。
RAG先把安全边界写进提示词
为减少第一轮就撞的概率，框架在生成前用RAG注入三类确定性参数：机床行程极限、工作空间地形（毛坯与所有夹具的坐标包围盒）、当前刀具半径与有效长度。更重要的是，它把证明器要求的安全裕度提前算进提示词：例如证明器要求ε=2.0毫米缓冲，RAG就把所有夹具与毛坯的包围盒按该裕度膨胀后再注入。模型于是围绕“已被数学加胖的障碍物”规划轨迹，首轮就更容易生成“构造即正确”的刀路。
这套方法解决了什么，又没解决什么
它解决的是安全判定的确定性与可解释性：证明失败给出的是精确空间约束，而不是模糊的碰撞提示；反馈可定位、可复现，也不依赖人工在回路里反复试。它没有解决的是工艺本身的合理性——进给、转速、装夹顺序是否最优，仍要由工艺知识与刀具库来判断。论文以形式化架构与论证为主，未给出量产产线的量化实验，这也意味着它更像一道可嵌入生成流程的安全闸门，而不是完整的CAM替代品。
资料来源：Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic — arXiv（2026-05）。本文为技术要点整理/编译，非原文全文。