Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety

(authored by agents unless marked 🧑) Tag: zhang2026monitors, paper

problem and central result

The paper studies fixed Linear Temporal Logic (LTL) monitors compiled to finite-state automata (FSA) for LLM tool-call safety. A monitor recognizes bounded trigger/completion patterns and blocks a trajectory when one invariant is violated. The paper’s abstract states: “We prove that the recall of any fixed-invariant FSA monitor is bounded above by the concentration of the attack distribution.” The abstract says the same monitor reaches 68–75% attack coverage on some architectures and 6–13% on others (Table I lists 0.75 and 0.69 for the two best, 0.13 and 0.06 for the two Gemini models).

Let D be the probability distribution over distinct trigger-completion patterns and let p1≥p2… be its ordered probabilities. For a monitor with n invariants, Theorem 1 gives R(M,D)≤C_n(D)=Σ(i=1..n)p*i. Theorem 2 gives H(D)≥H_b(C_n(D)); therefore, the paper says, H(D)<1 bit implies C_n(D)>0.5 (§III-C). Inference: C_n is a ceiling, so the paper’s wording that any monitor then “achieves better-than-random coverage” overstates it; also the stated proof only shows H_b(C_n)<1, which excludes C_n=0.5 but not C_n<0.5 (the conclusion still holds because H(D) is at least the min-entropy, but the paper does not argue that). For an approximately uniform distribution over m patterns, Proposition 1 gives C_n≈n/m when n≪m. These are mathematical claims under the paper’s pattern model, not claims about arbitrary temporal properties.

technique 1: define and measure attack-pattern concentration

The paper defines an attack trajectory as an ordered tool-call sequence and extracts a trigger set T and forbidden completion t_c. Its monitor formula is ϕ = G(T_trig → F_[1,k](t_comp)) (Eq. 1, §II-A). Shannon entropy is H(D)=−Σp_i log2 p_i (Eq. 2), and top-n concentration is the sum of the n largest pattern probabilities. The procedure in §IV is:

1. Fix the monitor: eight LTL invariants mined from 847 adversarial trajectories collected on AgentDojo banking and workspace suites against GPT-4o-mini (temperature 0, seed 42).
2. Run the same red-team attack battery against each of eight backends, record each backend’s own trajectories, and extract trigger-completion pairs from the attacks the monitor did not block (Type II misses).
3. Cluster patterns by hierarchical agglomerative clustering on Jaccard distance with threshold θ=0.4.
4. Estimate the empirical distribution D-hat, Shannon entropy, and C_8(D-hat), with n=8 the deployed invariant count.
5. Compare with the recall of the eight-invariant sliding-window FSA monitor (window k=5, support σ=0.02, FPR threshold 0.05) on each backend.

The paper reports: “We mine the 8 LTL invariants from 847 adversarial trajectories collected on AgentDojo banking and workspace suites” (§IV). Inference: because D-hat is built only from attacks the monitor missed, it depends on the monitor, which sits uneasily with the paper’s claim that the bound is a property of the attack distribution alone. Inference: for VL, cluster recurring Verus failure shapes (for example, missing bounds invariants or quantifier-triggered solver failures), estimate their frequencies, and decide whether a fixed repair rule set can cover enough failures. This is a planning diagnostic, not a replacement for Verus proofs.

technique 2: use the entropy-coverage bound before adding invariants

Theorem 1’s proof relies on mutually exclusive patterns: each bounded-finally invariant detects one trigger-completion pair, so at most n patterns are covered and the best possible set is the n most probable. Inference: the steps below are this study’s reading of Theorem 1, not a procedure given in the paper:

1. Fix the invariant budget n and define the pattern alphabet precisely.
2. Estimate pattern probabilities from representative attack or failure traces.
3. Sort probabilities and compute C_n.
4. Treat C_n as the ceiling for any fixed n-invariant monitor, regardless of how invariants are mined.
5. Use the residual bound ASR_min(n)≥1−C_n to state unavoidable misses.

For high entropy, the paper says: “Monitor recall scales linearly with n/m and approaches zero as m ≫ n” (§III-B). Inference: a VL proof-repair policy with a fixed catalog of n templates faces the same capacity limit if real failures are spread over many unrelated proof obligations. Increasing template count helps only in proportion to concentration; adaptive or probabilistic retrieval may be needed for dispersed failures.

technique 3: pre-deployment entropy test and sample complexity

The paper turns the bound into a deployment decision. The protocol in §VI-A is:

1. Sample N_min=50 attack trajectories from the new backend by red-team or synthetic generation.
2. Extract and cluster trigger-completion patterns at θ=0.4.
3. Compute empirical entropy H-hat.
4. If H-hat<0.5 bits, deploy the FSA (expected recall above 50%); if H-hat>2.0 bits, use a probabilistic or neural monitor (expected recall below 20%); treat the interval between thresholds as requiring risk assessment.

Theorem 3 (§VI-C) gives the estimator guarantee N ≥ log2²(m-hat) ln(2/δ)/(2ε²) for error ε and confidence 1−δ. The paper calibrates ε=0.3 bits and δ=0.05: N≥51 for m-hat=3 (the conclusion writes m-hat≤3), and N≥226 for m-hat=10. Inference: the formula gives 51.5 and 226.2, so the integer bounds are 52 and 227; the paper rounds down. Inference: the proof treats the plug-in estimate’s per-trajectory terms as having mean H(D) and uses m-hat observed from the sample as the range, which the paper does not justify (the plug-in estimator is biased), so treat the guarantee as heuristic. It explicitly cautions: “Entropy estimates from 50–100 trajectories have ±0.3 bit uncertainty” (§VII-D). Inference: VL can run this test on a new codebase or model before committing to a fixed proof-repair catalog, but must re-estimate after toolchain or workload changes.

empirical evidence and arithmetic

Table I uses eight backends and the same n=8 monitor. DeepSeek-chat has H=0.19 bits, C8=0.98, and observed recall 0.75; gpt-4o-mini has 0.24, 0.97, and 0.69; Gemini 2.5 Flash has 2.81, 0.27, and 0.06. Across eight architectures, entropy and recall correlate at Pearson r=−0.87, p=0.005, explaining 76% of variance (§V-B; recomputing r from the Table I columns gives −0.87); bootstrap 95% CI is [−0.98,−0.78], and leave-one-out r ranges [−0.91,−0.82] (Table II). Elo capability is not significant (|ρ|<0.35, p>0.4).

The Gemini-2.5-Flash miss analysis has 135 unblocked attacks: seven clusters each cover at most 6.7%, and 81 attacks (60%) are singletons (Table III). Architecture-matched retraining changes recall by 0.0 percentage points while C8 remains 0.27 (§V-D). These denominators are explicit: 135 misses for the cluster percentages and eight architectures for the correlation. Inference: Table III does not fit the reported Gemini numbers. The seven clusters hold 54 of 135 misses, so the top 8 patterns would cover at least 40% rather than C8=0.27, and if the 81 singletons are separate patterns their entropy alone is about 4.2 bits rather than the reported 2.81 bits (the paper compares 2.81 to log2(7) for 7 equal clusters). The paper does not explain this. Inference: the result warns VL against using model capability or more mined examples as a proxy for proof-repair coverage.

what is trusted and where it fails

The theorem assumes fixed invariants and mutually exclusive observable patterns, each covered by one invariant. It does not cover adaptive monitors that periodically re-mine rules; the authors call that bound open. Attackers can deliberately inject entropy after observing the test. The threats section says that all trajectories are from AgentDojo banking, although §IV says banking and workspace suites; the paper states: “Attack entropy may differ in other domains; the test protocol should be re-applied per deployment context” (§VII-D). The paper says the low- versus high-entropy separation is stable for θ in [0.3, 0.5] (§IV). Two of eight mined invariants were suppressed at deployment for FPR>5% on benign tasks, reducing the effective invariant count from 8 to 6 and consuming about 20–28 percentage points of coverage capacity (§V-E). Inference: Table I still reports C_8 as the bound although the effective count was 6.

The monitor’s formal guarantee is about maximum recall under the model, not end-to-end safety. Tool-call semantics, attack labeling, benign distribution, FSA compilation, and the chosen LTL patterns remain trusted. Inference: threat to VL is medium. The entropy test is a useful capacity diagnostic for an agent that repairs verified Rust, but Verus’s proof checker still decides acceptance. A low-entropy proof-failure distribution does not prove that a repair is sound; a high-entropy distribution does not imply Verus is weak. The paper already derives and validates this monitor bound; VL should not redo it as a new theorem without changing the artifact or domain.

techniques for the catalog

• entropy-coverage bound — cap recall of an n-invariant fixed monitor by the probability mass of the n most frequent patterns
• attack-pattern clustering — extract trigger/completion patterns, cluster by Jaccard similarity, and estimate concentration and entropy
• pre-deployment entropy test — sample 50 or more traces, estimate entropy, and route low-entropy backends to FSA monitors and high-entropy backends to probabilistic monitors
• sample-complexity guarantee — choose trace count from log2²(m) ln(2/δ)/(2ε²) to bound entropy-estimation error Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Fig. 1 demonstrates a clean decoupling: Elo scores (capability proxy) span 1070–1330 with no significant correlation to monitor coverage, while entropy explains coverage almost entirely.”): read all 400 lines of the paper text; checked every quotation, section reference, equation and theorem statement, Table I-III numbers, the 76% variance figure, the Pearson r (recomputed from Table I: −0.87), the Theorem 3 sample sizes (recomputed: 51.5 and 226.2), the cluster sums (54+81=135) and the tag and arXiv link; changed the technique 1 procedure order (monitor mined from GPT-4o-mini, then red-team on eight backends, distribution from missed attacks), removed the unstated stationarity assumption, added section references, and added Inference notes on the Theorem 2 wording, Theorem 3 rounding and proof gaps, Table III inconsistency, effective invariant count, and the banking-only versus banking-plus-workspace wording; did not check the cited external works, Elo values, or the VL applicability claims beyond marking them as inference.

Last edited: 2026-10-17