ProbGuard: Proactive Runtime Monitoring for LLM Agent Safety via Probabilistic Prediction

Motivation

• Reactive monitors detect rule violations only when they occur or become imminent, leaving little opportunity to intervene against long-horizon risks.For example, a collision rule may offer little opportunity once a collision becomes unavoidable.Source: §1 · p. 2

Approach

• ProbGuard learns a DTMC over predicate-abstracted execution traces, then estimates the probability of remaining safe and intervenes below a user-defined threshold.Its PAC analysis characterizes learned-dynamics deviation under finite sampling; the monitor assumes observed concrete-state sequences, not a particular agent policy.Source: §1 · p. 2

Empirical evaluation

• ProbGuard predicted traffic-law violations and collision risks in advance; re-prompting reduced unsafe behavior 65.37% versus the unmonitored baseline while retaining 80.4% of baseline task completion.Warnings extended up to 15.84 seconds at a threshold with no false alarms and up to 38.66 seconds under stricter thresholds; halting reduced unsafe behavior 93.60% at a larger completion cost.Source: §1 · p. 2

Contributions

• The framework is implemented on LangChain and released open-source, with a unified abstraction interface intended to support adaptation across domains.The evaluation reports runtime overhead below 50 ms for embodied agents and approximately 100 ms for autonomous driving scenarios.Source: §1 · p. 2

2.1 LLM Agents

• LLM agents are modeled as stochastic state-action systems whose actions induce state transitions and trajectories under a history-conditioned implicit policy.The agent and environment state are represented through valuations, with available actions drawn from the action set.Source: §2.1 · p. 3

2.2 Motivating Example

• When a household agent leaves a lit stove unattended, accumulating risk makes tracking stove status, location, and elapsed time important for intervention before the safety constraint is violated.Possible interventions include returning to the kitchen, switching off the stove remotely, or requesting human assistance.Source: §2.2 · p. 3

2.3 Problem Definition

• The problem is to predict future safety violations early enough to intervene, while encoding safety properties, learning statistically reliable dynamics, and estimating conditional risk from partial executions.The goal is actionable warning before unsafe states are reached, rather than detection only after violations occur or become imminent.Source: §2.3 · p. 3

3.1 Specifying Properties

• CTL expresses qualitative safety requirements, while PCTL queries the learned DTMC for the probability of satisfying their underlying path properties.The framework focuses on the invariant AG ¬unsafe but also supports temporally extended bounded-response properties encoded in CTL.Source: §3.1 · pp. 3–4

3.2 Modeling an Agent’s Behavior

• ProbGuard models agent behavior as a DTMC over symbolic states obtained through domain-specific abstraction.The abstractions incorporate domain-expert knowledge to capture safety-relevant semantics and invariants.Source: §3.2 · p. 4, §3.2.1 · p. 4

3.2.1 Domain-specific Abstraction.

• Domain-specific abstraction maps concrete states to predicate truth-value vectors and restricts the state space to semantically valid valuations.The valid_tran predicate excludes transitions ruled out by domain invariants, including physically irreversible outcomes.Source: §3.2.1 · p. 4

3.2.2 DTMC Model

• The DTMC uses symbolic states derived from behavioral predicates and estimates transitions from execution traces, pruning inconsistent or semantically invalid states.Valid-transition-aware Laplace smoothing assigns probability only to semantically valid transitions, preserving consistency while generalizing across sparsely observed valid transitions.Source: §3.2.2 · p. 4, §3.2.3 · p. 5

3.2.3 Learning the DTMC

• Algorithm 1 is (ε,δ)-PAC-correct for covered reachability or invariant safety properties under Laplace smoothing.For strongly persistent domains such as autonomous driving, the conditioning number can make the stopping condition prohibitively large, motivating frequency estimation with a narrower guarantee.Source: §3.2.3 · pp. 5–6

3.3 Runtime Monitoring

• A runtime monitor queries the learned DTMC for the probability of continued safety and intervenes when that probability falls below threshold θ.The enforcement policy is decoupled from risk detection and may halt, alert, or steer the agent.Source: §3.3 · p. 6

4 Implementing ProbGuard

• At runtime, ProbGuard queries a learned DTMC and appends risk-related context to the agent prompt when predicted safety falls below threshold θ.The LangChain implementation uses PRISM for probabilistic model checking.Source: §4 · p. 6
• In the embodied-agent example, a risk alert includes the safety rule, current symbolic state, and evidence, but does not override action selection or control flow.The agent may revise its reasoning, for example by turning off the stove before leaving.Source: §4 · p. 6
• ProbGuard also integrates with Apollo, and adapting it to a new domain requires an abstraction function, valid_tran predicate, and CTL safety property.The embodied-agent and autonomous-driving abstractions required approximately 200 and 250 lines of Python, respectively.Source: §4 · p. 6

5.1 Encoding Traffic Laws as CTL Safety Properties

• The traffic-law encoding translates bounded-response STL rules into CTL by tracking pending obligations with a deterministic monitor and reducing violations to reachability of an absorbing violation state.The monitor starts a K-step countdown when the trigger occurs; the example’s 100 Apollo control cycles correspond to a 10 s deadline.Source: §5.1 · p. 7

5.2 Empirical Evaluation

• Warnings precede violations in every evaluated case, yielding a 100% detection rate; advance times reach 15.84s and 13.41s for bounded-response cases and 38.66s for collision cases at stricter thresholds.Warning-time stability varies by scenario: some bounded-response cases are largely threshold-invariant, while Scenarios 4 and 5 are threshold-sensitive despite instantiating the same law.Source: §5.2 · p. 8
• At θ=0.3, ProbGuard records 0% false positives across four properties on safe traces; the false-positive rate rises to 75% at θ=0.5 and 100% at θ=0.7.The safe traces span six scenarios, including pedestrian crossings, lane changes, motorcycle encounters, and stationary obstacle avoidance.Source: §5.2 · p. 8
• Under REDriver’s fixed σ=0.4 threshold, Scenarios 1 and 2 produce no advance predictions; its robustness thresholds also combine variables with incompatible scales.ProbGuard’s θ instead represents a lower bound on the estimated probability of remaining safe.Source: §5.2 · p. 9
• In the left-turn stress test, estimated collision risk rises from 47.15% without a priority NPC or pedestrian ahead to 56.78% when a priority NPC is present.ProbGuard expresses these risk scores on a normalized [0, 1] scale.Source: §5.2 · p. 9
• Runtime monitoring overhead in autonomous driving is 100.79 ± 16.96 ms, with monitoring proposed at intervals below the control-loop frequency.The evaluation uses Apollo, collects 30 traces per scenario, and is intended to assess useful warning under limited data rather than formally certify the learned models.Source: §5.2 · pp. 8–9

6.1 Illustrative Example

• For the stove example, the safety property forbids the joint condition of the stove being on, the agent being in the kitchen, and elapsed time reaching T.The learned DTMC represents feasible predicate combinations as symbolic states; when predicted safety falls below a threshold such as 0.7, ProbGuard injects a corrective prompt to steer away from the hazardous configuration.Source: §6.1 · p. 9

6.2 Empirical Evaluation

• The embodied-agent evaluation uses ReAct with SafeAgentBench’s low-level controller, GPT-4o-mini at temperature 0, PRISM, and 30 traces per task to learn each DTMC.Safety properties are evaluated across enforcement regimes; Table 2 reports unsafe rate and task completion, with larger thresholds indicating stricter intervention.Source: §6.2 · p. 9, Table 2 · p. 10
• At θ=0.9, stop reduces unsafe outcomes to 2.60% (93.60% relative reduction), with 10.42% completion; reflect reduces unsafe behavior by 65.37% while retaining 47.74% completion, 80.4% of baseline.The unmonitored baseline has 40.63% unsafe outcomes and 59.38% task completion; Table 2 compares unsafe rate and completion across enforcement regimes.Source: §6.2 · pp. 9–10, Table 2 · p. 10
• ProbGuard’s predictive reasoning can early-reject unsafe trajectories before an action, avoiding redundant LLM queries and reducing average token use by 12.05% in long-horizon tasks.The paper contrasts this with AgentSpec’s reactive step-by-step checks and manually engineered symbolic constraints.Source: §6.2 · p. 10
• Cached DTMC inference reduces per-decision overhead from 430 ms to 5–8 ms for small abstractions, 13 ms at 8 states, 28 ms at 16 states, and below 50 ms at 32 states.Inference is the dominant uncached cost; caching precomputes unsafe-state probabilities for each symbolic state, enabling constant-time lookup. Figure 4 shows average overhead by number of abstract states, with run-to-run variation.Source: §6.2 · p. 10, Figure 4 · p. 10

PAC Bounds in Practice

• For reachability checking, the PAC bound requires 185–1,016 traces, while the evaluation uses only 30 traces per scenario.The analysis characterizes samples needed for formal certification; experiments report practical effectiveness with a smaller budget, and closing the gap requires more sampling and computational resources.Source: §7 · pp. 10–11
• Embodied-agent DTMCs are well-mixed with moderate conditioning, whereas autonomous-driving chains have self-loops above 99.9% and conditioning numbers around 10^7–10^8 under Laplace smoothing.Frequency estimation removes the error factor tied to Laplace smoothing, trading the stronger uniform CTL guarantee for a lower sample requirement suitable for runtime monitoring.Source: §7 · p. 11

Threats to Validity

• An incomplete or overly coarse abstraction can omit delayed or history-dependent effects, violate the Markov assumption, and bias learned transition probabilities and risk estimates.The PAC guarantees bound estimation error relative to the learned model, not misspecification caused by inadequate abstraction.Source: §7 · p. 11
• Residual variance from stochastic trajectory sampling and agent behavior may affect reproducibility and risk estimates, particularly in sparsely explored states, despite repeated runs and reported averages.The authors mitigate this threat through repeated runs and averages.Source: §7 · p. 11

Limitations and Future Work

• Scalability remains a challenge as the predicate space grows; proposed directions include abstraction refinement, compositional reasoning, symbolic model checking, and selective state-space exploration.Future work also includes active learning, online updates, improved predicate discovery and abstraction learning, richer PCTL properties, and natural language-to-specification pipelines.Source: §7 · p. 11

Agent Safety

• AgentSpec [42], ShieldAgent [12], and GuardAgent enforce local constraints, while ProbGuard models multi-step risk evolution through symbolic abstraction and probabilistic reachability.The passage describes these methods as typically assuming static constraints and ignoring multi-step risk evolution.Source: §8 · p. 11
• LMQL enforces logical constraints during decoding, whereas ProbGuard reasons dynamically at runtime over symbolic state transitions and probabilistic reachability.Toolformer [36] and Voyager [41] are cited as expanding agents into tool-augmented and open-world environments, motivating proactive safety enforcement.Source: §8 · p. 11

Runtime Verification

• ProbGuard learns a DTMC from observed agent trajectories and uses probabilistic reachability to support proactive intervention before unsafe states are reached.The framework builds on runtime verification while addressing stochastic agent workflows without a handcrafted transition model.Source: §8 · p. 11
• PSTMonitor [10] and MDP-based monitors incorporate stochastic reasoning but assume predefined probabilistic models or manually specified safety properties.Other probabilistic runtime-verification directions include state estimation, adaptive updates, and conformal prediction [11] [28].Source: §8 · p. 11

9 Conclusion

• Experiments in embodied-agent and autonomous-driving domains show that ProbGuard can improve safety while preserving task performance.The framework models behavior as DTMCs over symbolic abstractions and can intervene before violations occur.Source: §9 · p. 12

Data Availability Statement

• The repository at includes the benchmark, safety rules, learned DTMCs, source code, and a LangChain-based implementation of runtime monitoring and intervention.The artifacts are provided to support reproduction.Source: Data Availability Statement · p. 12

• The proof’s Theorems 5 and 6 are results of Bazille et al., not results of this paper.Source: A Proof of Theorem 3.4 · p. 13
• For reachability or invariant safety properties covered by, Algorithm 1 is (ε,δ)-PAC-correct at the stated confidence δ and error ε.Source: A Proof of Theorem 3.4 · p. 13
• Transition counts and the algorithm’s stopping rule support concentration bounds, combined across the |S| source states using a union bound.Source: A Proof of Theorem 3.4 · p. 13
• The proof propagates local transition-probability error to satisfaction probabilities using the reachability-sensitivity result of Theorem 5 of.Source: A Proof of Theorem 3.4 · p. 13
• The conditioning number is computed on the learned chain; Laplace smoothing keeps semantically valid transitions bounded away from zero, making the bound finite and runtime-checkable.Source: A Proof of Theorem 3.4 · p. 13