SMTrap: Cost-Effective DoS Attacks Against Large Reasoning Models via SMT Conflict Guidance

Researchers propose SMTrap, a CPU-only framework that uses Satisfiability Modulo Theories (SMT) solver conflict counts to generate inference-heavy Constraint Satisfaction Problem (CSP) instances, enabling cost-effective denial-of-service (DoS) attacks against large reasoning models (LRMs) without model queries or GPU computation. Evaluations across seven frontier models show SMTrap produces DoS effects multiple times stronger than existing baselines, and a tool-based mitigation significantly reduces token usage.

arXiv:2608.18921v1 Announce Type: new Abstract: 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.