SMTrap: Cost-Effective DoS Attacks Against Large Reasoning Models via SMT Conflict Guidance
Organizations: School of Information, Renmin University of China, Beijing, China · Beijing Advanced Innovation Center for Future Blockchain and Privacy Computing, Beihang University, Beijing, China · Xreal, Beijing, China · GigaAI, Beijing, China
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 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 SMTrap, a lightweight, CPU-only framework. Guided by SMT conflict counts, 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 SMTrap, producing DoS effects multiple times stronger than existing baselines. To mitigate the threat of SMTrap, we demonstrate a tool-based mitigation that significantly cuts token usage.
Figures & tables
| Method | Venue | Amp. | Steal. | Opt. | L.C. | H.T. |
| AutoDoS | ACL 2025 | ✗ | ✓ | ✗ | ✗ | ✗ |
| CatAttack | COLM 2025 | ✗ | ✓ | ✗ | ✗ | ✗ |
| ReasoningBomb | CCS 2026 | ✓ | ✓ | ✓ | ✗ | ✗ |
| SMTrap(Ours) | – | ✓ | ✓ | ✓ | ✓ | ✓ |
| Method | Venue | Claude Opus-4.7 | GPT 5.5 | Gemini 3.1-pro | Deepseek v4-pro | GLM 5.1 | MiniMax M2.7 | Kimi K2.6 | Avg. | BNTS | Amp. | Gene. Plat. |
| AutoDoS | ACL 2025 | 35,854 302 s | 9,734 187 s | 20,915 186 s | 35,418 901 s | 38,682 922 s | 25,590 424 s | 28,825 – s | 27,860 487 s | 18.10% | 5.99 | API/GPU |
| CatAttack | COLM 2025 | 1,067 9 s | 2,291 44 s | 11,205 96 s | 21,186 623 s | 17,279 363 s | 22,931 399 s | 17,784 – s | 13,392 255.67 s | 7.96% | 23.25 | API/GPU |
| ReasoningBomb | CCS 2026 | 5,739 47 s | 2,491 50 s | 14,388 235 s | 69,644 1876 s | 31,354 621 s | 34,944 535 s | 26,315 – s | 26,411 560.67 s | 14.05% | 124.58 | GPU |
| SMTrap -Sudoku | – | 59,191 425 s | 28,942 418 s | 32,392 303 s | 109,300 3530 s | 115,334 2029 s | 77,041 1282.6 s | 75,354 – s | 71,079 1,331.16 s | 44.17% | 270.65 | CPU |
| SMTrap -Zebra | – | 124,522 814 s | 31,029 478 s | 28,663 288 s | 91,677 2787 s | 80,271 1282 s | 85,593 1472.4 s | 92,776 – s | 76,362 1,186.9 s | 48.78% | 77.61 | CPU |
| Method | GPT-5.5 | GPT-5.4 |
| AutoDoS | 14.92 | 53.33 |
| CatAttack | 25.50 | 54.57 |
| ReasoningBomb | 36.33 | 69.67 |
| SMTrap -Sudoku | 314.97 | 880.20 |
| SMTrap -Zebra | 183.77 | 1308.33 |
| Task | Conflict Level | Shortcut Suppression | GPT-5.5 Web | GPT-5.5 API |
| Sudoku | Low(12) | w/o | 74.33 | 20,941 |
| Low(12) | w/ | 224.53 | 21,380 | |
| High(24) | w/o | 144.42 | 27,176 | |
| High(24) | w/ | 314.97 | 28,942 | |
| Zebra | Low(12) | w/o | 55.12 | 23,125 |
| Low(12) | w/ | 150.65 | 22,096 |
| Setting | SMTrap -Sudoku | SMTrap -Zebra | Average |
| w/o Tool Defense | 27,766 | 31,478 | 29,622 |
| w/ Tool Defense | 810 | 5,026 | 2,918 |
| 97.08% | 84.03% | 90.15% |
Appendix figures & tables9 assets
Supplementary material from the paper’s appendix.
Appendix
| Query Set | #Q | Normal | Malicious | Stealth. |
| AutoDoS | 12 | 2 | 10 | 16.67% |
| CatAttack | 30 | 15 | 15 | 50.00% |
| ReasoningBomb | 30 | 24 | 6 | 80% |
| SMTrap -Sudoku | 30 | 30 | 0 | 100.00% |
| SMTrap -Zebra | 30 | 20 | 10 | 66.67% |
| SMTrap -Overall | 60 | 50 | 10 | 83.33% |
| Variant | Avg. Time | CPU | Branches/Iter. |
| SMTrap -Sudoku | 35.8s | Ultra 9 285H | 5 |
| SMTrap -Zebra | 46.1s | Ultra 9 285H | 5 |
| Task | Conflicts | Decisions | Propagations |
| Sudoku | 0.90 | 0.52 | 0.48 |
| Zebra | 0.79 | 0.55 | 0.51 |
| Task | Low-Conflict | High-Conflict |
| Graph Coloring | 20,127 | 35,712 |
| Method | Generation | Claude Opus-4.7 | GPT 5.5 | Gemini 3.1-pro | Deepseek v4-pro | GLM 5.1 | MiniMax M2.7 | Kimi K2.6 | Avg. | BNTS |
| Sudoku-Bench | Manual design | 69,247 | 15,569 | 30,539 | 124,031 | 47,675 | 73,157 | 114,892 | 67,873 | 40.86% |
| Puzzle-Bench | Manual design | 52,404 | 25,594 | 29,311 | 58,792 | 98,519 | 62,928 | 50,450 | 54,000 | 35.28% |
| SMTrap -Sudoku | CPU symbolic | 59,191 | 28,942 | 32,392 | 109,300 | 115,334 | 77,041 | 75,354 | 71,079 | 44.17% |
| SMTrap -Zebra | CPU symbolic | 124,522 | 31,029 | 28,663 | 91,677 | 80,271 | 85,593 | 92,776 | 76,362 | 48.78% |
| Behavior | Operational definition | Representative common patterns | Representative task-specific patterns |
| Propose assignments | Introduces a tentative value, assignment, candidate, case, or hypothesis for subsequent evaluation. | assume , suppose , let’s try , consider , maybe , candidate , tentative , guess , place , set , assign , fill | Sudoku: explicit cell assignments such as r3c5 = 7 or (3,5) = 7 . Zebra: tentative house–attribute assignments such as House 2 nationality = ... . |
| Check constraints | Performs deduction, verification, enumeration, elimination, or constraint checking without explicitly reporting a contradiction. | therefore , must be , cannot be , implies , because , eliminate , verify , check , consistent with , possible values , remaining | Sudoku: references to rows, columns, boxes, cells, candidate sets, digits, or the grid. Zebra: references to clues, houses, adjacency, left/right relations, attributes, or constraints. |
| Encounter contradictions | Identifies an invalid, inconsistent, impossible, or rule-violating partial assignment. | contradiction , conflict , impossible , invalid , inconsistent , no solution , dead end , violate , duplicate , fails | Shared contradiction expressions are used for both Sudoku and Zebra-Game. |
| Revise failed branches | Withdraws, rejects, or modifies a previous assignment or branch after it fails. | backtrack , undo , retract , go back , try again , reconsider , instead , reassign , rule out , revise , reject | Case-transition expressions such as Case B , try another , and try a different ... are used for both tasks. |
| 6 | 1 | 2 | 7 | 9 | 8 | 3 | 5 | 4 |
| 5 | 4 | 3 | 2 | 6 | 1 | 7 | 9 | 8 |
| 9 | 8 | 7 | 3 | 5 | 4 | 2 | 6 | 1 |
| 3 | 5 | 8 | 4 | 2 | 6 | 1 | 7 | 9 |
| 2 | 6 | 4 | 1 | 7 | 9 | 8 | 3 | 5 |
| 7 | 9 | 1 | 8 | 3 | 5 | 4 | 2 | 6 |
| 1 | 7 | 6 | 9 | 8 | 3 | 5 | 4 | 2 |
| Attribute | H1 | H2 | H3 | H4 | H5 | H6 | H7 | H8 | H9 |
| Color | Orange | Purple | Yellow | Blue | Pink | Green | Red | White | Brown |
| Nationality | Italian | Danish | German | French | Spanish | English | Japanese | Swedish | Norwegian |
| Drink | Juice | Lemonade | Soda | Wine | Tea | Water | Beer | Coffee | Milk |
| Cigarette | Dunhill | Blends | PallMall | Lucky | Prince | Marlboro | Rothmans | Camel | BlueMaster |
| Pet | Horse | Turtle | Rabbit | Dog | Bird | Fish | Hamster | Cat | Zebra |
| Hobby | Fishing | Music | Reading | Gardening | Cooking | Sports | Chess | Painting | Dancing |
Adversarial Attacks on LLMs
Adversarial attacks on large language models probe how crafted inputs, internal changes, and agent interactions bypass safety or disrupt reliable behavior.
See all 355 papers