想象一下，你正在尝试教导一位极具创造力和想象力的艺术家（一个人工智能）如何使用机械臂从一块大理石中雕刻出一座雕像。这位艺术家非常擅长理解你的描述（“雕刻一只鸟”），并能将之转化为机器人的操作指令。然而，这位艺术家从未真正见过这个车间。他们不知道固定大理石的沉重夹具位于何处，也不知道机械臂的尺寸有多大。他们可能会写出在纸面上看起来完美的指令，但这些指令却会导致机器人直接撞向夹具，从而损坏机器。

本文提出了一种解决方案，通过将富有创造力的艺术家与一位严格且数学上完美的安全检查员组队合作来解决这一问题。

以下是他们合作方式的分解步骤：

1. 两位合作伙伴

艺术家（人工智能）： 这是一个大型语言模型（具体称为 GLLM），源自早期的研究工作。GLLM 擅长将你的自然语言请求（“雕刻一只鸟”）转化为机器人指令列表（G 代码）。它处理检索增强生成（RAG），即引入关于机器和任务的相关背景信息，并检查代码在语法和语义上是否合理。但它不负责防止机器人物理撞击，也从未被设计用于此目的——它没有内置的避障功能。
检查员（安全证明器）： 这是作者从他们之前的工作中引入的一个分离逻辑证明器，具体出自论文《Separation Logic for Verifying Physical Collisions of CNC Programs》(arXiv:2605.10437)，其中首次引入了空间堆（Spatial Heap）模型和证明器。检查员的唯一职责是检测物理碰撞——即工具和障碍物试图在同一时间占据同一空间的情况。它不是通用的代码审查员，不检查代码在广义上是否“错误”；它纯粹是一个碰撞探测器。

本文的实际贡献在于将这两个现有工具连接起来——构建一个神经符号反馈循环，将检查员发现的碰撞转化为对艺术家的结构化指导。

2. “数字沙盒”（空间堆）

为了让数学运算生效，系统将物理车间转化为一个由微小立方体组成的巨大 3D 网格（类似于 3D 版的《我的世界》）。

一些立方体被标记为**“大理石”**（待切割的材料）。
一些被标记为**“夹具”**（障碍物）。
一些被标记为**“真空”**（安全空间）。
机器人的工具也被表示为特定形状的立方体。

重要的是，检查员从不实际观察机器人移动，也从不运行几何模拟。它直接逐行读取 G 代码脚本，计算出每个工具移动需要占据哪些立方体。它执行的规则很简单：工具所占据的立方体，绝不能已经被夹具或其他障碍物所占据。

3. 安全缓冲区（“蓬松外套”）

机器人并非完美无缺。它们可能会轻微晃动，或者工具可能会发生微小弯曲。为了应对这种情况，系统不仅仅检查工具的确切尺寸，而是给工具穿上了一件“蓬松外套”（即数学安全裕度）。

如果工具宽 5 毫米，系统为了安全起见会将其视为 7 毫米宽。
检查员会检查这件“蓬松工具”是否撞到了任何东西。如果撞到了，该移动就会被禁止。

4. “数据竞争”（碰撞警报）

在计算机科学中，“数据竞争”是指两个程序试图同时使用同一内存的情况。作者将物理碰撞称为**“空间数据竞争”**。

当艺术家写出会导致碰撞的移动指令时：

检查员读取代码并查看 3D 网格。
它发现“工具立方体”与“夹具立方体”重叠。
数学证明失败。检查员大喊：“停止！你正试图占据同一空间！”

5. 反馈循环（“别去那里”的便条）

在过去，如果人工智能犯错，你可能只会告诉它“再试一次”，并指望它碰运气。这是低效的。

这个系统更聪明。当检查员发现碰撞时，它不仅仅说“不行”。它会精确定位碰撞发生的具体位置，并在其周围画出一个微小而精确的方框。

信息： “你试图移动到坐标 X、Y、Z。在这个特定的方框内有一个夹具。不要进入这个方框。”
修正： 这条便条被发送回艺术家。艺术家阅读便条，意识到错误，并重新编写指令以绕过该方框。

6. 结果：“构建即正确”

他们不断进行这个循环——艺术家编写，检查员检查，检查员指出碰撞，艺术家修正——直到检查员能够从数学上证明，在当前描述给证明器的工作空间中，工具极不可能与任何障碍物发生碰撞。

因为该系统仅在证明通过时才停止，所以最终的指令集对于该工作空间及其障碍物描述而言是**“构建即正确”的。保证是：在检查员所接收到的空间模型下，工具路径不会产生物理碰撞。（没有任何证明能排除代码生成后工作空间发生变化——如夹具移动、新工件出现、操作员将工具遗留在工作单元内——所导致的碰撞，因此这是一个基于工作空间条件的保证**，而非无条件的保证。）

总结

本文描述了一种通过将有创造力的 AI 与严格的基于数学的安全检查器配对，来确保 AI 生成的机器人指令安全的方法。检查器将物理世界转化为网格，检查重叠（碰撞），并向 AI 发送精确的“禁止进入”警告，直到指令在数学上被验证为与当前空间模型一致且无碰撞。

技术摘要：基于分离逻辑的“构建即正确”G 代码生成

问题陈述

将大语言模型（LLM）集成到计算机数控（CNC）加工中，为从自然语言自动合成底层机器指令（G 代码）提供了潜力。然而，将生成式模型直接部署到信息物理系统中引入了关键的安全挑战。虽然像 GLLM 框架这样的 LLM 能够生成在语法上正确且与目标几何形状在语义上对齐的代码，但它们缺乏固有的空间感知能力和确定性的安全保证。

一个主要限制是工具路径的“幻觉”，即假设存在无限且无障碍的工作空间。即使逻辑上合理的工具路径，也可能由于动态环境变量（例如更新的夹具、毛坯尺寸）和机械现实（例如伺服滞后、主轴跳动）而导致物理碰撞。传统的安全机制，如几何仿真或最坏情况裕度测试，虽对可视化有效，但缺乏符号化的数学证明，无法保证针对连续物理运动和极端情况碰撞的安全性。因此，需要一种独立的、确定性的验证机制，在代码执行前从数学上保证空间上的不相交性。

方法论

本文提出了一种神经符号框架，将概率性 AI 生成与确定性形式验证相结合。该架构由一个单向、迭代的流水线组成，涉及两个主要代理：生成器（LLM）和验证器（分离逻辑证明器）。

注：本文使用的空间堆（Spatial Heap）形式化方法和分离逻辑（SL）证明器源自作者先前的工作（Lee, arXiv:2605.10437）。本文的贡献在于将现有的证明器与 GLLM 集成到一个闭环神经符号流水线中。

1. 生成器 - 验证器架构

生成器（GLLM）： 利用经过微调的 LLM（例如 StarCoder-3B），并增强检索增强生成（RAG）。RAG 系统将静态上下文（机器运动学限制、工作空间地形、刀具几何形状）和动态安全裕度注入提示中。GLLM 是一个已发表的框架，其在此处的角色保持不变：负责生成 G 代码草案并确保语义和语法正确性。需要明确的是，碰撞避免从未是 GLLM 的范畴，它也不执行碰撞检测。
验证器（SL 证明器）： 一个特定领域的分离逻辑（SL）证明器，将物理 CNC 工作空间视为离散的**“空间堆”**。在此模型中，物理占用被作为逻辑资源进行管理，离散三维整数格点（ $\mathbb{Z}^3$ ）中的坐标映射为 Tool（刀具）、Environment（环境）、Stock（毛坯）或 Empty（空）等状态。该证明器及空间堆模型是作者先前提出的（Lee, arXiv:2605.10437），本文直接复用该证明器，而非重新定义它。
本文贡献： 本文的核心贡献在于这两个现有组件之间的迭代神经符号集成——即构建一个反馈流水线，将验证器发现的碰撞（空间数据竞争）编码为边界框指令并反馈给生成器。

2. 神经符号循环

该框架通过连续的迭代周期运行：

初始化与 RAG： 处理用户意图和工作空间边界。RAG 系统使用安全裕度（ $\epsilon$ ）预计算扩展的环境边界，并将这些约束注入 LLM 的上下文中。
生成与离散化（解析器）： LLM 合成一份 G 代码草案序列。中间解析器将这些连续的运动学命令（浮点数 $\mathbb{R}^3$ ）转换为离散空间逻辑（ $\mathbb{Z}^3$ ）。此过程对刀具几何形状应用闵可夫斯基和膨胀，以封装物理不确定性（例如伺服滞后），将轨迹转换为有限集的空间资源请求。离散化直接从 G 代码生成一组有限的空间资源请求；SL 证明器随后在这些符号化声明上验证与环境的分离性。本流程中不进行任何几何仿真、扫掠体积渲染或运动学回放。
形式验证： SL 证明器使用分离逻辑三元组 $\{P\}C\{Q\}$ ${P} C {Q}$ 评估离散化路径。它检查分离合取（ $*$ $*$ ），该合取断言刀具的扫掠体积与环境障碍物严格不相交。
- 成功： 如果合取成立，则该移动在数学上被证明是安全的。
- 失败（空间数据竞争）： 如果刀具体积与环境相交，则分离合取失败。这种逻辑矛盾被识别为空间数据竞争（Spatial Data Race），即物理碰撞的形式化表达。SL 证明器不检查通用的代码逻辑错误；语义和语法正确性由上游的 GLLM 负责。
反馈与精炼： 一旦失败，系统不会简单地拒绝代码。相反，它将冲突的体素压缩为一个最小的、轴对齐的边界框（ $B_{conflict}$ ）。这种数学上的失败被转化为结构化的自然语言错误信号，其中包含碰撞的具体坐标以及绕过受限体积的指令。
自我修正： 错误信号被附加到 LLM 的上下文窗口中，引导模型精炼工具路径的特定部分。该循环重复进行，直到获得空间不相交性的形式证明。

主要贡献

本文概述了该神经符号 AI 和制造领域的三项主要贡献：

生成器 - 验证器神经符号架构： 一个将连续物理运动学与逻辑空间评估解耦的二元框架。LLM 充当创造性生成器，而 SL 证明器充当坚定不移的确定性验证器，确保输出是构建即正确的。
通过空间数据竞争实现的符号到神经转换： 一种将逻辑矛盾传达给神经引擎的形式化机制。通过将物理碰撞重新定义为对分离合取（即空间数据竞争）的违反，系统将几何交集转化为结构化的、机器可读的指令（边界框），从而约束 LLM 的生成过程。在此框架中，“空间数据竞争”是物理碰撞的正式名称，而非通用的逻辑错误类别。
确定性的自动化自我修正： 与依赖人工循环验证或路径相似性度量的经验方法不同，该框架引入了全自动反馈循环。SL 证明器提供精确的、零误报的空间反馈，使 LLM 能够自主精炼轨迹，直到建立形式安全证明。

结果与主张

本文确立了该神经符号方法的理论可行性和架构设计。它主张通过将 GLLM 框架与空间堆模型相结合：

该系统成功地将物理碰撞转化为可形式验证的逻辑矛盾（空间数据竞争）。
在离散化阶段使用闵可夫斯基和，使系统能够在不复杂化证明器离散逻辑的情况下，从数学上保证针对机械不确定性的安全裕度。
反馈机制有效地限制了 LLM 的概率搜索空间，防止重复幻觉，并引导模型走向经过数学验证的无碰撞工具路径。

作者指出，虽然架构已确立，但全面的实验验证（例如，在大规模工业序列上与 VERICUT 等传统 CAM 工具进行基准测试）仍是未来工作的持续努力。

意义

这项工作的意义在于其从 AI 驱动制造中的经验安全向形式安全的转变。通过将物理工作空间概念化为受管理的逻辑资源，该框架使得将严格的数学证明应用于信息物理系统成为可能。这种方法解决了人类指令与机器执行之间关键的“意图差距”，为完全自主、零碰撞的 CNC 制造提供了一条可扩展的路径。它证明了，当生成式 AI 与确定性符号验证层相结合，将安全视为逻辑必然性而非统计概率时，它可以被安全地部署在高 stakes 的物理环境中。需要明确的是，这种形式安全保证在代码生成时空间堆所建模的工作空间范围内成立，并不延伸至代码生成后的环境变化。

Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic