Pro2Guard: Proactive Runtime Enforcement of LLM Agent Safety via Probabilistic Model Checking

• URL: http://arxiv.org/abs/2508.00500v1
• Date: Fri, 01 Aug 2025 10:24:47 GMT
• Title: Pro2Guard: Proactive Runtime Enforcement of LLM Agent Safety via Probabilistic Model Checking
• Authors: Haoyu Wang, Chris M. Poskitt, Jun Sun, Jiali Wei,
• Abstract summary: Large Language Model (LLM) agents exhibit powerful autonomous capabilities across domains such as robotics, virtual assistants, and web automation.<n>Existing rule-based enforcement systems, such as AgentSpec, focus on developing reactive safety rules.<n>We propose Pro2Guard, a proactive runtime enforcement framework grounded in probabilistic reachability analysis.
• Score: 8.970702398918924
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large Language Model (LLM) agents exhibit powerful autonomous capabilities across domains such as robotics, virtual assistants, and web automation. However, their stochastic behavior introduces significant safety risks that are difficult to anticipate. Existing rule-based enforcement systems, such as AgentSpec, focus on developing reactive safety rules, which typically respond only when unsafe behavior is imminent or has already occurred. These systems lack foresight and struggle with long-horizon dependencies and distribution shifts. To address these limitations, we propose Pro2Guard, a proactive runtime enforcement framework grounded in probabilistic reachability analysis. Pro2Guard abstracts agent behaviors into symbolic states and learns a Discrete-Time Markov Chain (DTMC) from execution traces. At runtime, it anticipates future risks by estimating the probability of reaching unsafe states, triggering interventions before violations occur when the predicted risk exceeds a user-defined threshold. By incorporating semantic validity checks and leveraging PAC bounds, Pro2Guard ensures statistical reliability while approximating the underlying ground-truth model. We evaluate Pro2Guard extensively across two safety-critical domains: embodied household agents and autonomous vehicles. In embodied agent tasks, Pro2Guard enforces safety early on up to 93.6% of unsafe tasks using low thresholds, while configurable modes (e.g., reflect) allow balancing safety with task success, maintaining up to 80.4% task completion. In autonomous driving scenarios, Pro2Guard achieves 100% prediction of traffic law violations and collisions, anticipating risks up to 38.66 seconds ahead.

Related papers

• WebGuard: Building a Generalizable Guardrail for Web Agents [59.31116061613742]
  WebGuard is the first dataset designed to support the assessment of web agent action risks.<n>It contains 4,939 human-annotated actions from 193 websites across 22 diverse domains.
  arXiv  Detail & Related papers  (2025-07-18T18:06:27Z)
• OpenAgentSafety: A Comprehensive Framework for Evaluating Real-World AI Agent Safety [58.201189860217724]
  We introduce OpenAgentSafety, a comprehensive framework for evaluating agent behavior across eight critical risk categories.<n>Unlike prior work, our framework evaluates agents that interact with real tools, including web browsers, code execution environments, file systems, bash shells, and messaging platforms.<n>It combines rule-based analysis with LLM-as-judge assessments to detect both overt and subtle unsafe behaviors.
  arXiv  Detail & Related papers  (2025-07-08T16:18:54Z)
• SafeAgent: Safeguarding LLM Agents via an Automated Risk Simulator [77.86600052899156]
  Large Language Model (LLM)-based agents are increasingly deployed in real-world applications.<n>We propose AutoSafe, the first framework that systematically enhances agent safety through fully automated synthetic data generation.<n>We show that AutoSafe boosts safety scores by 45% on average and achieves a 28.91% improvement on real-world tasks.
  arXiv  Detail & Related papers  (2025-05-23T10:56:06Z)
• SafePath: Conformal Prediction for Safe LLM-Based Autonomous Navigation [67.22657932549723]
  We introduce SafePath, a framework that augments Large Language Models (LLMs) with formal safety guarantees.<n>In the first stage, we use an LLM that generates a set of diverse candidate paths, exploring possible trajectories based on agent behaviors and environmental cues.<n>In the second stage, SafePath filters out high-risk trajectories while guaranteeing at least one safe option is included with a user-defined probability.<n>In the final stage, our approach selects the path with the lowest expected collision risk when uncertainty is low or delegates control to a human when uncertainty is high.
  arXiv  Detail & Related papers  (2025-05-14T14:28:24Z)
• LlamaFirewall: An open source guardrail system for building secure AI agents [0.5603362829699733]
  Large language models (LLMs) have evolved from simple chatbots into autonomous agents capable of performing complex tasks.<n>Given the higher stakes and the absence of deterministic solutions to mitigate these risks, there is a critical need for a real-time guardrail monitor.<n>We introduce LlamaFirewall, an open-source security focused guardrail framework.
  arXiv  Detail & Related papers  (2025-05-06T14:34:21Z)
• AgentSpec: Customizable Runtime Enforcement for Safe and Reliable LLM Agents [8.290987399121343]
  We propose AgentSpec, a lightweight language for specifying and enforcing runtime constraints on LLM agents.<n>With AgentSpec, users define structured rules that incorporate triggers, predicates, and enforcement mechanisms.<n>We implement AgentSpec across multiple domains, including code execution, embodied agents, and autonomous driving.
  arXiv  Detail & Related papers  (2025-03-24T13:31:48Z)
• Guardians of the Agentic System: Preventing Many Shots Jailbreak with Agentic System [0.8136541584281987]
  This work uses three examination methods to detect rogue agents through a Reverse Turing Test and analyze deceptive alignment through multi-agent simulations.<n>We develop an anti-jailbreaking system by testing it with GEMINI 1.5 pro and llama-3.3-70B, deepseek r1 models.<n>The detection capabilities are strong such as 94% accuracy for GEMINI 1.5 pro yet the system suffers persistent vulnerabilities when under long attacks.
  arXiv  Detail & Related papers  (2025-02-23T23:35:15Z)
• Criticality and Safety Margins for Reinforcement Learning [53.10194953873209]
  We seek to define a criticality framework with both a quantifiable ground truth and a clear significance to users.<n>We introduce true criticality as the expected drop in reward when an agent deviates from its policy for n consecutive random actions.<n>We also introduce the concept of proxy criticality, a low-overhead metric that has a statistically monotonic relationship to true criticality.
  arXiv  Detail & Related papers  (2024-09-26T21:00:45Z)
• SMARLA: A Safety Monitoring Approach for Deep Reinforcement Learning Agents [7.33319373357049]
  This paper introduces SMARLA, a black-box safety monitoring approach specifically designed for Deep Reinforcement Learning (DRL) agents. SMARLA utilizes machine learning to predict safety violations by observing the agent's behavior during execution. Empirical results reveal that SMARLA is accurate at predicting safety violations, with a low false positive rate, and can predict violations at an early stage, approximately halfway through the execution of the agent, before violations occur.
  arXiv  Detail & Related papers  (2023-08-03T21:08:51Z)
• Safety Margins for Reinforcement Learning [53.10194953873209]
  We show how to leverage proxy criticality metrics to generate safety margins. We evaluate our approach on learned policies from APE-X and A3C within an Atari environment.
  arXiv  Detail & Related papers  (2023-07-25T16:49:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.