Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems

文章总结与翻译

一、主要内容总结

该文章提出了运行时验证（RV）与大型语言模型（LLMs）共生融合的愿景，旨在解决自主系统中学习驱动组件与开放环境带来的安全性和可信度挑战。

核心背景

• 形式化方法（FMs）虽能提供严格数学保障，但依赖完整模型和静态假设，难以应对神经控制器的不透明性、分布偏移及动态不确定环境。
• 运行时验证（RV）通过 runtime 监控执行过程（含预测性变体的违规预判）弥补形式化方法的不足，但存在规格说明获取复杂、不确定性处理困难等问题。
• 大型语言模型（LLMs）擅长将自然语言转化为形式化制品、识别数据模式，降低形式化验证门槛，但易产生幻觉、缺乏形式化保障，存在不稳定性。

核心融合逻辑

1. LLMs 助力 RV 发展：将自然语言需求转化为形式化规格说明和监控器，降低RV使用门槛；通过学习历史轨迹和领域语料，提供执行延续预测、填补信息缺口，增强预测性RV的不确定性处理能力，支持提前干预。
2. RV 保障 LLM 可靠运行：作为LLMs的多层防护栏，通过句法监控（过滤禁用令牌/模式）、语义监控（执行领域安全约束）、预测性监控（预判幻觉、分布偏移等风险），在 runtime 提供安全性保障，解决LLMs的不透明性和随机性问题。

关键挑战与展望

• 面临信任（LLM生成制品需形式化验