SemaPLC：面向 PLC 代码生成的项目接地、验证门控智能体框架 SemaPLC: A Project-Grounded, Verification-Gated Agent Harness for PLC Code Generation
验证门控智能体框架：LLM 生成的 PLC 逻辑须经规范、编译与实机三重外部验证方可交付
前置知识
PLC 与 IEC 61131-3 / Structured Text
PLC（可编程逻辑控制器）是驱动工厂产线、电站、水处理设施实时控制回路的工业计算机。IEC 61131-3 是其主流编程标准，其中 Structured Text（ST）是类 Pascal 的文本语言。PLC 程序按扫描周期（scan cycle）循环执行：读输入、执行逻辑、写输出，因此定时器（TON）、边沿检测等跨周期状态构造是核心也是难点。
本文的生成对象就是 ST 语言的功能块与程序，扫描周期语义决定了规范审查清单和运行时轨迹采样的设计，不理解执行模型就看不懂验证为何分层。
POU（Program Organization Unit）
POU 是 IEC 61131-3 中代码的组织单元，包括程序（Program）、功能块（Function Block）和函数（Function）。此前 LLM 生成 PLC 代码的基准几乎都以独立 POU 为单位：给定需求文本和接口声明，生成单个可编译单元。
论文区分了功能轨道（117 个独立 POU 任务）与项目上下文轨道（65 个需嵌入真实工程的任务），这一粒度差异正是本文对现有评测的核心批评点。
形式化验证与模型检查（PLCverif / nuXmv）
模型检查把程序翻译成状态机后穷举验证时序逻辑属性是否被满足。PLCverif 是 ABB 开源的工具，把 ST 代码与需求模式翻译为 nuXmv 等模型检查器的输入。它给出强保证但有覆盖边界：不支持的构造（如 TON 定时器）、翻译失败或超时都会返回非结论性（inconclusive）结果。
功能轨道的裁判就是 PLCverif+nuXmv 管道，且论文用表 5 证明定时器程序 0% 结论性覆盖，这是引入实机运行时验证的直接动机。
黄金轨迹差分（golden-trace differential）
把候选程序与隐藏的参考实现部署到同一实时 PLC 运行时，注入相同的场景输入 T，采样双方外部可观测变量的时间轨迹并逐端口比对（布尔和数值要求精确一致），动态分 $D(P', T)$ 是各场景端口一致比例的均值。它直接度量行为正确性而非代码形态。
这是项目轨道的核心指标，也是论文最有力的发现来源：静态分相近的方法在动态分上差距可达 30 分。
验证门控与交付完整性
验证门控指智能体无权凭自我评估终止任务，只有当带工具日志的外部检查（规范审查、编译、实机运行）确认结果后才算完成；交付完整性指交付的字节与赢得全部通过的候选完全一致，且每个声称的通过都能与工具调用日志交叉核对，无日志的自报通过一律降级为未检查。
这是全文的方法论核心，区别于自我反思、self-debug 等依赖模型自评的方案，也是理解算法 1 三条不变式的前提。
MCP（Model Context Protocol）
MCP 是给 LLM 智能体挂载外部工具的标准化协议。SemaPLC 把语法检查、编译、部署、运行状态与日志、变量读取与强制（force）、轨迹采样、脚本化行为检查封装进单一 PLC MCP 服务器，同时提供等价命令行接口，使任何经过标准 chat-completion 接口的模型都能驱动同一套验证设施。
工具层的模型无关性是论文声称 harness 是可靠性层而非某个骨干模型专属调优的证据基础。
研究动机
PLC 控制着工厂产线、电站和水处理设施，程序多用 IEC 61131-3 的 Structured Text（ST）编写。LLM 已经能为 PLC 生成独立的程序组织单元（POU），LLM4PLC、AutoPLC、Agents4PLC 等系统也分别引入了编译器反馈、厂商 IDE 调试和形式化验证。但生产环境还有两个更苛刻的要求：一是项目接地（project grounding），生成逻辑必须集成进已有工程，复用其功能块、变量、类型与接口，遵守构建、复位、初始化与安全约定；二是正确的运行时行为——即使编译与静态检查通过，程序仍可能配错定时器、走错状态转移、漏掉复位、破坏互锁或输出时序错误。然而现有系统的评测几乎都停留在独立 POU 粒度，运行行为只在少量测试或个例上被“演示”（demonstrated）而非“度量”（measured），没有任何跨方法、跨模型的统一评估能回答：生成的控制逻辑到底多可靠、能多大程度落入真实工程并跑对。
本文的目标是论文同时回答“怎么做”与“怎么量”。方法上，构建一个项目接地、验证门控的智能体框架 SemaPLC：生成以任务或项目上下文为锚点；规范审查、编译、实机运行三类外部验证结果被当作一等证据；智能体不允许凭自我判断终止，只有当带日志的外部检查确认后才算完成。度量上，建立两条互补评测轨道：功能轨道沿用 Agents4PLC 的 117 个独立 POU 任务，用任何方法都不可查询的隔离裁判按 $V_f \geq 0.80$ 的严格验证通过准则打分（非结论性与空生成一律计失败）；项目上下文轨道基于 Spec2Control 的 10 个工业厂区构造 65 个任务，要求生成逻辑在真实工程内编译并部署运行，分别报告集成编译 $C(P')$、静态行为 $S(P', R_p)$ 与动态行为 $D(P', T)$，使每一层的失败都保持可见。
与已有工作不同的是，作者的独特切入不是堆砌新工具，而是“完成纪律”：终止必须由带日志的外部验证结果背书，任何编辑都会作废此前全部判定，每个声称的通过都要与工具日志交叉核对——这提供了固定流水线不具备的交付完整性保证。另一独特点是把运行时验证从展示品提升为度量品：将候选与隐藏参考部署到同一实时 PLC 运行时，在最多 6 个场景下对比采样轨迹，给出黄金轨迹差分分数，并在基准规模上跨 7 个骨干模型、3 个已发表基线统一评测。由此得到一个反直觉的实证发现：静态评分被压缩到几分类似的方法（基线均值 71.7–75.7），动态行为却 sharply 分化（22.4–31.4 对 SemaPLC 52.2）——执行而非静态评分，才是控制逻辑是否真正可用的忠实检验。
核心方法
直觉上 SemaPLC 像“有外部监理的施工队”：模型可自由规划、生成和修改，但每个“通过”必须由外部检查签字，且一旦改动代码，旧签字全部作废。技术上，框架跑在通用事件驱动的工具使用核心上（不含 PLC 专用逻辑，经标准 chat-completion 接口访问），其上组织五个组件：规划/编辑/解释验证结果的智能体核心，项目与任务接地，PLC 技能库，多源验证流程，以及决定完成的验证门。所有组件通过共享的 PLC MCP 工具层操作环境，工具覆盖语法检查、编译、部署、运行日志、变量读取与强制、轨迹采样和脚本化行为检查。算法 1 形式化全流程：输入需求 $R$ 与上下文 $X$，先接地 $\Gamma \leftarrow \text{GROUND}(X)$、生成 $L \leftarrow \text{GENERATE}(R, \Gamma)$，在预算 $B$ 内对缺失判定的检查运行 RUNCHECK，$V$ 满足完成准则即交付 $(L, V)$；否则修复失败检查（重试 < $r=2$），且编辑后 $V \leftarrow \emptyset$ 作废旧判定。
核心创新是验证门控迭代（verification-gated iteration），由三条不变式治理：其一，有界重试：每项检查最多允许 $r=2$ 轮修复，防止无限循环；其二，编辑作废：任何代码修改都使此前全部判定失效、所有检查重跑，使判定精确绑定到字节级代码，杜绝“旧结论配新代码”；其三，凭据声明（earned claims）：每个结果是机器可读哨兵值并与工具调用日志交叉验证，未记录在日志中的自我声称一律降级为未检查（unchecked）。三者合成交付完整性保证：交付程序与赢得全部报告通过的候选逐字节一致，且没有任何自报通过能脱离工具日志存活。这区别于 LLM4PLC 的编译器反馈循环、AutoPLC 的厂商 IDE 调试和 Agents4PLC 的固定五智能体闭环——它们的停止时机由内部流程或自派生属性决定，而 SemaPLC 把终止权交给外部证据，门要求的不是完美分数而是与交付字节匹配的日志化外部证据。
方法步骤详情
流程按算法 1 展开。第 1 步接地与生成：GROUND 在项目轨道检索项目树、定位相关模块、复用已有变量与功能块接口、避免重定义既有接口并在有界范围内编辑（函数轨道退化为解析 POU 接口 $I_f$），随后 GENERATE 产出初始实现 $L$。第 2 步多源验证：规范审查逐条核对自然语言需求（具名设备/信号/发布变量、阈值边界、互锁/互斥/优先级不变式、扫描周期状态语义）；编译检查语法、类型、符号、接口与集成构建，只反馈首条诊断以保持修复局部化；实机运行验证则构建部署、初始化运行时、注入场景输入、采样外部变量，与需求派生的断言或黄金轨迹比对。第 3 步门控：带日志确认的判定写入 $V$，满足完成准则即接受。第 4 步修复循环：失败检查（重试 < 2）的首条诊断送回修复，编辑后作废全部旧判定并重跑所有检查；重试耗尽或预算 $B$ 用尽则报失败。失败阶段还指示修复目标：平直轨迹指向接线、变化但错误的轨迹指向块逻辑、迟到跳变指向定时器或边沿检测。
技术新颖性
技术新颖性有四点。一是完成纪律而非工具集合：贡献不在新工具，而在“终止需日志化外部验证 + 编辑作废旧判定 + 凭据与日志交叉核对”这一治理规则，形成固定流水线缺失的交付完整性保证。二是领域知识以文档而非代码承载：规则文件规定验证顺序、工具用法与扫描周期语义；策划的 wiki 记录 PLC 工程师从实践蒸馏的功能块签名、控制模式与编译器陷阱；程序化技能脚本化多步检查——这些产物只含通用 IEC 61131-3 与验证器语义，不含任何基准答案或任务特定属性，规避了数据污染质疑。三是统一 MCP 工具层使 harness 模型无关：bare 消融证明同一套设施让 7 个模型全部提升 8.5–33.3 个百分点，是可靠性层而非单一骨干的调优。四是评测基础设施设计：功能轨道对 Agents4PLC 有缺陷的 oracle 由 PLC 工程师审计修复了 43/117 个任务以保证公平；项目轨道的参考实现、黄金轨迹与断言 oracle 全程隐藏并做过泄漏审计（无逐字复制）。
实验结果
RQ1（功能轨道，117 任务，严格验证通过率）：SemaPLC 在 7 个骨干模型上全部最佳，均值 72.6%，比最强基线 Agents4PLC 的 63.9% 高 8.8 个百分点；GPT-5.5 上 82.1% 对 79.5%；最差模型 67.5% 仍超所有基线均值。bare 消融显示 harness 让每个模型提升 8.5–33.3 个百分点，离散度从 37.6 收窄到 14.6。RQ2（项目轨道，65 任务）：集成编译均值 89.4（基线 58.7–81.5），静态行为 81.6（基线 71.7–75.7），动态行为 52.2 对最强基线 AutoPLC 的 31.4——7 模型全胜且最低不低于 30，基线最差掉到 3.0。RQ3：三基线静态分仅差 4.0 而动态分差 9.0；静态到动态跌幅 SemaPLC 29.4 对基线 41.4–53.3；分层消融（DS-V4-Flash）显示动态分随规范/编译/运行层单调上升 23.1→30.3→43.7→54.1，成本 34k→129k token；含 TON 定时器的 174 条属性 100% 非结论性，凸显运行时验证不可替代。RQ4：功能轨道每任务 6.5 次请求（基线 6.3）、71 秒（基线 454 秒）；项目轨道 34.1 次请求（基线 6.9），动态优势以模型交互次数为代价。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 功能轨道：117 个独立 POU 任务（Agents4PLC 修复版） | 严格验证通过率（隔离裁判，7 模型均值，%） | SemaPLC 72.6（GPT-5.5 最高 82.1） | Agents4PLC 63.9（AutoPLC 62.4、LLM4PLC 30.2、bare 55.3） | +8.8 个百分点，7 个模型全部第一，最差模型（67.5）仍超所有基线均值 |
| 项目轨道：65 个任务，集成编译 | 集成工程 RuSTy 构建成功率（%，7 模型均值） | 89.4（GPT-5.5 100.0） | AutoPLC 81.5（最高基线；LLM4PLC 仅 58.7） | +7.9 个百分点 |
| 项目轨道：65 个任务，动态行为 | 黄金轨迹差分动态分 $D(P',T)$（0–100，7 模型均值） | 52.2（GPT-5.5 65.4） | AutoPLC 31.4（最高基线；Agents4PLC 30.3、LLM4PLC 22.4） | +20.8 分，7 个模型全部第一；最差 31.3 对基线最差 3.0–4.5 |
| 项目轨道：65 个任务，静态行为 | 断言 oracle 静态分 $S(P',R_p)$（0–100，7 模型均值） | 81.6（GLM-5.2 88.0） | LLM4PLC 75.7（最高基线） | +5.9 分，5/7 模型第一（GPT-5.5 上落后基线 84.1 对 88.8） |
| 验证层消融（DS-V4-Flash，65 任务） | 动态分 / 每任务 token 与请求数 | 满配 54.1 / 129k token / 47.8 次请求 | 仅生成 23.1 / 34k token / 8.9 次请求 | 动态 +31.0 分（编译层 +13.4、运行层 +10.4、规范层 +7.2） |
局限与改进
作者承认两条：动态评分只覆盖来自隐藏参考的有界场景集（每场景最多 6 个、每任务最多 6 场景），未见条件下的行为无法度量；在最强模型 GPT-5.5 上优势收窄——动态 65.4 对 Agents4PLC 的 63.6 仅差 1.8 分，静态行为 84.1 甚至低于基线最高 88.8，说明动态增益是“在模型不足处补足的可靠性”而非恒定优势。我还注意到：分层消融只在 DeepSeek-V4-Flash 单模型上进行，跨层结论的普适性未验证；运行轨迹是采样而非每扫描周期记录，瞬态事件只能靠持久断言近似，可能漏检短脉冲故障；静态 oracle 由子串存在性、必需调用、归一化数值常量等文本断言构成，理论上可能被形式正确但语义取巧的实现满足；黄金轨迹差分隐含假设隐藏参考本身完全正确，参考中的错误会系统性惩罚正确实现；项目轨道任务全部派生自 Spec2Control 的 10 个厂区，工程多样性受单一语料限制。
独立分析的弱点
第一，交互成本失衡：项目轨道每任务平均 34.1 次模型请求是基线（6.9）的近 5 倍，弱骨干最高 60.4 次，按 token 计费的生产场景成本压力大；改进方向是为高频检查引入规则化预筛，只在高价值决策点唤醒大模型。第二，运行时验证依赖真实 PLC 资源，构建-部署-执行使运行层最昂贵（129k token/任务），可引入高保真仿真器并行摊薄。第三，评分场景由隐藏参考派生、注入场景由需求自派生，两边只通过需求间接对齐——需求有歧义时可能系统性偏向同一种误读。第四，规范审查本质是 LLM 逐条核对清单，其查全/查准率未被单独度量，误报浪费预算、漏报放走缺陷。第五，形式化管道对定时器完全失效（0/174 结论性判定），时序构造上验证门只剩运行时一条腿，部署失败即计 0 分，存在单点依赖。第六，交付完整性依赖工具日志不可伪造，若模型能诱导工具层返回假哨兵值则整套门控失效。
未来方向
作者提出的方向是把该架构扩展为端到端 PLC 开发环境：编辑、生成与部署都由同一验证门治理，并把验证延伸到过程仿真以覆盖更广工况。基于本文成果还可延伸：其一，把 TON 定时器等跨扫描周期构造纳入可判定验证，例如定时器语义展开、或将运行时断言编译进 PLCverif 管道，补齐 0% 结论性覆盖的短板；其二，研究场景自动生成与覆盖度量（如变异测试驱动的场景补全、工况覆盖率估计），把“有界场景集”变成可量化的覆盖保证，回应未测行为这一局限；其三，技能库自动化——wiki 与规则文件目前由工程师人工提炼，可改造成从项目历史与修复日志中自动蒸馏，并研究跨项目迁移；其四，成本-可靠性帕累托优化：消融显示编译层单位动态收益最高（+13.4），可做检查的自适应排序与提前剪枝，压低 34.1 次请求的均值；其五，GPT-5.5 上优势收窄提示研究 harness 与模型能力的互补边界——哪些检查应外置为基础设施、哪些应内化为训练目标（例如以运行时反馈作为强化学习信号，让模型内化扫描周期语义）。
复现评估
代码已在 GitHub 开源（https://github.com/midea-ai/SemaPLC）。评测数据可复建：功能轨道基于公开的 Agents4PLC 基准（论文给出 43/117 缺陷任务的修复版），项目轨道派生自公开的 Spec2Control 语料（10 厂区、65 任务）并做过泄漏审计；但隐藏的参考实现、黄金轨迹与断言 oracle 是否随仓库发布未在正文说明，第三方完整复现评分管线可能受限。主要工程门槛在运行时验证：需要可部署的实时 PLC 运行时，配合 RuSTy 编译器与 PLCverif/nuXmv 裁判；纯功能轨道只需 LLM API 即可基本复现（每任务约 6.5 次请求、71 秒）。模型侧需接入 7 个骨干端点（MiniMax-M2.7/M3、Qwen3.5-Plus、DeepSeek-V4-Flash/Pro、GLM-5.2、GPT-5.5），项目轨道满配每任务约 34 次请求、129k token，全量评测的 API 开销中等偏大但个人可承受。总体：中等偏易复现——核心管道开源、基准公开，不确定性集中在私有评分工件与 PLC 运行时环境搭建。
论文图表
核心算法伪代码。输入需求 R、上下文 X、必需检查集 K 及完成准则、每检查重试上限 r、交互预算 B；输出带日志化验证结果 V 的实现 L 或失败。流程：接地 Γ←GROUND(X)、生成 L←GENERATE(R,Γ)；循环内对无有效判定的检查运行 RUNCHECK，日志条目确认才写入 V（否则 unchecked）；V 满足完成准则则交付；否则取失败且重试未尽的检查集 F，空则报失败；L'←REPAIR(L, 诊断)，L'≠L 时 V←∅（编辑作废）；预算耗尽报失败。
这是方法的精确形式化，三条不变式（有界重试 r=2、编辑作废、凭据声明）全部落在此伪代码中。第 5 行“日志确认才算 earned claim”与第 11 行“编辑清空 V”是交付完整性保证的技术落点，读懂它才能复现或改进该框架。