{"id":"721b04fc-d762-4724-ba2e-6fe40f0e6a9c","arxiv_id":"2508.00500","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Pro2Guard learns a discrete-time Markov chain from LLM agent traces and triggers intervention when the computed probability of reaching an unsafe state exceeds a user-set threshold.","lead":"Pro2Guard is a runtime monitor that learns a probabilistic model of an LLM agent's behavior from execution traces and warns or intervenes when the model says a safety violation is likely. A generalist reader might care because it promises to catch unsafe agent behavior seconds earlier than reactive rule-based systems.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"AV '100% prediction' and time-ahead numbers rest on an in-sample evaluation with no held-out split or false-alarm metric; the PAC bound is cited but never checked.","rationale":"The reader's stated weakest assumption is the Markov/stationarity premise, which is theoretically load-bearing; my focus is the more immediately checkable empirical gap: the AV '100% prediction' and time-ahead results are not shown to be out-of-sample, and no false-alarm rate is defined despite the abstract claiming a no-false-alarm threshold. This is not a fabrication accusation, and the paper's open-source release makes the proposed holdout check feasible. The concern does not move the verdict because the reader already assigned CONDITIONAL; it sharpens the reason: the empirical core of the claim lacks demonstrated predictive validity. If the holdout evaluation passes, the paper could move toward ACCEPT; if it fails or shows high false alarms, the central claim should be downgraded.","tokens_in":18616,"tokens_out":6798,"duration_ms":72787,"concrete_test":"Using the released repository, rebuild the AV experiment with strict holdout: train the DTMC on scenarios 1–4 and evaluate prediction%, time-ahead, and false-alarm rate on scenarios 5–7 plus additional non-violation runs, at θ = 0.3, 0.5, and 0.7; also report per-state n_p values and check Eq. (2). If prediction% or time-ahead drops on unseen scenarios, or false alarms occur at the threshold claimed to have none, the proactive-prediction claim is not established.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4.1 states that each configuration is replayed five times but never separates the traces used to learn the DTMC (Section 3.3) from the traces used to measure prediction; no train/test split, cross-validation, or false-alarm denominator is reported anywhere in the AV evaluation. Table 2's central claims—100% prediction and warnings 0.77–38.66s ahead—are therefore compatible with a model that merely encodes the base rate of violation in the training scenarios: lowering the decision threshold can make the reachability probability exceed θ from almost any state, yielding large 'time ahead' values without genuine forecasting. The abstract's 'threshold yielding no false alarms' is not supported by any false-alarm computation. The PAC guarantee of Eq. (2) could in principle certify out-of-sample behavior, but the paper never reports n_p or max_q n_pq/n_p counts or verifies the inequality for the actual sample sizes. Hence the headline empirical claim is not presently distinguishable from in-sample curve fitting.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes Pro2Guard (also titled 'ProbGuard' in the header/abstract), a runtime monitoring framework for LLM agents. It abstracts agent executions into Boolean predicate states, learns a Discrete-Time Markov Chain (DTMC) from execution traces with validity-aware Laplace smoothing, and at runtime computes the probability of eventually reaching a user-specified unsafe state via PCTL reachability. If the estimated probability exceeds a threshold, an intervention (stop, user inspection, or LLM self-reflection) is triggered. The authors claim that this predict-then-enforce paradigm outperforms reactive rule-based enforcement, reporting reduced unsafe outcomes in embodied household tasks and '100% prediction' of traffic violations and collisions in autonomous driving scenarios, with warnings up to 38.66 seconds ahead. A PAC-style guarantee is cited as justification for the learned model's reliability. The paper includes a discussion of domain abstraction, runtime overhead, and generalizability.","tokens_in":18669,"tokens_out":2497,"duration_ms":27628,"significance":"If the empirical claims were properly supported, this would be a useful contribution to LLM-agent runtime safety: it combines a standard formal-methods toolchain (DTMC learning + PCTL model checking) with a realistic deployment interface, and the open-source implementation and domain-agnostic predicate interface are concrete strengths. The conceptual pipeline is coherent and the use of a cited PAC bound is appropriate. However, the current evaluation does not separate training from test data, so the headline empirical results are not yet established. The idea itself is not highly novel, as DTMC-based probabilistic verification is well known, but the application to proactive LLM-agent enforcement and the explicit treatment of semantic validity constraints give it practical value. The paper's significance depends on a rigorous evaluation that distinguishes genuine forecasting from in-sample curve fitting, which the present manuscript does not provide.","major_comments":[{"comment":"The AV experiments report '100% prediction' and time-ahead values of 0.77–38.66 seconds, but the evaluation never separates the traces used to learn the DTMC (Section 3.3) from those used to measure prediction. Section 4.1 states only that each configuration is replayed five times; it does not state whether the DTMC is trained on the same runs that are then replayed for evaluation. Without a held-out split or cross-validation, the numbers in Table 2 are compatible with an in-sample plug-in estimate that simply reflects the base rate of violations in the training data. The claim is therefore not presently distinguishable from in-sample curve fitting.","section":"Section 4.1, Table 2"},{"comment":"The PAC bound is cited but never checked against the actual data. The paper does not report the per-state counts n_p, the ratios n_pq/n_p, the state space size m, or the chosen epsilon and delta, so the reader cannot verify whether Equation (2) holds for the traces used in Section 4. This matters because the bound is the main justification that finite-sample learning yields statistically reliable reachability estimates. Without reporting these quantities, the claim that Pro2Guard provides 'statistical reliability' remains unsupported.","section":"Section 3.4, Eq. (2)"},{"comment":"The abstract states that a threshold yields 'no false alarms', yet no false-alarm rate, specificity, or confusion-matrix statistic is reported anywhere in the AV evaluation. At low thresholds (e.g., theta = 0.3), a monitor that almost always raises a warning would achieve large time-ahead values and 100% recall on a small set of scenarios while having an arbitrarily poor false-alarm rate. The paper needs a proper detection-theoretic evaluation: true positives, false positives, and true negatives over a held-out set of safe and unsafe episodes, ideally with a comparison against a base-rate forecaster that always predicts eventual violation.","section":"Table 2 / Abstract"},{"comment":"The load-bearing modeling assumption—that abstract transitions are IID draws from a stationary distribution—is explicitly conceded as 'idealized' in Section 3.3. This assumption is not validated for the evaluated domains; the paper does not report tests of stationarity, episode-length distributions, or sensitivity to the 100-frame STL lookback window. Since the reachability probability is computed from the fitted transition matrix, any violation of the IID/stationarity assumption directly biases the risk estimates used for intervention. The paper should at least report a stability analysis (e.g., model trained on different trace subsets, varying smoothing alpha) to show the reported numbers are not artifacts of a particular trace collection.","section":"Section 3.3"}],"minor_comments":[{"comment":"The paper title in the header and abstract reads 'ProbGuard' while the body and running head use 'Pro2Guard'. This inconsistency must be resolved before resubmission.","section":"Title/Abstract"},{"comment":"The text reports an average inference overhead of approximately 430 ms per decision cycle, then reports cached per-decision runtimes of 5–28 ms. It should be clarified whether the 430 ms figure is a cold-cache cost and whether the 5–28 ms figures include the abstraction and I/O overhead reported separately.","section":"Section 4.3"},{"comment":"The property names 'Law38_2', 'Law51_5', 'Law53', and 'No Collision' should be defined or referenced to the LawBreaker specification, and the 'sub-1'/'sub-5' notation in the text is not explained.","section":"Table 2"},{"comment":"The phrase 'Predication successful rates' should be 'Prediction success rates', and throughout the paper 'predication' is used in several places where 'prediction' is intended.","section":"Section 4.1"}],"recommendation":"major_revision","confidential_remarks":"The core technical approach is reasonable and the open-source release is a positive factor. The main barrier to publication is the evaluation methodology: in-sample evaluation and the absence of any held-out or false-alarm analysis undermine the headline claims. The authors should be asked to provide a clear train/test split, report PAC-bound satisfaction or explain why it cannot be verified, and present detection-theoretic metrics. I would also encourage them to unify the paper's title/name before the next round, as the current inconsistency creates confusion about what is being reviewed."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"What you should know: this paper is a genuine new combination of known tools—predicate abstraction, Laplace-smoothed DTMC learning, and PCTL reachability—put to work as a proactive runtime monitor for LLM agents. That combination is new in the LLM-agent-safety space, and the authors are honest about where the model stops. The empirical claims, though, are not yet supported by the numbers as reported.\n\nThe AV \"100% prediction\" and 0.77 to 38.66 second early-warning figures come from seven scenarios, five repeats, no train/test split, no false-alarm denominator, and no error bars. The stress-test concern is on point: nothing in Section 4 separates the traces used to fit the DTMC from those used to measure prediction, so the headline results are compatible with a model that mostly encodes base rates. The PAC bound in Eq. (2) is cited from [43] and never checked against the observed n_p counts, so it cannot rescue the evaluation.\n\nWhere the paper earns credit: the pipeline is coherent and easy to follow. The validity-aware Laplace smoothing over semantically valid transitions is a sensible guard against impossible states. The embodied-agent table shows a clear, interpretable safety/completion tradeoff, and the token-reduction comparison with AgentSpec is a nice practical point. The authors list the key limitations themselves—per-task DTMCs, no time-bounded STL, and the stationarity assumption—which tells me they know where the boundary is.\n\nThe softer spots beyond the evaluation: the load-bearing assumption is that LLM agent behavior over the chosen predicates is a stationary, time-homogeneous DTMC. That is a real simplification for agents with long-horizon context, and the paper only justifies it by episodic resets, not by checking predictive accuracy on held-out deployment data. The predicate set is hand-picked from safety laws, so anything outside those predicates is invisible. Neither of these is fatal—they are scope conditions—but they should be stated more prominently than \"idealized... practically justified.\"\n\nBottom line: this is a serious paper that deserves a serious referee. A good review could tighten the evaluation: add a held-out split, report false alarms and error bars, check the PAC sample-complexity inequality, and test the Markov assumption by comparing one-step lookahead against actual distributions. I would be happy to see it in a venue after that. If you work on LLM-agent safety or runtime verification, it is worth reading; just do not quote the 100% prediction number without the caveats.","headline":"Legitimate new combination of DTMC learning and PCTL reachability for LLM-agent monitoring, but the empirical case is in-sample and the early-warning numbers should not be taken at face value.","tokens_in":19343,"tokens_out":2246,"would_cite":true,"duration_ms":21540,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","60J10"],"pacs":[],"model":"deepseek-v4-flash","headline":"ProbGuard claims a Markov chain learned from an agent's traces lets a runtime monitor estimate the probability of reaching an unsafe state, and that intervening at a risk threshold stops violations reactive rules catch too late.","keywords":["LLM agent safety","runtime monitoring","probabilistic model checking","discrete-time Markov chain","PCTL reachability","proactive enforcement","autonomous driving","embodied household agents"],"falsifier":"Collect a fresh batch of traces from the same agent under the same task distribution, partition them by abstract state, and compare, for each state, the DTMC's predicted probability of eventually reaching the unsafe state against the empirical frequency with which runs from that state actually end in the unsafe state; systematic miscalibration, particularly predictions that worsen as the number of relevant prior steps grows or after a modest shift in the task or environment distribution, would refute the central claim. A cheaper version in the driving setup is to replay recorded scenarios in which the monitor said the risk was below threshold and count how many still produced violations, testing the claim that thresholds like $\\theta=0.3$ yield 100% prediction.","tokens_in":18279,"feed_emoji":"🛡️","tokens_out":19672,"duration_ms":164245,"temperature":0.7,"pith_summary":"ProbGuard's thesis is that LLM-agent safety can be enforced with foresight instead of reaction: abstract the agent's observable state into a handful of safety-relevant Boolean predicates, learn a Discrete-Time Markov Chain from offline execution traces, and at runtime intervene as soon as the model's probability of eventually reaching an unsafe state crosses a user-set threshold. If that thesis holds, a monitor can catch multi-step hazards whose individual actions look benign, such as putting a metal fork in a microwave and then switching it on, two or more steps before the violation, which fixed reactive rules cannot do. The reported numbers support that claim: in driving scenarios the monitor predicts 100% of evaluated traffic-law violations and collisions at threshold 0.3, with warning lead times from 0.77 to 38.66 seconds, and in embodied household tasks it cuts unsafe outcomes from 40.63% to 2.60% when configured to halt, or to 14.07% in a reflection mode that preserves 80.4% of baseline task completion. The paper claims the risk estimates are not merely heuristic: a PAC sample-complexity bound certifies, under stated assumptions, how many traces are needed before the learned reachability probabilities lie within $\\varepsilon$ of the true model. It also concedes limits, one DTMC per task-environment pair and no native handling of time-bounded specifications such as STL, which the paper itself lists as future work in Section 5.2.","feed_headline":"38 seconds early: model foresees unsafe AI-agent moves","feed_subtitle":"A Markov chain over symbolic states lets monitors halt LLM agents before they break rules, and embodied violations drop from 40.6% to 2.6%.","key_machinery":"The central object is a learned Discrete-Time Markov Chain, a finite directed graph whose edges carry the probability of moving from one symbolic state to another, built from predicate-abstracted execution traces. Everything else is in service of making that object faithful and cheap to query. Validity-aware Laplace smoothing ensures no probability mass is assigned to semantically impossible transitions, which matters because sparse data would otherwise make rare unsafe rows look deterministic or unreachable. PCTL reachability in the form $P_{\\le\\theta}[\\mathrm{F}\\,\\mathit{unsafe}]$ is the query that converts the model into a decision, and a PAC bound (Equation 2) converts collected trace counts into a formal statement about how close the learned reachability probabilities are to the ground-truth model. A cache over the finite abstract state space turns repeated model checking into a constant-time lookup, which is what keeps per-decision overhead at 5 to 28 ms.","core_discovery":"On its own terms, the paper's discovery is that a deliberately small probabilistic model, not the LLM itself, can serve as the safety oracle: agent executions are projected onto a state space of predicate valuations (is the fork in the microwave, is the microwave on, is vehicle speed below 0.5 km/h, is a priority NPC ahead), the resulting abstract traces are pooled into a DTMC with Laplace smoothing applied only to transitions that pass domain-specific validity checks, and the monitor answers PCTL queries of the form $P_{\\le\\theta}[\\mathrm{F}\\,\\mathit{unsafe}]$ from the current abstract state. The framework appears as Pro2Guard in the paper's main text and as ProbGuard in the title and abstract. The empirical payload is that this learned reachability probability anticipates violations before they materialize: 100% prediction in all evaluated driving scenarios at $\\theta=0.3$ with 0.77 to 38.66 seconds of lead time, though at the looser $\\theta=0.7$ detection collapses to 0% for most law scenarios, and in embodied tasks the predict-then-enforce loop brings unsafe outcomes down from 40.63% to 2.60% in halt mode and to 14.07% with reflection while keeping 80.4% of the baseline completion rate. The paper's statistical claim is that the learned model is $(\\varepsilon,\\delta)$-PAC-correct for reachability properties, with a per-state sample-count bound (Equation 2) that also serves as a stopping rule for trace collection.","pith_inferences":["Editorial extension: the Markov assumption could be probed directly with an adversarial-history experiment, comparing predicted reachability probabilities for abstractly identical states that were entered through different multi-step prompt or memory histories and correlating any prediction error with history length; the paper does not run this test.","Editorial extension: the reflect mode's success hints that feeding the numeric risk estimate back into the agent's context, rather than only a flag, could act as a behavioral shaping signal, and one could test whether repeated episodes with that feedback reduce the frequency of high-risk states on their own, independent of halting.","Editorial extension: because the predicate vocabulary is drawn from known safety rules, harm expressible only through unmodeled predicates is invisible to the monitor by construction; an audit worth running is adversarial fuzzing that measures how many unsafe outcomes occur on abstract states the monitor rates as safe.","Editorial extension: a hierarchical variant, one chain per task or environment glued by a task-choice action, or a single chain whose transition rows are conditioned on a task-identity feature, could transfer risk estimates across scenarios and shrink the per-task trace budget; the paper notes the MDP direction as future work but does not develop it."],"forward_implications":["A reactive rule framework can be upgraded to proactive enforcement without discarding its symbolic predicates or its intervention actions: the rules' conditions become the DTMC's state space, and halting, user inspection, or LLM self-reflection fire on predicted risk rather than on imminent violation.","Safety becomes a tunable dial rather than a fixed rule: at threshold 0.1 with halting, unsafe outcomes in embodied tasks drop from 40.63% to 2.60% at the cost of completing only 10.42% of tasks, while the reflect mode keeps 47.74% completion (80.4% of the baseline rate) and still cuts unsafe outcomes to 14.07%, a 65.37% relative reduction.","The PAC bound doubles as a sampling budget: a developer can collect traces until every abstract state satisfies Equation 2 for the desired $(\\varepsilon,\\delta)$, and only then deploy the monitor with a stated guarantee on the learned reachability probability.","Because the abstract state space is finite, the reachability probability for every state is precomputed and cached, making each monitoring decision a table lookup with 5 to 28 ms overhead, which the paper measures as acceptable for soft real-time planning loops.","The model produces explainable warnings: in the driving experiments the monitor anticipated 100% of evaluated law violations and collisions at $\\theta=0.3$ with 0.77 to 38.66 seconds of lead time, and it can report the estimated collision probability per state (e.g., 56.78% when a priority NPC is ahead at speed); the paper also reports an average 12.05% token saving over the reactive baseline from"],"supporting_citations":[{"why":"The standard reference for DTMC and PCTL semantics; supplies the model formalism and property language on which the whole pipeline is built.","marker":"[6]"},{"why":"Provides the global PAC bounds for learning DTMCs that ground the paper's claim that the learned transition model is statistically reliable.","marker":"[10]"},{"why":"Supplies the per-state sample-complexity bound (Equation 2) that the paper adapts as its stopping condition for trace collection.","marker":"[43]"},{"why":"The reactive rule-based enforcement baseline that ProbGuard extends and compares against, and the source of its three intervention modes.","marker":"[47]"},{"why":"Source of the traffic-law specifications and law-violating driving scenarios that define the AV domain's unsafe predicates and ground truth.","marker":"[44]"},{"why":"Supplies the autonomous-driving scenarios on which the 100% prediction and 0.77 to 38.66 second lead-time results are measured.","marker":"[45]"},{"why":"The embodied household benchmark that provides the tasks and low-level controller for the embodied-agent safety evaluation.","marker":"[61]"},{"why":"The probabilistic model checker used to evaluate the PCTL reachability queries that decide whether to intervene.","marker":"[25]"}],"fun_headline_variants":["Probabilistic monitor catches agent violations up to 38 seconds early","Markov-chain safety check anticipates unsafe actions in LLM agents","Proactive guard learns agent behavior, predicts violations before they occur","38 seconds heads-up: DTMC-based monitoring forewarns agent rule breaks","Reduce unsafe agent actions by 93% with probabilistic runtime monitoring"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that what the agent does next depends only on its current abstracted situation, and that the situations seen in offline traces match what happens at runtime; the paper's Section 3.3 admits this is an idealization, so if an agent's next action is shaped by a long past that the abstraction discards, or by circumstances that shift after deployment, the predicted risk estimate is untrustworthy no matter how many traces were collected.","fun_headline_variants_meta":{"raw":{"variants":["Probabilistic monitor catches agent violations up to 38 seconds early","Markov-chain safety check anticipates unsafe actions in LLM agents","Proactive guard learns agent behavior, predicts violations before they occur","38 seconds heads-up: DTMC-based monitoring forewarns agent rule breaks","Reduce unsafe agent actions by 93% with probabilistic runtime monitoring"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000949,"raw_usage":{"total_tokens":4163,"prompt_tokens":1171,"completion_tokens":2992,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":787,"completion_tokens_details":{"reasoning_tokens":2902}},"tokens_in":787,"tokens_out":2992,"duration_ms":21786,"temperature":1.0,"reasoning_tokens":2902,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T10:07:09.858024+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Collect a fresh batch of traces from the same agent under the same task distribution, partition them by abstract state, and compare, for each state, the DTMC's predicted probability of eventually reaching the unsafe state against the empirical frequency with which runs from that state actually end in the unsafe state; systematic miscalibration, particularly predictions that worsen as the number of relevant prior steps grows or after a modest shift in the task or environment distribution, would refute the central claim. A cheaper version in the driving setup is to replay recorded scenarios in which the monitor said the risk was below threshold and count how many still produced violations, testing the claim that thresholds like $\\theta=0.3$ yield 100% prediction.","supporting_citations":[{"cited_title":"Principles of Model Checking","cited_arxiv_id":null,"evidence_quote":"The standard reference for DTMC and PCTL semantics; supplies the model formalism and property language on which the whole pipeline is built."},{"cited_title":"Global pac bounds for learning discrete time markov chains","cited_arxiv_id":null,"evidence_quote":"Provides the global PAC bounds for learning DTMCs that ground the paper's claim that the learned transition model is statistically reliable."},{"cited_title":"Probabilistic verification of neural networks against group fairness","cited_arxiv_id":null,"evidence_quote":"Supplies the per-state sample-complexity bound (Equation 2) that the paper adapts as its stopping condition for trace collection."},{"cited_title":"Poskitt, and Jun Sun","cited_arxiv_id":null,"evidence_quote":"The reactive rule-based enforcement baseline that ProbGuard extends and compares against, and the source of its three intervention modes."},{"cited_title":"Poskitt, Jun Sun, Yuqi Chen, and Zijiang Yang","cited_arxiv_id":null,"evidence_quote":"Source of the traffic-law specifications and law-violating driving scenarios that define the AV domain's unsafe predicates and ground truth."},{"cited_title":"Poskitt, Kun Wang, and Jun Sun","cited_arxiv_id":null,"evidence_quote":"Supplies the autonomous-driving scenarios on which the 100% prediction and 0.77 to 38.66 second lead-time results are measured."},{"cited_title":"Prism 4.0: Verification of probabilistic real-time systems","cited_arxiv_id":null,"evidence_quote":"The probabilistic model checker used to evaluate the PCTL reachability queries that decide whether to intervene."}],"review_version":1}