AI 中文总结
本研究提出基于SMT冲突引导的轻量级CPU框架SMTrap，无需模型查询或GPU即可生成高影响力CSP查询，实现强于基线数倍的LRM-DoS攻击，还展示了对应的缓解工具
AI 中文摘要
现有的大型推理模型拒绝服务（LRM-DoS）方法严重依赖模型反馈来合成攻击查询，要么需要对目标模型进行重复查询，要么需要训练专用的攻击模型，这些高成本操作极大地削弱了攻击的影响力。在本文中，我们提出了一种新颖的无模型反馈的LRM-DoS范式——“搜索放大（search amplification）”，它采用可满足性模理论（SMT）求解器得出的冲突计数作为低成本外部信号，来指导推理密集型约束满足问题（CSP）实例的合成。我们的关键观察是，LRM在求解CSP时依赖试错回溯搜索，给定CSP实例上更高的SMT冲突计数与更广泛的LRM回溯搜索以及显著更长的输出轨迹呈正相关。基于这一发现，我们提出了轻量级、仅CPU运行的框架SMTrap。在SMT冲突计数的引导下，SMTrap无需模型查询、攻击模型训练或GPU计算即可生成推理密集型CSP查询。对7个前沿模型的评估表明，SMTrap具备最先进的LRM-DoS能力，产生的DoS效应比现有基线强数倍。为缓解SMTrap的威胁，我们展示了一种基于工具的缓解措施，可大幅减少令牌使用量。
英文摘要
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.
