SemaPLC: A Project-Grounded, Verification-Gated Agent Harness for PLC Code Generation 精读

论文链接：SemaPLC: A Project-Grounded, Verification-Gated Agent Harness for PLC Code Generation 代码仓库：midea-ai/SemaPLC 发表时间：2026年8月20日（arXiv:2608.18565v1，标注日期2026-08-19） 机构：美的 AIRC + KUKA + 上海交通大学 + 浙江大学 领域标签：cs.SE / LLM代码生成 / 工业控制

机构合作说明：这是一份典型的"制造业龙头+机器人厂商+高校"产学研配置。美的 AIRC 是第一机构（一作严伦与两位通讯作者王华灿、徐毅均来自美的），定义了"真实工厂里代码必须集成进既有项目、必须跑得对"的工业口径——这是纯学术组很难给出的需求侧约束；KUKA 作为工业机器人厂商带来自动化产线的工程经验（共同通讯作者张辉）；上海交大、浙大 补齐方法学与评测的学术严谨性。通讯作者邮箱后缀（wanghc141@midea.com、hui.zhang9@kuka.com、xuyi42@midea.com）直接印证了这条企业主导的合作链。代码开源于 midea-ai 组织，工业需求 → 学术方法 → 开源落地的闭环完整。

一、论文背景

1.1 PLC 是什么：工厂里的"工业大脑"

可编程逻辑控制器（PLC）是驱动工厂流水线、电厂和水处理设施的工业计算机。它不跑通用操作系统，而以一种固定节拍循环执行控制程序：读输入 → 执行逻辑 → 写输出，每轮循环称为一个扫描周期。PLC 主要使用 IEC 61131-3 标准定义的编程语言，其中 Structured Text（ST，结构化文本） 是唯一的文本型语言——语法近似 Pascal，却在时间语义上与普通代码截然不同：TON 定时器要跨扫描周期累积计时、互锁条件必须在任何逻辑分支下不被破坏、复位时序错一个扫描周期就是产线事故。

这是全部理解的前提：PLC 代码是"时间敏感的状态机器"，不是"算完就结束的函数"。

1.2 LLM 生成 PLC 代码与生成普通代码有何不同

前序工作已证明 LLM 能生成独立的 PLC 程序组织单元（POU），并受益于编译、验证、执行等反馈。但论文一针见血地指出：生产环境中的控制逻辑极少是孤立 POU，部署施加了两个更高的要求：

• 项目接地：生成的逻辑必须集成进既有工程——复用它的模块与功能块、尊重它的变量/类型/接口、遵守它的构建/复位/初始化/安全约定。在一个有十年历史的车间项目里，你不能发明新变量名，必须像老工程师一样在既有框架里干活。
• 正确的运行时行为：即使程序集成了、编译了、过了静态检查，它仍可能配错定时器、走错状态转移、漏掉复位、破坏互锁、以错误时序驱动输出。编译通过 ≠ 跑得对——这些缺陷全部只在程序跑起来之后才暴露。

因此论文给出一个关键论断：集成编译、静态/形式化判定、动态运行时行为是同一程序的三种独立属性。 任何只测前两者的评测都在盲区里放行缺陷。

1.3 “演示过能跑"与"量化测过跑得多对"之间的空白

论文用一句话概括现有工作的局限：”Demonstrated, not measured（演示过，而非测过）"。此前的系统会执行生成代码来展示"它能跑"，但从不测量"它可靠地跑对的概率"。基准任务停留在独立 POU 或孤立需求，项目集成与运行时行为的报告依赖少量测试或个位数案例。没有任何统一评测回答过：跨方法、跨模型，生成的逻辑可靠地满足上述两个部署要求吗？ 论文用一个方法（验证门控的 harness）加一套测量（三层分开打分的基准规模评测）填这个空白。

二、论文定位和关联工作

2.1 LLM4PLC → AutoPLC → Agents4PLC 谱系

谱系读法：反馈信号从"编译器"到"厂商 IDE"到"模型检查器"逐步增强，但每一步都止步于"某个检查过了就交付"。SemaPLC 的区分点不在工具集合，而在完成的定义权——此前所有系统在某个检查后停止，SemaPLC 要求三层检查全部通过、且每个判定都有工具日志背书才准交付。

2.2 更广的关联工作

• Agentic 代码生成与修复：self-debugging / self-refine 用执行或批评反馈改进 LLM；工具使用 agent（ReAct）把推理与行动交织；MCP（Model Context Protocol）把工具服务标准化。SemaPLC 把这套实践移植到持续执行的、状态与时间敏感的 PLC 程序上——普通代码的运行时验证只看一次输出，PLC 的验证要看时间序列上的轨迹。
• 形式验证 vs 运行时验证：PLCverif 把 ST 和需求模式翻译成模型检查器输入（nuXmv 后端），对支持的形式化性质给出强保证。但 TON 定时器或大状态空间在实践中会产生 unsupported 或 inconclusive 结果——形式验证的能力边界恰恰是运行时验证的用武之地，两者互补而非替代。

定位结论：SemaPLC 是"完成纪律"层面的创新。它明说"新颖性不在工具集，而在统治工具的完成纪律：终止需要留档的外部验证结果、编辑使先前判定失效、每个声称的通过都与工具日志交叉核对——三者合力给出固定管线不具备的交付完整性保证"。这是把 agentic 工程实践（ReAct、MCP、self-debug）与工控领域"签字验收"传统融合的产物。

三、问题定义

论文用两条互补的轨道（complementary tracks，注意：是两种评测设置，不是一个任务的两个阶段）形式化了问题。

3.1 Function track：既有能力的公平锚点

给定需求 Rf 和局部接口 If，系统产出 POU：Lf = G(Rf, If)。一个held-out judge（任何方法都不可查询）编译 Lf 并模型检查由 Rf 导出的性质。以 Vf 为被验证满足的性质比例，主指标是：

VerifiedPass(Lf) = 𝟙[Vf ≥ 0.80]

阈值 0.80 沿用 Agents4PLC。两条严格的记分规则：模型检查既非满足也非违反（不支持构造、翻译失败、超时）的inconclusive 一律计为失败；生成失败留在分母里。编译率只是辅助完整性指标。

3.2 Project track：部署要求的可测量化

给定控制需求 Rp 和既有项目 P（功能块库、变量声明、接口、入口 harness、构建配置），系统产出新逻辑 Lp = G(Rp, P)，集成程序 P’ = P ⊕ Lp。这是项目接地的生成，不是从零综合整座工厂。 P’ 由三个独立指标打分，共用同一个 65 任务分母：

• 集成编译 C(P’) ∈ {0,1}：对集成程序做二进制 RuSTy 构建；
• 静态行为 S(P’,Rp) ∈ [0,100]：对程序文本做需求导出断言的确定性检查（子串出现/缺失、必需调用、规范化数值常量、结构引用、any-of 集合），不执行程序；
• 动态行为 D(P’,T) ∈ [0,100]：金迹差分——把 P’ 部署到 live runtime，在最多 6 个注入场景 T 下采样核心输出端口轨迹，与隐藏参考实现的轨迹精确对比（布尔与数值逐点精确匹配），D 为场景得分均值。

3.3 核心抽象：“完成的定义权"移交

两条轨道共享一个统一记号 (R, X, L)，也共享论文最核心的思想：把"任务完成"的判定权从模型的自我判断移交给外部验证证据。 基线系统在模型/编译器/自产属性说"够了"时停止；SemaPLC 只在留档的外部检查说"够了"时停止。

为什么动态金迹差分是三种属性中最忠实的？ 因为静态断言检查的是"程序文本长什么样”，编译检查的是"程序能不能构造"，而金迹差分检查的是"程序在时间维度上做了什么"。定时器配错、状态走岔、互锁被旁路、输出时序错——这些缺陷在文本层面可能完全合规，只有强制注入触发条件、观察输出端口随时间的演化才能暴露。D 是唯一直接观测"控制行为"的指标，其余两者都是它的代理。

四、问题解法

4.1 五组件架构

SemaPLC 跑在一个不含任何 PLC 专属逻辑的通用事件驱动工具使用核心（ReAct 式，chat-completion 接口）上，其上组织五个组件：

1. Agent 核心：规划、编辑、解释验证结果（算法 1 中的 GENERATE 与 REPAIR）；
2. 项目/任务接地：GROUND 步骤，输出接地上下文 Γ；
3. PLC 技能库（文档而非代码，见 4.3）；
4. 验证过程：规格审计、编译、live runtime 三源；
5. 验证门：按 Algorithm 1 决定完成。

所有组件通过共享的 PLC MCP 工具层作用于环境——单个工具服务器，MCP stdio 接口 + 等价 CLI 双暴露。工具覆盖：语法检查（plc_check，与评测同一编译器）、编译（plc_compile，行锚定结构化诊断）、I/O 映射提取（plc_detectIO）、上传部署（plc_upload）、一键构建运行（plc_buildAndRun）、启停/状态/日志、实时变量读取（plc_readVariables）与强制（plc_forceVariables，模拟外部信号注入）、轨迹采样（plc_trace）、逐扫描记录（plc_record）、原子"强制-期望-释放"检查（plc_verifyBehavior）、过程仿真场景构建（plc_buildSimulation）。这套工具谱系就是"把工业调试台变成 agent 的手"。

4.2 Algorithm 1 逐行精读：验证门控的生成循环

输入: 需求 R; 上下文 X (POU接口或项目); 检查集 K 及完成标准;
      每检查重试上限 r; 交互预算 B
输出: 实现L + 留档验证结果V, 或失败

1:  Γ ← GROUND(X); L ← GENERATE(R, Γ); V ← ∅     // 接地→生成→清空判定
2:  while 预算B未耗尽 do
3:    for all 无有效判定的检查 c ∈ K do
4:      (v, ec) ← RUNCHECK(c, L)                  // 规格审计/编译/运行时
5:      V[c] ← v if 日志项 ec 确认 v, else unchecked  // 【earned claims】
6:    end for
7:    if V 满足完成标准 then return (L, V)          // 接受
8:    F ← {c ∈ K | V[c] 失败 且 重试(c) < r}        // 可修复检查集
9:    if F = ∅ then return 失败 with V              // 无可修复检查
10:   L' ← REPAIR(L, {ec | c ∈ F})                 // 用失败日志修复
11:   if L' ≠ L then V ← ∅                          // 【edit invalidation】
12:   L ← L'
13: end while
14: return 失败 with V                              // 预算耗尽

三条不变量统治这个循环，我用工程语言翻译一下：

• Earned claims（挣得的声明 / 签字验收制）：第 5 行，每个检查结果是一个机器可读的哨兵值，必须与工具调用日志交叉验证——没有日志背书的"通过"一律降级为 unchecked。就像工程验收单上每个签字必须对应一份实测记录，口头说"我测过了"不算数。
• Edit invalidation（编辑作废 / 改动即复检）：第 11 行，任何修改使全部旧判定失效，所有检查重跑——判定附着于精确字节。焊过一个接点的电路板必须重新做全部绝缘测试，不能沿用上次的报告。
• Bounded retries（有界重试 / 返工上限）：每检查至多 r=2 轮修复（retries(c) 由 harness 维护），防死循环，超限如实报失败。

三者合成交付完整性保证（delivery-integrity guarantee）：交付的程序与赢得每个"通过"判定的候选在字节上完全同一，没有自报的通过能脱离工具日志存活。 附录 D 给出门控的三个具体条件：交付文件不含定位地址字面量（注入只属于测试副本）；交付字节哈希匹配最近一次成功编译（其输入清单含该文件）的输入；会话日志带有部署与强制输入证据。

4.3 项目接地与技能库：文档而非代码

项目轨道上 agent 检索项目结构、定位相关模块、复用既有变量与功能块、不重定义既有接口、在有界范围内编辑——保持项目约定而非重新生成整个项目。接地输出 Γ 在功能轨道退化为解析 POU 接口。

领域知识全部装在文档里，不含任何代码：规则文件（验证顺序、工具用法、扫描周期语义）；策展 wiki（PLC 工程师从工程实践中蒸馏的功能块签名、控制模式、编译器陷阱）；程序性技能（把多步检查脚本化，spec-review / fix-compile-error / benchmark-verify 三个技能，一层一个，明文禁止读取或猜测任何隐藏工件——验证性质、参考实现、录制轨迹都不许碰，评审只能对照自然语言需求）。技能库不含任何基准答案或任务特定性质——这是防"知识泄露"的干净设计。

规格审计按缺陷类别组织清单：合同提取→覆盖（需求点名的每个设备/信号是否有功能块实例、是否每扫描被调用、每个发布变量是否有驱动——专抓"编译通过但永远保持初值的死输出"）→边界纪律（每个阈值显式选择严格/非严格比较、显式处理 otherwise）→全局不变量→行为保真→扫描周期语义（区分跨扫描持久状态与每扫描重算状态、固定边沿检测更新顺序），收尾于六条领域公理（报警/互锁激活时执行器不得滞留危险态；互斥命令不得同真；传感器故障时控制器不得继续调节；故障或复位后必须保持失效安全方向；工程值必须在标定范围内；普通逻辑不得绕过许可条件）。每项要么通过、要么给出具体修订。

编译反馈有个细节：只回传首个诊断，让修复保持局部、避免级联重写。

4.4 Live Runtime 验证：金迹差分怎么做

运行时验证五步：构建并部署实现 → 初始化 runtime → 注入场景输入 → 采样外部变量 → 对比。对比对象是需求导出的运行时断言，或存在可信录制时的金迹（golden trace）。失败分期指示修复靶点：平直轨迹指向接线、变化但错误的轨迹指向块逻辑、迟到的转移指向定时器或边沿检测器——诊断信号本身就是修复的定位器。

关键的评测隔离设计（附录 E 的 Table S4 值得细读）：agent 注入的场景自己从任务规格推导；打分场景与金迹从隐藏参考独立推导，绝不暴露。两套场景可以经由共享的需求而对齐，但 agent 无法访问任何打分工件。因此动态分测量的是"基准场景下的行为"而非"未见工况的泛化"——论文把这条边界画得很诚实。

4.5 案例全流程：焦化炼厂 Section 8 任务

Figure 2 的案例是理解整个循环的最佳标本。需求把同一个设定点绑给两个竞争条件：

• 低流量（F T-701 < 50 kg/hr）⇒ SlaveSP = 500
• 变送器故障 ⇒ SlaveSP = 2500

四个方法四种死法：

注意：两个编译通过的候选全都死在优先级上，缺陷在"竞争条件下的输出选择"，语法和接口层完全看不见。 SemaPLC 的运行时验证强制注入 F T-701 = 30 kg/hr，期望 SlaveSP=500、实测 2500——具体错值被暴露。失败分期把修复定位到"按成因选择输出"：IF Fault_Active THEN ManOut := 2500.0; ELSE ManOut := 500.0; END_IF。重新验证后两个异常情形均通过，交付。

这个案例浓缩了论文的全部主张：只有运行时强制注入触发条件，优先级覆盖类缺陷才暴露；只有门控循环，暴露的缺陷才在交付前被修复。

五、评估指标与实验证据

设置速览：7 个骨干模型横跨 5 家厂商两个能力档（MiniMax-M2.7/M3、Qwen3.5-Plus、DeepSeek-V4-Flash/Pro、GLM-5.2、GPT-5.5），所有方法调同一模型端点。基线为 LLM4PLC、AutoPLC（从其发布框架运行）、Agents4PLC（忠实重实现、自产性质、judge 性质保持隐藏），各自按发表版迭代预算运行。bare 配置在同一循环上剥掉 harness（无技能无工具），量化 harness 整体贡献。

5.1 RQ1：Function track——严格通过率（Table 1，分母 117）

五个要点：

1. 全部 7 个模型最高严格通过率，含最强的 GPT-5.5（82.1% vs 79.5%）；均值 72.6% 超最强基线 Agents4PLC（63.9%）8.8 个百分点。
2. 最差模型 67.5% 仍超所有基线的均值；分数跨度仅 14.6 点，基线跨度 25-31 点。
3. Harness 效应：bare→full 每模型 +8.5~33.3 点，弱模型受益最大（MiniMax-M2.7 +29.9、DS-V4-Flash +33.3）；跨模型带宽从 bare 的 37.6 点收窄到 14.6 点；bare 编译率均值 85.5% 升到 99.2%。harness 是模型无关的可靠性层，不是针对某个骨干调的提示词。
4. 为什么比较是公平的：held-out judge（任何方法不可查询，Agents4PLC 重实现自产性质所以判定性质保持隐藏）+ 工程师三轮审计修复了 Agents4PLC oracle 中 43/117 任务的缺陷性质（五类缺陷：错误常量/极性、恒真断言、与设计矛盾的性质、虚构阈值、复制粘贴重复；两轮独立确认才修，无据性质直接删除而非编造阈值替代）+ 所有方法在同一修复数据上评测。
5. bare vs full 混合了陈述性知识与验证循环，论文诚实地把增益归因于 harness 整体，循环的分解留给 RQ3。

5.2 RQ2：Project track——三层证据（Table 2，分母 65）

各方法跨 7 模型的 Worst / Best / Mean 汇总：

• 编译：89.4% vs 基线 58.7-81.5。
• 静态：7 个模型中 5 个领先，均值 81.6 vs 71.7-75.7——静态层各方法其实挤在 4 分之内。
• 动态：决定性差异。均值 52.2 vs 基线最高 31.4（AutoPLC）；全部 7 模型最佳；从不低于 30，而固定管线在最差模型上跌到个位数（Worst 列：3.0 / 4.0 / 4.5）。
• 诚实的边界：优势随模型变强而收窄——GPT-5.5 上动态仅领先 Agents4PLC 1.8 点（65.4 vs 63.6），静态甚至落后（84.1 vs 最高 88.8）。harness 提供的是模型自身不足处的可靠性，不是随前沿移动的固定增益。

5.3 RQ3：跨层验证——静态相近、动态悬殊

三条证据链：

（1）静态层压缩、动态层分离。 三个基线静态均值挤在 71.7-75.7（4 分内），动态却从 22.4 铺到 31.4；SemaPLC 拿到 81.6 静态 / 52.2 动态。相似静态分不蕴含相似动态行为——运行时层把静态打分压缩的方法分离、甚至重新排序。 SemaPLC 的静态→动态落差也最小（29.4 vs 基线 41.4-53.3；论文注明两分测量不同属性，落差不是逐点可靠性损失）。即便最强方法动态分仍远低于静态分：运行时 PLC 生成远未解决。

（2）层消融（Table 3，DS-V4-Flash，65 任务，逐层累加）：

动态分单调上升：编译层单项动态增益最大（+13.4，因为建不起来的程序运行时计 0），运行时层次之（+10.4，此时编译已饱和）；静态分移动很少（71.5→78.0）。成本随层攀升（34k→129k token、8.9→47.8 请求），运行时验证（构建+部署+执行）最贵。决定性的动态可靠性来自 agent 被门控在其上的检查，不来自生成本身。（注明：单模型消融。）

（3）3590 项场景-端口值检查的分解（Table 4）：not built/run 类结构性失败从 74.7% 降到 21.5%，full harness 只留 3.3% 检查未能构建；这 53 点迁移分成"变正确"（23.1%→54.1%）和"变得可测的错误值"（2.1%→24.4%）——错误值上升是覆盖扩张的副产品而非退化：检查先要能跑才可能错，观察到的错值正是运行时反馈要修的东西。残余错值集中在极限违限场景（breach 17.3% vs normal 7.1%）。

（4）形式覆盖 motivate 运行时验证（Table 5）：1293 个交付程序汇总，无 REAL/定时器组 75.7% 结论性、含 REAL 组 87.0%、含 TON 定时器组 0.0%——32 个含定时器程序上的 174 条性质无一得到结论性判定，不支持模式与翻译失败主导。定时器并非原则上不可验证，而是此管线中跨扫描周期的有状态时序构造落在结论性覆盖之外——这恰是运行时验证直接锻炼的东西。

5.4 RQ4：交互成本（Table 6，对比最强基线）

功能轨道上请求数相当（6.5 vs 6.3）——增益不来自更多请求；墙钟反而更低（71s vs 454s），因为 Agents4PLC 每次迭代都调 PLCverif+nuXmv 模型检查、主导其墙钟。项目轨道墙钟相当（347 vs 344s）但请求数是 5 倍（34.1 vs 6.9）——动态领先是用模型交互买来的。架构性差异：Agents4PLC 固定多 agent 工作流有界迭代、请求近乎恒定（6.8-7.0）；SemaPLC 开放循环里每个工具调用都是模型决策，门控让它交互到检查通过为止，请求随骨干浮动（16.4-60.4）。

六、效果优势的根源解释

把证据串成因果链，才能理解 SemaPLC 为什么赢、以及为什么只在某些地方赢得多。

根因：各循环在哪个检查后停止交付。 基线在编译器和（至多）自产性质满足后交付——此时规格错配与语义错误（优先级、时序）尚未被任何检查触碰，缺陷流出循环、交给下游（或评测）承担。SemaPLC 把完成权交给外部证据且编辑作废一切旧判定，规格审计在交付前逐条款对照需求、运行时验证强制注入触发条件观察真实轨迹——同样的缺陷在循环内暴露、在循环内修复，而非交付后返工。 差值就是 Table 1/2 里那 8.8 与 20.8 点。

为什么动态层差距最大（52.2 vs 31.4）而静态层只差 4-6 分？ 机制根源在于两层检查的对象不同：静态断言检查程序文本（子串、常量、调用结构）——LLM 生成"看起来合规"的文本本来就是强项，各方法都被拉到 70+ 的窄带里；金迹差分检查时间维度的行为——状态如何演化、定时器何时到点、输出何时翻转。优先级覆盖类缺陷（案例中 500 覆盖 2500）在文本层完全合法，只有强制注入触发条件、观察端口轨迹才能暴露。静态层测的是模型的语言模仿力，动态层测的是 harness 的行为约束力——SemaPLC 的优势成分恰好只作用于后者，所以动态层分离最狠。

为什么弱模型受益最大（+33.3 vs +8.5）、带宽从 37.6 收窄到 14.6？ 因为三类检查全部外置于模型：模型不必自己知道扫描周期语义、不必自己记得查互锁——外部工具替它查、查不过就打回。强模型（GPT-5.5 bare 已 71.8）自身已内化大量此类纪律，harness 的边际贡献小；弱模型（DS-V4-Flash bare 34.2）缺的正是这些，外部检查全额补上。harness 是"外部验证对模型能力的补偿器"——补偿量自然是缺口越大越大。

诚实的收窄：GPT-5.5 上动态领先只剩 1.8 点（65.4 vs 63.6）。 这不是 harness 失效，而是其价值结构使然：它提供的是"模型自身不足处的可靠性"，不是恒定增益。模型越强、自身不足越少、可补的缺口越窄。论文把这层写得很明白——这也预示了这条路线的天花板形态：当模型内化了验证纪律，harness 的增益趋近于零，剩下的是保险而非提升。

七、必要知识反推

要从这篇论文快速入门，需要补的知识可以分三层。

领域层（工控）：IEC 61131-3 标准与其五种编程语言（重点是 ST）；扫描周期执行模型（读输入→执行→写输出的固定节拍，理解一切时序问题的地基）；TON 定时器语义（跨扫描累积计时——形式验证的边界物种）；互锁与优先级（工业安全的底线机制：互斥命令不得同真、报警时执行器不得滞留危险态、失效安全方向）。不掌握"状态跨扫描持久 vs 每扫描重算"这对区分，就理解不了规格审计清单为何那样设计。

方法论层（agent 工程）：agent harness 概念（模型之外的脚手架：工具管理、上下文构建、控制流、失败恢复——SemaPLC 是"harness 的完成纪律决定交付质量"的又一实证）；编译器在环修复（LLM4PLC 开创，self-debugging 谱系在工控的落地）；模型检查能力边界（PLCverif/nuXmv 对 TON/大状态空间会 unsupported/inconclusive——形式保证的适用域）；金迹差分测试思想（golden-trace differential，轨迹级对比是时序系统最忠实的行为检验）；MCP 协议（工具服务标准化，SemaPLC 单服务器双暴露 MCP+CLI 的设计值得抄）。

工程层（工具链）：RuSTy（PLC-lang 项目的 ST 解析器与 LLVM 前端——评测与 harness 用同一编译器，保证"练习即考试"）；PLCverif 工具链（ST+需求模式→模型检查器输入的翻译）；Spec2Control 语料（十个工业工厂叙事→ST 项目，65 任务的来源，其 130 个空函数块体构成任务面）；OpenPLC runtime（部署与变量强制的目标环境）。

融合节点：这篇论文真正的知识结构是把"LLM agent 工程实践"（ReAct 工具循环、MCP、self-debug）移植到"时序敏感的工控验证传统"（签字验收、复检制度、失效安全）——把 verification gate 当作第一公民是两个领域此前都没想到要合并的接口。Sema Code（同团队前作，把 AI 编码 agent 解耦为可编程嵌入基建）是其直接技术底座。

八、通用性灵感

这篇论文的价值远超 PLC 领域——它验证了四条可迁移的工程原则。

① 完成权外部化：agent 不许自判完成。 “模型认为够了"是最危险的停止条件——模型的自我评估与其真实正确性之间隔着编译、集成、运行时三道鸿沟。SemaPLC 用"留档外部检查"替换"自我判断”，效果是全部 7 个模型的严格通过率同时抬升。推广：任何自动生成系统的验收（文档生成、数据分析、测试生成）都该问一句——“完成"的判定者是谁？AI 编程工具的"完成"定义若只是模型不再输出 diff，那就还是 bare 配置。

② 编辑即作废：任何改动使全部旧判定失效。 这条不变量看似浪费（改一行重跑全部检查），实则是交付完整性的唯一保证——判定附着于精确字节，改后的程序与改前的通过判定在逻辑上毫无关系。SemaPLC 的交付保证（“交付字节 = 赢得判定的字节”）完全依赖它。推广：CI/CD（任何 commit 触发全量而非增量流水线的地方）、合规审计（文件修订后旧审计结论自动失效）、科研代码复现（“此结果对应此 commit 哈希”）。反例俯拾皆是：增量验证省下的时间，最后都变成了"哪个判定对应哪个版本"的考古成本。

③ 三层证据金字塔：规格 → 编译 → 运行时，缺一不可。 三层各自拦截不同缺陷类：规格审计抓"编译器接受但需求禁止”、编译抓构造失败、运行时抓时序与状态错误。层消融显示每层都有不可替代的独立贡献（动态 23.1→30.3→43.7→54.1 单调上升）。推广：代码评审（风格 → 类型/构建 → 测试三层金字塔同构）、自动驾驶验证（法规符合 → 仿真构建 → 封闭场地实测）、医疗 AI（指南符合 → 集成测试 → 临床影子部署）。关键教训：任何一层单独看都会制造"看起来可靠"的幻觉，Table 2 里静态 74 分的方法动态只有 22 分。

④ 静态相近动态悬殊：评测必须下探到执行层。 这是论文最有分量的实证发现——静态分挤在 4 分内的方法，动态分从 22 铺到 31、再到 52；运行时层甚至重新排序静态层压缩的方法。任何"看起来对"与"跑起来对"可能背离的领域（时序系统、有状态服务、并发程序、具身控制），评测止步于静态/形式层就无法区分可靠与不可靠的方法。推广：评测集设计的通用原则——最难测的层（执行/部署/时间维度）往往是最有分辨力的层，也是被跳过的层。

⑤ 跨模型带宽收窄 = 可靠性层而非提示工程。 bare 带宽 37.6 点 → full 14.6 点，弱模型 +33.3、强模型 +8.5。harness 的贡献形态是"把最差的情况拉起来"而非"把最好的情况推更高"——这是可靠性工程的签名特征（对比提示工程：针对单模型调优、换模型即失效）。推广：“弱模型 + 强验证"是一条被低估的工程路线——当验证可以外置时，模型能力的边际价值递减，验证完备性的边际价值递增。选型含义：预算有限时，先投资验证基建还是先买最强模型？SemaPLC 的数据说——DS-V4-Flash + full harness（67.5）吊打 GPT-5.5 + 最好基线（79.5? 不，吊打的是所有基线均值）且成本结构完全不同。当你的 harness 能把最弱模型的下限抬到 67，模型选型就从"能力问题"变成了"成本问题”。

结语

SemaPLC 讲了一个"纪律胜过天赋"的故事：全部由常规工具组装（编译器、模型检查器、runtime、MCP），没有任何新算法，仅靠一条铁律——agent 不许凭自判断宣布完成，只有工具日志确认的三层检查过关才准交付，任何编辑作废一切旧判定——就在 7 个模型上拿到了全面最高的严格通过率，并把动态行为分从基线最高 31.4 抬到 52.2。

它留给社区的两份遗产同样重要：一份是方法（验证门控 harness，开源可复用）；另一份是测量（把"集成编译/静态/动态"三层分开打分的评测协议）——后者揭示的"静态相近、动态悬殊"现象，适用于一切时序敏感的生成任务。而它诚实录下的"GPT-5.5 上领先收窄到 1.8"则标定了这条路线的本质：harness 提供的是模型自身不足处的可靠性，不是随前沿前进的固定增益。 当模型足够强时，验证门控从"提升器"退化为"保险丝"——但工业场景恰恰是保险丝比提升器更值钱的地方。