⚡ electrical engineering

NeuroSymbolic Robustness Analysis for Discrete Systems with Respect to Transition Deviations

本文提出了一种神经符号框架，该框架结合了用于推断可行转移偏差的大语言模型与用于计算离散事件系统鲁棒性保证的符号分析，有效地解决了现有方法的扩展性和保守性限制问题。

原作者： Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

发布于 2026-06-03

📖 1 分钟阅读☕ 轻松阅读

原作者： Shih-Jie Shih, Jonghan Lim, Ilya Kovalenko, Rômulo Meira-Góes

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在为一个繁忙的交叉路口构建一个极其严格的交通控制器。你编写了一本完美的规则手册（“监督者”），它精确地告诉车辆何时停止、何时通行，从而确保不会发生事故。如果车辆和道路的行为完全符合你在蓝图上的设计，这本规则手册将完美运行。

但在现实世界中，情况并不总是按照蓝图进行。汽车可能会熄火，传感器可能会出现故障，或者驾驶员可能会犯错。在工程术语中，这些被称为“偏差”（deviations）。如果你的规则手册没有考虑到这些现实世界的故障，你的交通控制器可能会失效，从而导致事故发生。

问题所在：“如果……会怎样”太多了

工程师们曾尝试通过询问：“如果汽车做出了任何不同于蓝图的行为，会发生什么？”来解决这个问题。

问题在于，这种“任何不同的行为”的情景数量是天文数字般的。这就像试图检查整个宇宙中所有可能的汽车故障方式一样。

速度太慢： 检查每一种可能性需要消耗如此巨大的计算能力，以至于除了最简单的系统外，其他系统都无法实现。
过于荒谬： 许多这些“如果……会怎样”的情景在物理上是不可能的。例如，蓝图可能说一辆车可以突然瞬间移动到马路的另一边。虽然这在计算机模型中在数学上是可能的，但在现实生活中在物理上是不可能的。检查这些荒谬的情景既浪费时间又会混淆结果。

解决方案：“神经符号”联手

本文提出了一种聪明的联手方式，将两种类型的人工智能结合起来以解决这些问题。你可以将其想象为雇佣了一名创意侦探和一名严谨会计师共同工作。

1. 创意侦探（“神经”部分）

首先，团队使用了一个大语言模型（LLM）——即那种可以写故事或回答问题的 AI。

它的作用： 这个 AI 阅读工程蓝图以及关于系统“应该如何”工作的自然语言描述（例如，“汽车不能瞬间移动”、“机器不能在零件到达前进行加工”）。
类比： 想象这个 AI 是一名侦探，它看着蓝图并说道：“好吧，我知道这台机器。它不可能凭空变出零件。这违反了物理定律。因此，我会忽略这种不可能的情景。”
结果： AI 过滤掉了这些不可能的故障，并为团队提供了一份简短且现实的可能出错清单。

2. 严谨会计师（“符号”部分）

一旦创意侦探提供了这份简短且现实的故障清单，严谨会计师就会接管工作。

它的作用： 这个部分使用传统的、基于数学逻辑的方法（符号推理），针对那份简短的清单对系统进行严格测试。
类比： 会计师不靠猜测，而是进行数据计算。他们会检查：“如果机器像这样卡住，交通控制器是否仍能确保每个人的安全？”
结果： 由于清单很短且具有现实意义，会计师可以快速完成任务，并给出数学上完美的安全性保证。

实际应用中的运作方式

研究人员在三个现实场景中测试了这个“侦探 + 会计师”团队：

工厂机器： 检查如果零件到达过快或被卡住，存储箱是否会溢出。
Therac-25（医疗设备）： 一个著名的历史案例，其中一台放射治疗机由于设计缺陷导致了事故。他们检查了安全规则是否能处理操作员按键过快或选择了错误的模式。
通信协议： 检查消息系统是否能够处理丢失或重复的数据包而不崩溃。

研究结果

研究发现，这种新方法是一个巨大的进步：

它减少了噪音： 在某些情况下，AI 成功过滤掉了超过 90% 的“荒谬、不可能”的情景。
它保持了安全性： 尽管检查的情景较少，但他们发现的安全性保证与检查了“每一个”可能情景后的强度是一样的。
它更快： 通过忽略那些不可能的故障，计算机不需要承受那么重的负担就能找到答案。

总结

本文介绍了一种让机器安全检查变得更聪明的方法。与其预测所有可能发生的事情（包括不可能的魔术表演），它利用 AI 来确定现实世界中“实际”可能发生什么，然后使用严格的数学来证明系统针对这些特定且现实的风险是安全的。这就像是在检查一座桥梁是否存在锈迹和裂缝，而不是担心它会被陨石击中。

技术摘要：针对离散系统转换偏差的神经符号鲁棒性分析

问题陈述

在离散事件系统（DES）的监督控制中，控制器被合成以强制执行对受控对象模型的规范。虽然经典方法提供了“正确性构建”（correct-by-construction）的保证，但这些保证严格依赖于受控对象模型的准确性。在实践中，由未建模动力学、传感器噪声或抽象误差引起的失配会导致实际系统偏离标称模型，从而可能危及安全性。

近期的研究通过定义离散鲁棒性来解决这一问题，即定义了在维持安全性的前提下，监督器所能承受的所有可能转换偏差（即在标称受控对象中增加的额外转换）的集合。然而，这种基于转换的方法面临两个关键局限性：

可扩展性： 可能的偏差空间随状态和动作空间的增加呈指数级增长，使得对于除了极小规模系统之外的所有系统，进行穷举枚举在计算上都是不可行的。
保守性： 大多数在数学上可能的偏差在物理上是不可行的（例如，机器在没有输入的情况下自发输出零件）。包含这些不可行的偏差会夸大搜索空间，并产生不能准确反映现实世界系统行为的鲁棒性结果。

现有的尝试通过使用形式化系统约束（ $P_{sys}$ ）来过滤不可行偏差的方法，需要领域专家将物理定律手动编码进形式化规范中，这增加了负担并提高了分析流程的开销。

方法论

本文提出了一种神经符号计算框架来解决这些可扩展性和可行性挑战。该方法将物理可行性的推理与鲁棒性保证的形式化计算解耦，利用一个两阶段过程：

1. 神经可行性过滤（LLM 层）

第一阶段利用大语言模型（LLM）来推断物理上可行的偏差转换子集（ $D$ ）。

输入： 框架摄取受控对象和监督者的形式化 LTS 模型、系统状态和事件的自然语言描述、安全规范以及关于物理定律的领域知识（例如，“一个零件不能同时出现在两个地方”）。
过程： 使用结构化提示模板引导 LLM 对这些输入进行推理。LLM 的任务是识别出代表现实故障或与系统语义及物理约束一致的偏差转换。
输出： 一个缩减后的可行偏差集合 $D \subseteq (Q_E \times Act_E \times Q_E) \setminus R_E$ ，该集合显著小于完整的转换空间。

2. 符号鲁棒性验证（符号层）

第二阶段在缩减后的集合 $D$ 上进行形式化验证。

过程： 暴力算法（算法 1）遍历所有可行偏差 $D$ 的子集。对于每个候选偏差集 $d$ ，它使用标准的模型检测来验证由监督器 $S$ 控制的偏差系统 $E_d$ 是否满足安全属性 $P$ （即， $E_d/S \models P$ ）。
细化： 该算法仅提取极大鲁棒偏差（即不被其他鲁棒偏差包含的偏差）以形成最终的鲁棒性集合 $\Delta_f$ 。
保证： 由于验证是在形式化定义的转换系统上针对偏差集 $D$ 进行的，因此所得的鲁棒性保证在相对于推断出的集合 $D$ 时，在数学上保持正确。

核心贡献

本文概述了两项主要贡献：

一种神经符号框架： 一种新颖的架构，结合了用于推断物理可行偏差模型的 LLM 与用于计算鲁棒性保证的符号方法。这种方法实现了从自然语言和领域知识中自动提取物理约束，消除了手动进行形式化编码 $P_{sys}$ 的需求。
原型与评估： 实现了一个原型工具，并在三个不同的案例研究上进行了实验评估：制造系统、Therac-25 放射治疗接口以及交替比特协议（ABP）。

实验结果

该框架使用 LLM（GPT-5.2 和 Claude 3.5 Sonnet）进行可行性过滤，并使用基于 Python 的符号验证器进行了评估。

制造系统： LLM 识别出 18 个可行偏差（在理论空间为 108 个的情况下）。符号层找到了一个极大鲁棒偏差集，确认该系统对 15 个特定转换具有鲁棒性，但对特定的缓冲区卸载故障表现脆弱。
Therac-25： 分析识别出 9 个可行偏差。研究发现，系统对于重复的操作员“输入（enter）”按键是鲁棒的，但对于涉及选择电子疗法的特定竞态条件是脆弱的，这准确捕捉到了历史性的设计缺陷。
ABP 协议： LLM 识别出 16 个可行偏差。分析确认了系统对消息丢失、重复和损坏的鲁棒性，这符合协议的设计意图。

定量发现：

可行性缩减： LLM 显著缩小了搜索空间。与完整转换空间相比，缩减幅度从 67%（Therac-25）到 99%（ABP）不等。
可行性准确度： 对于制造系统示例，GPT 生成的转换中有 89% 是物理可行的，而 Claude 为 54%。在更复杂的系统（如 ABP）上，两个模型的可行性率均有所下降（分别为 63% 和 36%），这表明需要改进提示工程或领域本体。
鲁棒性等效性： 尽管是在缩减后的偏差集上运行，该框架产生的鲁棒性保证与在评估案例中通过全转换空间分析获得的保证相当。

意义与主张

本文声称，这种神经符号方法成功解决了离散鲁棒性分析中可扩展性与包含不可行偏差之间的权衡问题。通过使用 LLM 基于语义和物理理解来过滤解空间，该方法使得对于那些无法进行穷举枚举的系统，其鲁棒性分析变得切实可行。

作者强调，虽然 LLM 组件在识别可行偏差时引入了概率性元素，但随后的符号验证确保了最终的鲁棒性保证相对于推断出的集合 $D$ 在形式上是正确的。这项工作证明，通过在大幅缩减的、具有物理意义的偏差子集上运行，可以恢复出与全空间方法相当的鲁棒性分析。

论文最后进行了谦逊的总结，指出当前实现的暴力算法在处理更大规模系统时需要优化，未来的工作将侧重于改进提示工程、引入领域本体以增强 LLM 的准确性，以及研究由符号结果引导 LLM 查询的交互式细化循环。