一句话总结

来自美的AIRC、KUKA、上海交通大学和浙江大学的研究者提出SemaPLC，一个面向PLC代码生成的项目接地、验证门控agent工具框架，该框架采用严格的完成规则，要求确认的规格、编译和实时运行时检查均通过后方可完成，在117个独立POU任务上实现72.6%的平均严格通过率，并将基线模型的动态行为得分从22.4至31.4提升到SemaPLC的52.2。

核心贡献

• SEMAPLC是一个面向PLC代码生成的验证门控agent工具框架，将生成过程锚定在现有任务或项目中，仅当规格检查、编译检查和实时运行时行为检查的记录均确认结果无误后，才声明完成。
• 提出一个包含65个任务的项目上下文评估轨道，通过在实时PLC运行时上进行集成编译、基于静态断言的的行为检查和动态黄金轨迹比对来评分，生成逻辑与参考逻辑均在场景输入下执行。
• 在七个骨干模型上，SEMAPLC在117个任务函数轨道上取得最高的严格验证通过率，平均值为72.6%，最佳平均集成编译得分为89.4，最佳动态行为得分为52.2，而基线方法最高仅为31.4。结果表明，相似的静态得分可能掩盖显著不同的运行时行为，因此需要实时执行才能区分可靠方法。

引言

可编程逻辑控制器(PLC)运行着工厂产线、发电厂和水处理设施，通常使用IEC 61131-3标准中的结构化文本进行编程。此前的研究表明，大语言模型可以生成独立的PLC程序组织单元，并通过编译器、形式化验证和执行反馈进行改进，但生产逻辑还必须集成到现有项目中，并在运行时正确运行。早期系统通常仅证明生成的代码在有限场景下可以运行，而非大规模衡量运行时可靠性，其基准测试也主要关注独立单元或孤立需求。作者提出了SEMAPLC，一个验证门控agent工具框架，将生成过程锚定在目标项目中，并要求在完成前记录编译、规格和实时运行时检查，同时提出双轨评估体系，分别对集成编译、静态行为和动态行为进行评分。

数据集

作者使用两个任务集进行评估。

函数轨道

• 构成：来自Agents4PLC基准的117个独立POU任务。
• 修复与过滤：已发布的oracle包含导致正确实现无法通过的缺陷验证属性和任务描述。PLC工程师审计并修复了117个受影响任务中的43个。
• 使用方式：所有方法均在相同的修复后数据上进行评估。

项目上下文轨道

• 构成：来自Spec2Control的65个任务，基于十个工业对象，经过审查的控制叙述被转换为IEC 61131-3 ST项目。
• 任务模式：每个任务针对一个对象工段，提供工段叙述、函数块接口目录与库，以及一个空的入口框架。生成的逻辑必须能够编译并部署到完整项目中。
• 防泄漏控制：参考实现、运行时轨迹和原始答案均保持隐藏。泄漏审计未发现逐字复制。

处理与数据使用

• 摘录未说明训练划分、混合比例、裁剪策略或元数据构建细节。
• 数据集用作评估基准：函数轨道中为修复后的任务，项目上下文轨道中为隐藏参考的项目级任务。

方法

作者在两条轨道上形式化PLC代码生成任务：函数轨道上，系统在给定需求(R_f)和局部接口(I_f)的情况下生成程序组织单元(POU)(L_f = G(R_f, I_f))；项目上下文轨道上，系统生成集成到现有项目(P)中的新逻辑(L_p = G(R_p, P))。为了实施该任务，作者提出了SemaPLC agent工具框架，接受自然语言控制需求(R)和任务上下文(X)。

该工具框架构建在一个通用的事件驱动工具使用核心之上，该核心不包含任何PLC特定逻辑。在该核心之上，系统组织了五个关键组件：用于规划和编辑的agent核心、项目与任务接地、PLC技能库、验证流程以及验证门控。

如框架图所示，agent核心通过共享的PLC MCP工具层执行操作，该工具层提供语法检查、编译、部署、运行时状态、实时变量读取、轨迹采样和脚本化行为检查等工具。工具框架接受控制需求和上下文，使agent核心能够规划、生成、编辑和修复逻辑。来自规格检查、编译和实时运行时验证的外部验证结果被送入验证门控，仅当满足轨道特定的完成标准时，验证门控才接受实现。失败的检查会在剩余重试次数和预算允许的情况下，生成诊断反馈用于修复迭代。

在项目接地方面，agent在项目轨道上检索项目结构并定位相关模块。它复用现有变量和函数块，避免重新定义已有接口，并保持项目约定。领域知识封装在文档中而非代码中，包括用于验证顺序和扫描周期语义的规则文件、用于函数块签名和控制模式的管理wiki，以及用于多步骤检查的流程技能。

作者采用多源验证方法。规格结果来自结构化需求审计，逐条比对候选实现与自然语言需求，覆盖设备、信号、阈值和联锁。编译结果检查语法、类型、符号和接口，返回首个诊断信息以保持修复的局部性。实时运行时验证构建并部署实现，初始化运行时，注入场景输入，并对外部变量进行采样。它将观察到的行为与运行时断言或黄金轨迹进行比较。不匹配和执行失败均成为诊断反馈，指向特定失败阶段，例如接线、块逻辑或定时器行为。

验证门控的迭代循环受三项不变式约束，以确保交付的完整性。第一，有界重试将每项检查限制为至多(r = 2)轮修复。第二，编辑失效确保任何修改都会使所有先前判定失效，要求每项检查重新运行，使判定绑定到确切的字节内容。第三，应得声明要求每个结果都是机器可读的哨兵值，并与工具调用日志交叉验证，任何未记录的声明都会被降级为未检查。三项不变式共同保证交付的程序与获得每项报告通过结果的候选程序完全一致。

实验

研究在七个骨干模型上，将SEMAPLC与三个既有基线在函数级和项目接地的PLC生成任务中进行评估。函数级结果表明，该工具框架提升了每个模型的严格正确性，并作为模型无关的可靠性层发挥作用；项目级结果则显示动态运行时行为提升最大，尽管在最强模型上的优势有所收窄。验证层分析表明，实时运行时验证是最具区分度的检查，每增加一个验证层都能将原本不可运行的检查转化为可衡量和可修复的行为。主要的权衡在于交互成本，因为可靠性提升来自额外的模型驱动验证和执行循环，而非仅来自生成环节。

完整的SEMAPLC工具框架在所有列出的模型上取得最高的严格验证通过率，且平均领先最强基线。比较裸配置和完整配置显示，该工具框架提升了每个骨干模型，对较弱模型的提升最大，且得分分布明显收窄。改进来自编译之外的检查，尤其是规格审计和实时运行时验证，它们在交付前捕获语义不匹配。SEMAPLC完整版在所示每个模型上均录得最高严格通过率，大幅优于所有基线。每个模型从裸配置到完整配置均有提升，最弱的骨干模型获益最大，同时跨模型差异缩小。裸配置到完整配置的提升归因于工具框架的验证循环，尤其是规格和运行时检查，它们在交付前修复语义错误。

在项目上下文轨道上，SEMAPLC在集成编译、静态行为和实时动态行为方面均领先基线，其中动态性能优势最为显著。运行时层最具区分度：基线在静态得分上相近，但在动态得分上差异明显，且远低于SEMAPLC。SEMAPLC也表现出最小的静态到动态降幅，尽管各方法的动态得分均显著低于其静态得分。SEMAPLC在比较方法中取得最高的平均集成编译率和最高的平均静态得分。动态行为是最具区分度的层，基线静态得分紧密聚集，但动态得分分散且远落后于SEMAPLC。SEMAPLC的动态得分从未低于30，而基线方法在最差模型上跌至个位数，并且SEMAPLC的静态到动态降幅最小。

累计增加验证层可将动态得分从23.1提升至54.1，而静态得分仅从71.5升至78.0。编译提供最大的单项动态增益，其次是运行时验证，但每一层都会增加token和请求成本，其中运行时验证是最昂贵的步骤。随着规格、编译和运行时检查的逐步增加，动态性能单调改善，而静态性能仅小幅变化。token和请求成本随着每一个验证层的增加而上升，完整运行时验证是最昂贵的阶段。

增加规格、编译和运行时检查可逐步提高正确结果比例，并减少结构性失败。由于更多检查变得可运行，错误值结果也随之增加，尤其是在限值突破场景中，这反映了覆盖范围的扩大而非性能退化。随着累计层次增加，正确结果从23.1%上升至54.1%，而结构性失败从74.7%降至21.5%。一旦运行时检查启用，错误值结果集中在更困难的限值突破条件下，达到17.3%，而正常运行条件下为7.1%。

对于交付的不使用定时器的程序，形式化验证覆盖率较高，涉及REAL结构的程序取得最高的定性判定率。含定时器的程序是明显缺口：在此流程中，这些程序的任何属性均未获得定性判定。这使得有状态时序行为不在形式化覆盖范围内，并促使采用直接运行时验证。不含REAL或定时器结构的程序大多呈现可定性判定的形式化覆盖率，含REAL结构的程序定性判定占比更高。含定时器的程序没有可定性判定的验证结果，所有与定时器相关的属性均保持未定性状态。形式化流程可处理许多非定时器场景，但无法对跨扫描周期的时序结构得出定性判定。

实验通过严格通过率比较、项目上下文集成与动态行为基准、累计验证层消融、结果分析以及形式化覆盖评估来评价SEMAPLC。完整工具框架提升了每个骨干模型，对较弱模型的提升最大，并在最具区分度的动态运行时行为上最为领先。增加规格、编译和运行时检查将正确的动态结果从23.1%提升到54.1%，主要是通过将结构性失败转化为可运行场景来实现的，尽管运行时验证是最昂贵的步骤。形式化验证可对许多非定时器和REAL程序得出定性判定，但对含定时器的结构保持未定性状态，这促使采用直接运行时验证。