用大模型增强运行时验证，让自主系统更安全可靠。
Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
- 大模型辅助生成形式化规范，提升验证效率。
- 运行时验证为大模型决策提供实时安全约束。
- 适合研究可信自主系统与智能安全的学者。
确保自主系统在学习组件和开放环境中的安全性和可信性极具挑战。形式化方法虽能提供强保证，但依赖完整模型和静态假设。运行时验证（RV）通过运行时监控执行过程，并在预测性变体中提前识别潜在违规。大语言模型（LLMs）擅长将自然语言转化为形式化产物并识别数据模式，但存在错误且缺乏形式保证。本文提出一种协同融合机制：RV可作为大模型驱动自主性的护栏，而大模型则能辅助规范捕获、支持前瞻性推理并处理不确定性。我们阐述该互促机制区别于现有综述与路线图之处，讨论挑战与认证影响，并提出迈向可靠自主性的未来研究方向。
原文摘要 · Abstract (English)
Assuring the safety and trustworthiness of autonomous systems is particularly difficult when learning-enabled components and open environments are involved. Formal methods provide strong guarantees but depend on complete models and static assumptions. Runtime verification (RV) complements them by monitoring executions at run time and, in its predictive variants, by anticipating potential violations. Large language models (LLMs), meanwhile, excel at translating natural language into formal artefacts and recognising patterns in data, yet they remain error-prone and lack formal guarantees. This vision paper argues for a symbiotic integration of RV and LLMs. RV can serve as a guardrail for LLM-driven autonomy, while LLMs can extend RV by assisting specification capture, supporting anticipatory reasoning, and helping to handle uncertainty. We outline how this mutual reinforcement differs from existing surveys and roadmaps, discuss challenges and certification implications, and identify future research directions towards dependable autonomy.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。