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

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autore principale: Ferrando, Angelo
Natura: Preprint
Pubblicazione: 2025
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866908662341042176
author Ferrando, Angelo
author_facet Ferrando, Angelo
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2511_14435
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
Ferrando, Angelo
Software Engineering
Artificial Intelligence
Logic in Computer Science
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.
title Watchdogs and Oracles: Runtime Verification Meets Large Language Models for Autonomous Systems
topic Software Engineering
Artificial Intelligence
Logic in Computer Science
url https://arxiv.org/abs/2511.14435