SMTrap Uses SMT Conflicts to Stall Reasoning LLMs

Problem

The paper studies how to cheaply induce denial-of-service style resource exhaustion in large reasoning models by causing them to perform long, inference-heavy chain-of-thought reasoning. Prior black-box attacks require repeated queries or costly attacker-model training, reducing attacker leverage. The work asks whether low-cost, model-feedback-free signals can guide synthesis of benign-looking constraint satisfaction problems (CSPs) that force extensive trial-and-backtracking search in deployed models, substantially increasing token usage and latency.

Approach

The authors introduce search amplification, a paradigm that uses the conflict count reported by an SMT solver (Z3) as an external, low-cost proxy for the amount of backtracking a CSP will induce in a large reasoning model. They implement SMTrap, a CPU-only framework that starts from a valid solution and an initial clue state, then iteratively branches and prunes clues to produce candidate clue states. Each candidate is encoded as an SMT formula and evaluated with Z3 for satisfiability, uniqueness and conflict count. SMTrap greedily accepts valid candidates with higher conflict counts, preserving unique solvability and clue count. Final clues are rendered as natural-language puzzles (Sudoku, zebra puzzles, and preliminarily graph colouring) with optional shortcut-suppression instructions to prevent tool-based shortcuts on web interfaces. SMTrap requires no model queries, no GPU training, and runs on commodity CPUs.

Key Findings

• SMT conflict counts positively correlate with explicit trial-and-backtracking behaviours in LRMs and with completion length; higher conflict levels generally produce longer outputs and more constraint checks, assignment proposals, contradiction handling and branch revisions.
• SMTrap achieves state-of-the-art LRM-DoS performance across seven frontier models. SMTrap-Zebra averaged 76,362 completion tokens across seven LRMs and outperformed AutoDoS, ReasoningBomb and CatAttack by roughly 2.74×, 2.89× and 5.70× respectively; SMTrap-Sudoku reached a 270.65 amplification ratio and about 1,331 seconds average reasoning time in API tests.
• Web-interface experiments showed practical impact: on GPT-5.5 SMTrap-Sudoku produced 314.97 seconds of reasoning time and on GPT-5.4 SMTrap-Zebra reached 1,308.33 seconds, exceeding baselines by large factors. SMTrap synthesis is inexpensive (tens of seconds of CPU time) while induced inference can last dozens of minutes.
• SMTrap payloads are largely stealthy at prompt level: an external classifier labelled 83.33% of generated queries as normal; Sudoku prompts were all classified as normal while some zebra puzzles were flagged due to unusually large problem size.
• A simple tool-based defence that routes CSP inputs to bounded local solvers and returns solver output directly reduced token usage by about 90.15% on average and achieved reductions of 97.08% and 84.03% for SMTrap-Sudoku and SMTrap-Zebra on GPT-5.5.

Limitations

Experiments focus on CSP-style tasks (Sudoku, zebra puzzles, graph colouring) under fixed encodings and a single SMT solver configuration; conflict counts depend on encoding, solver heuristics and parameters. Web-interface measurements can be affected by service load and interface-specific limits. The study does not release a full corpus of high-risk prompts to limit misuse.

Implications

An attacker can cheaply generate benign-looking puzzles that steer a model into prolonged trial-and-backtracking reasoning without querying the target model or training attack models, creating a practical availability threat that scales on commodity CPUs. The attack exploits a cost asymmetry between inexpensive symbolic synthesis and expensive neural inference, suggesting providers should route high-search structured queries to bounded solvers, apply task-aware cost estimation and enforce bounded reasoning rather than relying solely on prompt-level filtering.