用SMT冲突数引导生成推理负担重的查询，低成本实现大模型拒绝服务攻击。
SMTrap: Cost-Effective DoS Attacks Against Large Reasoning Models via SMT Conflict Guidance
- 基于SMT求解器的冲突计数，无需模型反馈生成攻击查询
- 在7个前沿模型上攻击效果是基线的数倍，且不需GPU或训练
- 适合研究模型安全与防御机制的团队关注
现有大型推理模型拒绝服务攻击方法严重依赖模型反馈来生成攻击查询，需反复调用目标模型或训练专用攻击模型，成本高昂。本文提出「搜索放大」新范式，完全不依赖模型反馈。该方法利用满足可判定理论（SMT）求解器的冲突计数作为低成本外部信号，指导生成高推理负载的约束满足问题（CSP）实例。关键观察发现：模型在求解CSP时采用试错回溯搜索，而更高冲突计数的实例会引发更深度的回溯和更长的输出轨迹。基于此，我们设计轻量级纯CPU框架SMTrap，仅凭SMT冲突数即可生成高负载查询，无需模型调用、攻击模型训练或GPU计算。在七个前沿模型上的评估显示，SMTrap攻击效果显著优于现有基线，达到数倍更强的拒绝服务能力。为应对该威胁，我们还提出一种基于工具的缓解方案，可大幅降低模型令牌使用量。
原文摘要 · Abstract (English)
Existing LRM-DoS methods rely heavily on model feedback to synthesize attack queries, requiring either repeated queries to the target model or training a dedicated attack model. These expensive operations severely weaken attack leverage. In this paper, we propose \emph{search amplification}, a novel, model-feedback-free LRM-DoS paradigm. It employs the conflict count derived from an Satisfiability Modulo Theories (SMT) solver as a low-cost external signal to guide the synthesis of inference-heavy Constraint Satisfaction Problem (CSP) instances. Our key observation is that LRMs depend on trial-and-backtracking search when solving CSPs, where higher SMT conflict counts on a given CSP instance positively correlate with more extensive LRM backtracking search and substantially longer output trajectories. Building on this finding, we propose \textsc{SMTrap}, a lightweight, CPU-only framework. Guided by SMT conflict counts, \textsc{SMTrap} generates inference-heavy CSP queries without model queries, attack-model training, or GPU computation. Evaluations across seven frontier models demonstrate the state-of-the-art LRM-DoS capability of \textsc{SMTrap}, producing DoS effects multiple times stronger than existing baselines. To mitigate the threat of \textsc{SMTrap}, we demonstrate a tool-based mitigation that significantly cuts token usage.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。