发帖
雷达卡
当大语言模型与运行时验证融合：自主系统迎来“智能+安全”双重保障
在自动驾驶、医疗机器人等高风险领域，自主系统的安全性与智能化水平始终面临严峻挑战。传统方法难以兼顾灵活性与可靠性，而本文提出的运行时验证（Runtime Verification, RV）与大语言模型（Large Language Models, LLMs）的协同框架，为这一难题提供了全新的解决思路。
论文核心信息
- 原标题：Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
- 作者：Angelo Ferrando
- 所属机构：意大利摩德纳和雷焦艾米利亚大学（University of Modena and Reggio Emilia）
- 发表会议：第七届国际自主系统形式化方法研讨会（Seventh International Workshop on Formal Methods for Autonomous Systems, FMAS 2025）
- 出版信息：EPTCS 436, 2025, pp. 80–87, doi:10.4204/EPTCS.436.8
引文格式（GB/T 7714）
Ferrando A. Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems[C]//Luckcuck M, Schwammberger M, Xu M, eds. Seventh International Workshop on Formal Methods for Autonomous Systems (FMAS 2025). EPTCS 436. 2025: 80-87. doi:10.4204/EPTCS.436.8
摘要概述
文章提出将运行时验证与大语言模型进行深度整合，构建面向自主系统的双向增强机制。形式化方法虽具备数学严谨性，但依赖完整建模，在动态环境中适应性差；RV通过实时监控行为轨迹弥补该缺陷，尤其支持预测性监控；LLMs则擅长自然语言理解与模式识别，可辅助生成形式化规格，但存在“幻觉”问题且缺乏安全保障。二者结合的关键在于：RV为LLM驱动的决策提供安全边界，而LLMs降低RV规格编写门槛，并支持不确定性推理与前瞻性分析。
与现有研究中单向应用（如LLM仅用于翻译需求为逻辑表达式，或RV仅用于监督LLM输出）不同，本文强调双向互动架构，并系统探讨了信任建立、计算效率、认证合规（如ISO 26262）、领域适配性及可解释性五大挑战。未来方向包括混合式预测RV、领域定制化LLM训练等。
背景剖析：自主系统的双重困境
设想一个场景：一辆自动驾驶汽车在雨夜行驶时，突然有行人闯入车道。系统必须在毫秒内判断是否紧急制动——但如果感知模块误判距离，或将湿滑路面的影响忽略，后果可能致命。这揭示了自主系统的核心矛盾：既要高度灵活以应对开放世界，又要绝对可靠以确保安全。
当前主流技术路径各有局限：
形式化方法（FMs）：精确却僵化
形式化方法类似于“预设的安全蓝图”，利用数学工具验证系统是否满足特定属性，例如“车速超过30km/h时必须激活预警”。然而其根本限制在于对环境模型的高度依赖——一旦出现未被建模的情况（如突发障碍物、极端天气），系统便无法做出正确响应。面对无限多变的真实世界，穷举所有可能情形显然不现实。
运行时验证（RV）：动态但复杂
RV扮演的是“运行中的审计员”角色，不追求事前证明一切，而是在系统执行过程中持续监测行为是否符合规范。例如检测到“车辆高速行驶但未发出警告”即触发警报。但其瓶颈在于：需要人工将模糊的自然语言需求（如“避免碰撞”）转化为严格的时序逻辑公式（如“若前方5米内有人，则2秒内减速至0”）。这一过程专业性强、成本高，阻碍了广泛应用。
大语言模型（LLMs）：便捷却不可信
LLMs展现出强大的语义解析能力，能够自动将非结构化指令转换为潜在的技术规格，甚至从历史数据中挖掘潜在规律（如“雨天制动距离延长”）。然而其固有问题不容忽视：容易产生“幻觉”——编造错误规则（如“穿红衣行人无需避让”），或误解关键参数（如将限速30写成50）。直接将其作为决策依据，相当于把安全托付给一个未经核实的信息源。
因此，自主系统如同一名需同时佩戴“安全帽”与“敏捷帽”的运动员：前者防止受伤，后者保证动作灵活。而现有方案往往只能兼顾其一，甚至两者相互冲突。本文所提的RV与LLMs共生架构，正是为了实现两者的协同增效。
创新突破：从单向辅助到双向赋能
本研究并非简单地将LLMs用作RV的前端输入工具，也不是仅用RV来事后检验LLM输出，而是构建了一种双向闭环协作机制。相较于以往工作，本文的三大核心贡献如下：
- 安全护栏 + 智能引擎：RV为LLM生成的行为策略设置硬性约束，充当“看门狗”（Watchdog），防止危险操作被执行；同时，LLM作为“预言机”（Oracle），反向协助RV自动生成、优化监控规则，提升其适应性和覆盖范围。
- 降低规格获取难度：借助LLM的理解能力，工程师可用自然语言描述监控目标，由模型自动转化为形式化逻辑表达式，显著降低RV部署门槛。
- 支持预见性与不确定性处理：LLM可基于上下文预测潜在风险场景，推动RV从被动检测转向主动预测；同时在信息不全或模糊条件下，仍能提供合理推断，增强系统鲁棒性。
此外，论文还深入讨论了实际落地中的关键挑战，包括如何建立对LLM输出的信任机制、如何平衡实时性与计算开销、如何满足功能安全标准（如ISO 26262）的要求，并呼吁开展跨学科合作，推动该范式走向工程实践。
LLM的“三重身份”：从被动执行到协同共治
以往研究中，大语言模型（LLMs）通常仅承担单一角色——要么作为“翻译中介”，协助形式化验证（RV）编写系统规格；要么作为“被监管对象”，由RV对其输出进行纠错审查。本文创新性地赋予LLM三种并行角色，实现功能跃迁：
- 赋能者：将非专业的自然语言需求自动转化为RV可解析的形式化规格，显著降低工程师使用门槛；
- 协作者：基于历史运行数据预测系统行为趋势（例如，“检测到行人 → 极可能触发制动”），辅助RV提前识别潜在风险；
- 被监控者：其生成内容需接受RV的多层级审核，防止因“幻觉”引发安全漏洞。
这一转变相当于将LLM从“仅能打字的文员”升级为“既能制定策略、又能提出预警、同时接受监督的智能伙伴”。
RV的“三层防御机制”：从事后响应到事前干预
传统RV机制更像“消防员”，只有在违规事件发生后才发出警报（如“车辆已越线才报警”）。而本文提出的RV体系则进化为“主动式安全顾问”，具备三层递进式防护能力：
- 句法层防护：拦截LLM输出中的明显语法错误或危险指令（如禁止出现“禁止刹车”类表述）；
- 语义层校验：确保生成内容符合领域特定规则（如“自动驾驶必须遵守交通信号灯”）；
- 预测层预判：结合LLM对系统未来轨迹的预测结果，提前评估风险（如“LLM预测2秒后车速仍高于30km/h”，RV即刻启动预警）。
通过这种机制，系统实现了从“事后补救”向“事前预防”的跨越，为自主决策争取了关键的“时间裕度”。
[此处为图片2]认证适配机制：推动动态安全保障获得合规认可
当前一项关键技术瓶颈在于监管层面的认可问题。以汽车行业为例，ISO 26262等标准主要承认“静态、预先证明的安全证据”，而RV与LLMs联合提供的却是“运行时动态监控数据”。直接宣称“系统会自行保障安全”难以通过合规审查。为此，本文提出核心解决方案：将RV+LLMs产生的“动态证据链”纳入认证框架，例如：
- LLM生成的每条规格均附带RV验证记录；
- 实时监控过程日志具备完整可追溯性。
此举有效打通了高阶智能系统通往实际部署的“最后一公里”。
研究路径解析：如何构建“双向协同”体系？
论文采用“问题定位→架构设计→价值验证”的逻辑主线，系统性地推进研究，具体分为五个清晰步骤：
步骤一：梳理技术痛点，明确改进方向
作者首先系统分析了形式化方法（FMs）、RV与LLMs各自的局限性，并通过对比表格归纳其能力边界。此步骤旨在精准锁定核心问题，避免方案偏离真实需求。例如发现：“RV的最大障碍是难以获取高质量规格”，而“LLMs的主要风险在于缺乏安全保障机制”。这些问题为后续“双向协同”设计提供了切入点。
步骤二：构建“双向共生”系统架构（核心图示见图2）
作者设计了一套闭环交互架构，明确定义RV与LLMs之间的协作流程：
- 前端处理：LLM将自然语言需求转为候选规格，交由RV验证（如“10米内遇行人须刹车”是否符合法规）；
- 中端运行：系统执行过程中，LLM基于运行日志预测下一步行为（如“感知到行人 → 预测即将制动”），RV据此提前评估安全性；
- 后端控制：所有LLM输出必须经过RV的“三重过滤”（句法→语义→预测），仅通过审核的指令方可下达至自主系统。
该架构的核心在于形成“LLM助力RV，RV约束LLM”的双向闭环，实现能力互补与风险制衡。
[此处为图片3]步骤三：分维度验证协同增效价值
作者并未泛泛而谈“融合有益”，而是从两个方向深入论证协同优势：
LLM如何增强RV能力？
- 降低使用门槛：通过“提示生成→RV验证→反馈修正”的迭代循环，使非专业人员也能产出合规规格；
- 提升预测能力：利用LLM从历史数据中学习行为模式，补全不完整观测（如仅检测到行人即可推断制动意图），帮助RV实现前置风险判断。
RV如何保障LLM可靠性？
- 错误防范机制：通过句法过滤禁用词、语义检查领域规则，阻止LLM“幻觉”导致的危险输出；
- 安全兜底策略：当LLM预测置信度不足（如“无法确定是否应刹车”）时，RV自动切换至传统监控模式，仅依据实际运行轨迹判断，确保安全底线不被突破。
步骤四：横向对比凸显创新性
为突出本文贡献，作者专门设计对比表格（Table 1），将本方案与三类现有研究进行对照：
| 研究类型 | LLM角色 | RV角色 | 本文改进点 |
|---|---|---|---|
| LLM→规格翻译 | 单向翻译官 | 离线验证者 | 引入LLM参与实时行为预测，而非仅做静态翻译 |
| LLM单向监控 | 被监控黑箱 | 单向安全员 | 让LLM反向优化RV，形成双向支持 |
| 传统预测RV | 无 | 依赖预设模型预测 | 利用LLM补全不确定场景下的行为轨迹 |
该对比清晰表明：本文并非简单整合已有技术，而是首次解决了“双向协同”这一未被充分覆盖的关键问题。
步骤五：直面挑战，规划落地路径
作者坦诚指出当前面临的五大现实挑战：信任建立、运行效率、人机协作、系统鲁棒性及伦理合规，并针对每一项提出初步应对思路（如采用轻量化LLM模型缓解效率压力）。同时，文章还关联ISO 26262、DO-178C等主流认证标准，探讨如何使RV+LLMs生成的动态证据满足监管要求。这使得整个方案不仅具有理论深度，更具备工程落地潜力。
研究成果与领域贡献：构建新型安全范式
本研究并未聚焦于新算法的发明，而是提出了一套全新的系统级解决方案，为自主系统安全领域带来三项实质性贡献：
| 成果类型 | 具体内容 | 领域价值 |
|---|---|---|
| 理论成果 | 提出RV与LLMs的“双向共生模型” | 打破“安全 vs. 灵活性”的固有矛盾，提供全新的理论框架支撑高可信自主系统发展 |
| 技术落地价值 | 设计可集成的协同架构与认证适配方案 | 推动动态安全保障机制走向实际应用，弥合学术研究与产业需求之间的鸿沟 |
本文提出了一种全新的“双向共生”范式，旨在解决自主系统中长期存在的“安全性与适应性难以兼顾”、“技术门槛高”以及“认证落地难”三大核心挑战。通过将运行时验证（RV）与大语言模型（LLMs）深度融合，构建了一个互为支撑、协同进化的安全框架，推动自主系统向更智能、更可信的方向发展。
该方案的核心价值在于实现了两个关键突破：一是解决了RV在实际应用中的“规格门槛”问题，使中小团队也能借助LLMs自动生成形式化规格；二是回应了LLMs在安全关键场景下的“行为不可控”隐患，利用RV对LLM输出进行多层级监控，确保其决策始终处于安全边界之内。这种双向赋能机制显著降低了技术普及成本，使得更多资源有限的团队能够安全地引入智能能力。
在认证层面，论文创新性地提出“将runtime证据纳入认证体系”的理念，打通了技术从实验室到工业落地的“最后一公里”。尤其针对汽车、航空等强监管领域，传统认证标准（如ISO 26262、DO-178C）主要依赖离线验证和静态追溯，难以应对动态环境下的不确定性。为此，本文建议从三个方面升级认证要求：
（1）可追溯性标准升级：需建立从自然语言需求，经由LLM生成的形式化规格，再到RV监控器执行的完整审计链路，确保每一步转化过程均可追溯、可审查；
（2）动态证据纳入：认证应接受RV+LLM系统在运行过程中产生的实时日志、预测性违规概率、LLM拒绝响应的原因分析等runtime数据作为安全保障的有效组成部分；
（3）LLM可信度评估机制：要求系统提供关于LLM性能的量化报告，例如生成规格的准确率、预测延续的可靠性，并通过静态分析工具对LLM输出进行前置验证，防止隐性缺陷渗透至安全控制环节。
[此处为图片2]针对研究方向的引导，本文明确了未来值得深入探索的技术路径，包括混合预测型RV架构的设计、LLMs在特定领域（如航空航天、医疗设备）的行为适配优化等。这些方向为后续研究提供了清晰的“靶标”，有助于避免重复投入与资源浪费。
值得注意的是，本工作属于典型的“愿景论文”（Vision Paper），当前尚未发布开源代码或公开数据集。其核心贡献不在于实现具体工具，而在于提出一套具有前瞻性的框架性思路——这类结构性创新往往是推动整个领域跃迁的关键驱动力。
关键问题解析
问题一：RV与LLMs如何通过双向协同缓解自主系统的“安全性-适应性”矛盾？
自主系统必须同时满足安全性（依赖形式化方法保障）与适应性（应对复杂多变环境），二者往往存在张力。本文提出的双向协同机制有效化解了这一矛盾：
（1）LLMs提升适应性：通过理解自然语言需求并快速转化为形式化规格，大幅降低RV的应用门槛；同时，LLMs能从历史运行数据中学习环境规律（例如“雨天→刹车距离增加”），为RV提供预测性执行延续，增强系统在不确定条件下的响应能力；
（2）RV保障安全性：采用句法、语义与预测性三层监控机制，对LLM的黑箱输出进行实时监督，防止幻觉引发危险决策；当LLM预测置信度不足时，RV可自动切换至保守模式，沿用传统形式化规则维持系统稳定，从而确保安全约束永不被突破。
由此形成“适应性由LLMs拓展，安全性由RV兜底”的动态平衡结构。
[此处为图片3]问题二：现有研究未能覆盖的核心场景是什么？本文如何填补空白？
当前相关研究普遍存在三大局限，未能覆盖自主系统所需的“实时性-不完全信息-双向协同”三位一体场景：
（1）LLM→规格转换类工作（如Cohen & Peled）仅支持静态规格生成，无法满足自动驾驶等高实时性任务的持续监控需求；
（2）LLM监控类研究（如Pro2Guard）仅为单向监督，LLM本身不参与监控逻辑，难以处理部分可观测环境下的推理补全；
（3）传统预测性RV缺乏数据驱动能力，难以从海量交互数据中提炼行为模式。
本文通过两项创新填补上述空白：
（1）场景聚焦：面向医疗机器人、自动驾驶等毫秒级响应需求，设计“LLM预测 + RV验证”的低延迟闭环流程；
（2）机制创新：允许LLM主动参与RV的预见性推理（如基于上下文补全缺失观测），同时接受RV对其输出的反向制约，构建“LLM增强RV，RV约束LLM”的双向闭环体系，超越传统的单向依赖模式。
问题三：RV+LLM融合对安全关键领域的认证体系提出了哪些新要求？
如前所述，核心诉求是认证框架必须认可runtime阶段产生的动态证据。具体体现在以下三点：
（1）建立从原始需求到最终监控执行的端到端追溯链条，涵盖LLM生成中间产物的过程；
（2）将系统运行期间生成的实时监控记录、风险预警信号、LLM拒绝推断的理由说明等动态信息，正式纳入合规性评估依据；
（3）制定针对LLM本身的可信评估标准，要求系统输出包含LLM行为验证报告，例如由形式化检查器确认其生成规格的正确性。
总结：迈向“智能即安全”的新范式
这篇论文最重要的贡献，是确立了自主系统安全治理的“新范式”——从过去单一防线式的“被动防护”，转向RV与LLMs相互促进的“共生共守”。它并非否定已有技术，而是通过优势互补，实现了对既有能力的有机整合。
当然，该框架仍有待完善之处：例如LLM生成规格后的验证效率仍需提升，在极端实时场景下轻量化部署尚存挑战，且在伦理与法律责任划分上（如事故归因于LLM误判还是RV失效）还需进一步明晰。
但不可否认的是，这种“让系统既懂规则又能灵活应对”的设计理念，为自动驾驶、手术机器人等高风险应用场景开辟了一条切实可行的技术演进路径。
或许在未来某一天，当我们乘坐的无人驾驶车辆在突发状况下依然能做到“临危不乱、应对得当”，那时回望，便会想起这篇论文所倡导的“双向共生”思想——有时候，真正的突破不在于创造最强大的个体，而在于找到最佳的协作方式。
京公网安备 11010802022788号
