这篇论文说清了同一安全监控器在GPT/DeepSeek上能拦七成攻击、在Gemini上几乎失灵的原因，还给了部署前预测覆盖率的测试。
基于线性时序逻辑(LTL)和有限自动机(FSA)的运行时监控器用于拦截LLM智能体的不安全工具调用序列。研究发现同一监控器在GPT类和DeepSeek后端上攻击覆盖率约68-75%，在Gemini变体上仅6-13%。攻击分布的Shannon熵差异解释了这一差距：GPT类集中（H≈0.24比特，单个模式覆盖96%），Gemini分散（H≈2.81比特，7个簇各≤7%）。熵对覆盖率变异解释率为76%（Pearson r=-0.87，p=0.005），留一法验证r在[-0.91,-0.82]。论文提出部署前熵测试，可从小样本攻击数据预测监控覆盖率。
Why Formal Monitors Fail: Attack Distribution Entropy as a Coverage Bound for LTL-Based LLM Agent Safety
Runtime safety monitors based on Linear Temporal Logic (LTL) and finite automata (FSA) are increasingly deployed to intercept unsafe tool-call sequences in LLM agents. Yet the same monitor achieves 68-75% attack coverage on some model architectures and near-zero on others, with no explanation from capability scores, training data, or prompt design. We provide the missing theory. We prove that the recall of any fixed-invariant FSA monitor is bounded above by the concentration of the attack distribution: the fraction of attacks covered by the k most frequent trigger-completion patterns. When attacks concentrate (low Shannon entropy), a small fixed invariant set achieves high recall; when they disperse across many structurally distinct patterns (high entropy), no fixed invariant set of tractable size can, regardless of how the invariants were derived. We validate this entropy-coverage bound across eight frontier LLM architectures. GPT-class and DeepSeek backends yield highly concentrated attacks (H ~ 0.24 bits; one pattern covers 96%), explaining 68-75% recall; Gemini variants yield high-entropy distributions (H ~ 2.81 bits; 7 clusters each <= 7%), explaining near-zero recall (6-13%), invariant to architecture-matched retraining. Entropy accounts for 76% of variance in coverage (Pearson r = -0.87, p = 0.005, 95% CI [-0.98, -0.78]), holding under leave-one-out (r in [-0.91, -0.82]). We introduce a pre-deployment entropy test that predicts monitor coverage from a small attack sample, enabling architecture-aware monitor selection before deployment. The bound and test are architecture-agnostic and apply to any FSA-based runtime monitor over discrete action sequences.