PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Jian Yang, Zhenqi Feng, Zhaoyang Yu, Zhaoxin Fan, Kejian Wu, Xiaofeng Wang, Zheng Zhu, Jianjun Huang, Wei You, Bin Liang

arXiv:2608.18921v1cs.CLcs.AI

TL;DR

Existing LRM-DoS attacks require costly model feedback, limiting low-cost query generation. SMTrap instead uses SMT conflict counts to synthesize inference-heavy CSP queries, achieving substantially stronger DoS effects than existing baselines across frontier models.

  • Problem

    Existing LRM-DoS attacks depend on costly model feedback, motivating effective query generation without repeated target queries or attack-model training.

  • Method

    SMTrap uses CPU-only SMT conflict counts as a model-feedback-free signal to synthesize valid, inference-heavy CSP queries that induce LRM backtracking.

  • Results

    More than 2× the average output length of the strongest baseline was achieved across seven frontier LRMs, while web-interface tests increased reasoning time by at least 5×.

  • Takeaways & Limitations

    SMTrap exposes search amplification as a practical and potentially damaging resource-amplification threat to current LRM deployments.

  • Takeaways & Limitations

    The approach assumes CSP solving induces explicit search rather than generic verbosity, a premise examined using reasoning traces from one model.

Abstract

from arXiv · show

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.

1 Introduction

SMTrap introduces search amplification, a model-feedback-free LRM-DoS paradigm that uses CPU-side SMT conflict counts to synthesize inference-heavy CSP queries. Across seven frontier LRMs, it achieves state-of-the-art attack performance while substantially reducing attack-generation costs.

  • Motivation: A single short query can trigger reasoning outputs hundreds of times longer than its input, creating strong attacker-to-provider computational leverage.LRMs consume substantially more inference-time computation because they generate lengthy Chain-of-Thought trajectories.
  • Limitations of Existing Attacks: Existing black-box LRM-DoS attacks rely on target-model or surrogate-model feedback, requiring costly query generation, computation, and often GPU resources.Perturbation-based methods iteratively evaluate candidates, while ReasoningBomb trains an attack LLM using behavioral data and reinforcement learning.
  • Search Amplification: Search amplification uses SMT conflict counts as a low-cost external signal to guide generation of CSP instances that induce explicit over-reasoning in models.The SMT solver serves as a pseudo-surrogate model, replacing model feedback with cheap CPU-side solving.
  • SMTrap: SMTrap exploits the positive correlation between SMT conflict counts and LRM backtracking search to synthesize valid, uniquely solvable, inference-heavy CSP queries.It requires neither model queries nor attack-model training and runs as a lightweight, CPU-only framework without GPU computation.
  • Evaluation: More than 2× average output length and at least 5× reasoning time demonstrate SMTrap’s state-of-the-art LRM-DoS performance across seven frontier models.On the official OpenAI web interface, synthesized queries forced GPT-5.5 and GPT-5.4 to reason for dozens of minutes.

2 Related Work

Prior black-box LRM-DoS attacks use perturbation- or generation-based synthesis, often relying on model feedback, while reasoning benchmarks mainly assess accuracy rather than inference cost. Structured puzzles and CSPs have recently emerged as controlled environments for studying reasoning behavior.

  • Black-Box LRM-DoS attacks: Black-box LRM-DoS attacks mainly follow perturbation-based or generation-based paradigms.Perturbation methods modify query wording, embeddings, or triggers to search for DoS payloads.
  • Black-Box LRM-DoS attacks: Perturbation-based attacks can induce long responses but typically require victim- or surrogate-model feedback, making synthesis costly and prone to model-specific overfitting.They evaluate candidate prompts by modifying query wording, embeddings, or triggers.
  • Reasoning Benchmarks: Reasoning benchmarks include mathematical, multi-step, and logical tasks, but primarily measure reasoning accuracy rather than inference cost.Examples include GSM8K, MATH, BIG-Bench Hard, ReClor, LogiQA, ProofWriter, and FOLIO.
  • Reasoning Benchmarks: Structured puzzles and CSPs have recently been used as controlled environments for studying reasoning behavior.The passages identify ZebraLogic as the most similar prior work in this area, though the supplied text is truncated before describing it further.

3 Threat Model

The threat model considers a black-box attacker seeking to induce excessive inference costs in LRM services through benign-looking reasoning queries. Attack cost is assessed using observable proxies, while query synthesis occurs offline without access to internal model or provider information.

  • Attacker goal: The attacker aims to induce excessive inference cost from an LRM service using benign-looking reasoning queries.The stated cost proxies include output length and elapsed reasoning time.
  • Access assumptions: The attacker operates through a public web interface or API in a black-box setting.The attacker has no access to model weights, gradients, logits, hidden states, system prompts, decoding settings, or provider-side telemetry.
  • Attack construction: The attacker synthesizes queries offline using only inexpensive computation.

4 Search Amplification

Search amplification is grounded in evidence that CSP solving elicits trial-and-backtracking search in LRMs. SMT conflict counts provide a model-feedback-free signal because higher-conflict instances induce more explicit search and generally longer outputs.

  • Explicit Search in CSP Solving: 85.2% of Sudoku traces and 96% of zebra-puzzle traces comprise search-related behaviors, supporting the premise that CSP solving elicits explicit LRM search.Deepseek-v4-pro traces were analyzed over 200 randomly generated instances for each task.
  • SMT Conflict Guidance: SMT conflict count serves as a low-cost external signal for estimating LRM backtracking search without querying the target model.CSPs are encoded as SMT formulas, and conflicts reflect contradictions requiring search revision under shared constraints.
  • Conflict Counts Predict Outputs: Across Sudoku, zebra puzzles, and three LRMs, completion length generally increases with conflict level, with consistently positive Pearson and Spearman correlations.The trends are not strictly monotonic, but conflict count remains useful for identifying instances likely to induce higher inference cost.
  • Conflict Counts Predict Search: Higher conflict levels are associated with more explicit search behaviors, while search behavior count strongly correlates with completion length.The supported relationship is higher SMT conflict → more explicit LRM search → longer completion.
  • Inference-Cost Amplification: Higher-conflict instances increase inference cost through more assignment attempts, constraint checks, contradictions, and branch revisions.Conflict count is more predictive of LRM output length than decisions and propagation counts.

5 SMTrap

SMTrap is a CPU-only framework that synthesizes inference-heavy CSP queries by searching clue states with SMT conflict guidance. It preserves validity, unique solvability, and clue count while rendering high-conflict states with optional shortcut-suppression instructions.

  • Framework overview: SMTrap uses four components: CSP initialization, clue branching and pruning, conflict-guided acceptance, and shortcut suppression.The search runs on CPUs, can vary hidden solutions and random seeds, and generates diverse instances without changing task size.
  • SMTrap objective: SMTrap searches for a clue state C⋆ with higher conflict count than C0 while preserving satisfiability, unique solvability, and the original clue count.These constraints respectively ensure validity, exclude alternative solutions, increase conflict, and keep task size unchanged.
  • Clue-state search: Starting from a solution-consistent clue state, SMTrap adds one valid clue and removes one visible clue to preserve count while exploring neighboring states.Sudoku branches reveal hidden cells, while zebra-puzzle branches add valid relational clues; pruning reverses the clue composition change.
  • Query rendering and suppression: SMTrap renders the selected clue state as a natural-language CSP query and appends instructions to solve manually, reason step by step, verify constraints, and avoid code or external solvers.Shortcut suppression targets web-facing LRMs with tool access; in API settings without built-in tools, enabling it has limited effect because the high-conflict CSP remains the main amplification source.

6 Experiments

Experiments across seven frontier LRMs show that SMTrap substantially increases API-visible output cost and web-interface reasoning time, outperforming recent LRM-DoS baselines. Ablations support conflict count and shortcut suppression as key factors, while tool-based solver routing sharply reduces token usage.

  • Experimental setup: SMTrap was evaluated on seven frontier LRMs using API completion tokens, reasoning time, BNTS, web-interface reasoning time, and amplification ratio.The victim models were Claude-Opus-4.7, GPT-5.5, Gemini-3.1-pro, Deepseek-v4-pro, GLM-5.1, MiniMax-M2.7, and Kimi-K2.6.
  • API-level results: 76,362 average completion tokens made SMTrap-Zebra 2.74×, 2.89×, and 5.70× stronger than AutoDoS, ReasoningBomb, and CatAttack, respectively.SMTrap-Sudoku also achieved the best 270.65 amplification ratio and 1,331.16 seconds average reasoning time.
  • Web-interface results: 314.97 seconds on GPT-5.5 made SMTrap-Sudoku outperform AutoDoS, CatAttack, and ReasoningBomb by 21.11×, 12.35×, and 8.67×, respectively.On GPT-5.4, SMTrap-Zebra reached 1308.33 seconds and exceeded the same baselines by 24.54×, 23.97×, and 18.78×.
  • Ablation studies: Increasing conflict count consistently raised web reasoning time and API completion length across Sudoku and Zebra, with or without shortcut suppression.Without shortcut suppression, Sudoku increased from 74.33s to 144.42s in reasoning time and from 20,941 to 27,176 tokens in API output length.
  • Ablation studies: Shortcut suppression increased high-conflict web reasoning time from 144.42s to 314.97s for Sudoku and from 78.36s to 183.77s for Zebra.Without suppression, web models may generate and execute solver code, bypassing the CSP-induced search process.
  • Mitigation: 97.08% and 84.03% reductions in total token usage for SMTrap-Sudoku and SMTrap-Zebra yielded a 90.15% average reduction under tool-based solver routing on GPT-5.5.The defense routes Sudoku and zebra puzzle queries to local bounded solvers and returns solver output directly.

7 Conclusion · A Details of Tool-based Mitigation

SMTrap introduces model-feedback-free search amplification, using SMT conflict counts to generate inference-heavy CSP queries that induce extensive LRM backtracking and longer outputs. Its tool-based mitigation routes CSP solving to bounded local computation and directly returns solver results, reducing opportunities for unrestricted reasoning-based denial of service.

  • 7 Conclusion: SMTrap uses SMT conflict counts as a low-cost external signal to synthesize inference-heavy CSP queries without model feedback.The framework is CPU-only and targets valid, uniquely solvable CSP instances.
  • 7 Conclusion: Higher SMT conflict counts positively correlate with more extensive LRM trial-and-backtracking search and longer outputs.This relationship motivates search amplification as an LRM-DoS paradigm.
  • A Details of Tool-based Mitigation: The mitigation uses an agent-style API in which the LRM routes CSP requests while bounded local computation performs the actual solving.The model receives the original query, a defense prompt, and an exposed solve_csp tool; the host executes the tool locally.
  • A Details of Tool-based Mitigation: The defense policy requires solve_csp for Sudoku and Zebra-style tasks, separating CSP solving from model generation.It prevents unrestricted manual search and returns bounded solver output without asking the LRM to rewrite the solution.
  • A Details of Tool-based Mitigation: Canonicalization converts raw input into structured CSP representations before local solving, while valid canonical JSON can bypass this step.Sudoku uses a 9 × 9 grid, whereas Zebra puzzles encode houses, attributes, constraints, and an optional query.
  • A Details of Tool-based Mitigation: Local solvers handle Sudoku and Zebra CSPs, and any requested derivation trace is generated locally and capped by max_trace_steps.Sudoku uses minimum-remaining-value backtracking; Zebra solving uses finite-domain assignments and can use Z3 for constraint solving and uniqueness verification.
  • A Details of Tool-based Mitigation: Direct-return execution sends solver answer_text straight to the user without another LRM generation round, keeping response length under application control.A host-side fallback can invoke solve_csp when the model fails to call the tool, including when prompts request manual reasoning.
  • A Details of Tool-based Mitigation: The mitigation specifically targets unrestricted natural-language solving of structured high-search CSPs rather than eliminating all possible LRM-DoS attacks.The reported results support combining task-aware routing, bounded solving, and direct-return execution instead of relying only on prompt filtering.

B Stealthiness Evaluation … C.2 Web-Interface Evaluation Protocol

SMTrap queries resemble ordinary reasoning tasks yet achieve high stealthiness against a reasoning-exhaustion detector, while SMT-guided synthesis uses lightweight CPU-side search and web-interface measurements quantify user-facing reasoning cost. The appendices detail the synthesis controls, limitations, and evaluation protocols.

  • B Stealthiness Evaluation: SMTrap achieved 83.33% stealthiness, with 50 of 60 queries classified as NORMAL by GPT-4o.This exceeded AutoDoS (16.67%) and CatAttack (50.00%) and was comparable to ReasoningBomb (80%).
  • B Stealthiness Evaluation: All Sudoku queries were classified as NORMAL, while Zebra-style misclassifications mainly reflected unusually many houses, attributes, and relational clues.The queries contained no harmful instructions, adversarial suffixes, gibberish, or explicit infinite-loop requirements.
  • B Stealthiness Evaluation: Prompt-level filtering alone is insufficient because SMTrap constructs benign-looking reasoning tasks whose intrinsic search spaces induce high inference cost.The appendix identifies task-aware cost estimation and bounded solving as practical defenses.
  • C Additional Details: The appendices provide implementation details for SMT conflict-guidance validation and SMTrap synthesis.These details accompany the stealthiness and web-interface evaluations.
  • C.1 Synthesis Details and Cost: Validation controls task size and rendered prompt length within each family, using 9 × 9 Sudoku grids and Zebra puzzles with nine houses, categories, and values.Evaluated instances are rendered as normal CSP queries with comparable input lengths.
  • C.1 Synthesis Details and Cost: SMTrap treats Z3 conflict count as a predictive guidance signal rather than an independently manipulated causal variable.Visible clues are sampled randomly, so clue counts vary across instances and conflict levels.
  • C.1 Synthesis Details and Cost: SMTrap generates five candidate clue states per iteration, validates satisfiability and unique solvability with Z3, and greedily accepts the valid candidate with the highest improving conflict count.The search stops at empirical thresholds of 3,000 conflicts for Sudoku or 5,000 for Zebra-Game, or when the iteration budget is exhausted.
  • C.2 Web-Interface Evaluation Protocol: Web-interface evaluation manually tested GPT-5.5 and GPT-5.4 in their strongest available thinking modes through the official OpenAI interface.Each query was submitted three times, and mean elapsed reasoning time was measured from submission until completion or the interface reasoning limit.

C.3 Comparison of Z3 Search Metrics · C.4 Generalization Beyond Sudoku and Zebra · D Discussion

SMTrap’s conflict count is more predictive of LRM output length than other Z3 activity metrics, and preliminary graph-coloring results suggest search amplification extends beyond Sudoku and Zebra-Game. The discussion frames this as a low-cost attack enabled by a symbolic–neural cost asymmetry and motivates task-aware defenses.

  • C.3 Comparison of Z3 Search Metrics: Decisions and propagations show only moderate correlations with LRM output length, around 0.5, and are consistently weaker than Z3 conflict count.The comparison uses 12 discretized metric levels and Pearson correlation on Sudoku and Zebra-Game.
  • C.3 Comparison of Z3 Search Metrics: Conflict count better captures contradictory regions and failed branches that LRMs externalize through contradiction checking, branch revision, and backtracking.
  • C.4 Generalization Beyond Sudoku and Zebra: Search amplification requires a symbolic search space whose difficulty can increase while preserving a benign-looking query form, rather than being inherently tied to Sudoku or Zebra-Game.These two tasks are used as controlled CSP testbeds with symbolic encodings, validity checks, and natural-language renderings.
  • C.4 Generalization Beyond Sudoku and Zebra: High-conflict graph-coloring instances induce substantially longer LRM outputs than low-conflict instances under the same task family.The instances are valid and solvable, and the experiment compares graph-coloring problems constructed with different conflict levels.
  • C.4 Generalization Beyond Sudoku and Zebra: The graph-coloring result suggests search amplification can arise in structured reasoning tasks requiring explicit search, constraint verification, and backtracking.The evidence is preliminary and limited to one additional CSP family.
  • D Discussion: SMTrap introduces a low-cost DoS paradigm that increases intrinsic symbolic search pressure in benign-looking CSP queries, causing LRMs to externalize extensive search behavior.The discussion contrasts this approach with attacks targeting prompt wording, adversarial triggers, or attacker-generated prompts.
  • D Discussion: The risk reflects a broader mismatch between cheap symbolic task construction and expensive neural test-time reasoning, rather than dependence on a specific puzzle format.The discussion cites similar low-versus-high conflict gaps in graph coloring alongside Sudoku and Zebra-Game testbeds.
  • D Discussion: Task-aware routing is proposed as a first-line defense, using bounded solvers, reasoning budgets, concise verified answers, task-level cost estimation, and solver-assisted verification.The goal is to prevent models from externalizing an unbounded search trace on structured high-search tasks.

E Ethics, Responsible Disclosure, and Limitations

The study uses controlled evaluations, limits release of high-risk attack artifacts, and frames SMTrap as a mitigation-oriented analysis of a dual-use threat. Its evidence is limited to CSP-style tasks, with Z3 conflict count serving as a practical solver-side proxy rather than a complete difficulty measure.

  • Controlled evaluation: All experiments use bounded queries or manually recorded web-interface reasoning time, without traffic flooding, account abuse, or disruption of real services.API evaluations measure output-token usage under fixed protocols; web-interface evaluations record elapsed reasoning time.
  • Responsible release: The authors will not publicly release a complete high-risk prompt corpus, instead providing aggregate statistics, sanitized examples, solver-side analysis code, and bounded defensive tooling.This release strategy supports reproducibility while reducing misuse potential.
  • Mitigation-first framing: The tool-based mitigation redirects CSP-style inputs to bounded solvers rather than unrestricted natural-language reasoning and substantially reduces token usage.The defense is presented as a practical system-level response to search amplification.
  • Potential misuse: SMTrap is dual-use because adversaries could construct benign-looking queries that consume excessive reasoning resources.The authors emphasize mechanism analysis, aggregate measurements, mitigation strategies, monitoring, cost-aware routing, and bounded reasoning policies.
  • Limitations: The study covers CSP-style tasks from Sudoku, Zebra-Game, and another CSP family, while Z3 conflict count remains a practical solver-side proxy rather than a complete difficulty measure.These tasks cover a broad class of structured search problems but do not exhaust all possible LRM resource-amplification attacks.

F Detailed Behavior Analysis of Search Amplification

The analysis of DeepSeek-v4-pro’s reasoning traces finds a stable trial-and-backtracking search pattern across conflict levels. Higher SMT conflict counts are associated with more explicit search behaviors and longer outputs, without materially changing the reasoning composition.

  • Behavior attribution: Reasoning traces are split into non-empty line-based chunks and exclusively classified into proposing assignments, checking constraints, encountering contradictions, revising failed branches, or Other.Chunks of no more than eight characters are discarded; overlapping categories follow the priority order contradictions, branch revisions, assignments, then constraint checks.
  • Stable search-oriented reasoning composition: Across zebra puzzles and Sudoku, constraint checking has the largest character-length share, followed by assignment proposals, while contradictions and branch revisions remain smaller but persistent.The relative composition remains broadly stable across conflict levels; unmatched content is omitted from the displayed shares.
  • Interpretation: The findings indicate that higher SMT conflict counts increase the amount of trial-and-backtracking search within a stable reasoning style rather than merely inducing generic verbosity.The analysis links longer outputs to identifiable search behaviors whose frequency tends to increase at higher conflict levels.
  • Higher conflict is associated with more explicit search behavior: Higher-conflict instances generally produce more constraint checks, assignment proposals, contradiction encounters, and branch revisions, especially for Sudoku, although zebra puzzles show larger non-monotonic fluctuations.Behavior counts trend upward with conflict level, unlike the broadly stable relative shares.

G Comparison with Static Manual Stress Benchmarks

SMTrap differs from static manual puzzle benchmarks by automatically and cheaply synthesizing inference-heavy CSP payloads through CPU-side symbolic optimization. Static benchmarks can stress LRMs, but their finite, exposed instances are vulnerable to memorization, caching, filtering, blocking, or specialized routing.

  • Comparison with Static Manual Stress Benchmarks: SMTrap automatically synthesizes inference-heavy CSP payloads through CPU-side symbolic optimization rather than manual puzzle design.This supports the claim that DoS risk includes cheaply optimized reasoning payloads derived from the task search space itself.
  • Limitations of static public benchmarks as long-term DoS payloads: Static manual benchmarks provide effective stress tests, but their finite and enumerable instances can be memorized, cached, fingerprinted, blocked, or routed to specialized solvers.Public exposure also creates risks through training or tuning contamination and input-filter identification.
  • Optimizability as a requirement for practical LRM-DoS: Practical LRM-DoS payloads should be searchable, tunable, and improvable under a measurable cost objective, properties static hand-designed benchmarks do not naturally provide.Manual benchmark instances are fixed after release, whereas SMTrap optimizes payloads from task structure.
  • Why SMTrap is different: SMTrap shows that benign-looking CSP tasks can be optimized into inference-heavy payloads using only CPU-side symbolic search, exposing a broader vulnerability class than fixed human-designed puzzles.The distinction is central to assessing practical DoS risk, even though SMTrap is not intended to dominate every manual puzzle on every model.

H DoS Payload Examples from SMTrap … I.5 Z3 and the Conflict Count Used in This Work

SMTrap transforms solution-preserving CSP clue states into high-conflict attack payloads and uses Z3 conflict counts as a controlled, model-feedback-free signal for search amplification. The signal reflects conflict-driven backtracking behavior, but its interpretation depends on fixed encodings and solver configurations rather than a universal difficulty scale.

  • H DoS Payload Examples from SMTrap: SMTrap replaces solution-consistent clues while preserving task size, clue count, and the unique solution to increase solver conflicts.In Sudoku, eight clue replacements raise conflicts from 41 to 3,510 (85.61×); in a zebra puzzle, seven replacements raise them from 290 to 5,720 (19.72×).
  • H DoS Payload Examples from SMTrap: SMTrap embeds optimized CSP instances in natural prompts requesting manual step-by-step reasoning while suppressing tool-based shortcuts.The resulting payloads are designed to make ordinary initial instances substantially more search-intensive.
  • I.1 From SAT to SMT: SMT extends SAT by combining Boolean search with theory-specific reasoning over arithmetic, equalities, arrays, bit-vectors, and related structures.Modern SMT solving commonly coordinates a SAT engine with specialized theory solvers through the DPLL(T) framework.
  • I.2 Encoding CSPs as SMT Formulas: CSPs are encoded as SMT formulas whose satisfiability corresponds to puzzle solvability, while an additional disequality check can verify unique solutions.Changing visible clues alters the encoded instance without changing fixed task structure, enabling conflict-count comparisons across clue states.
  • I.3 Conflict-Driven Search in SMT Solvers: Conflict-driven SMT search propagates partial assignments, checks Boolean and theory consistency, learns from contradictions, and backjumps to revise failed branches.This structured trial-and-backtracking process can include theory propagation that reduces explicit branching.
  • I.4 Relation to LRM CSP Solving: SMT solvers and LRMs use different mechanisms but exhibit analogous CSP behavior: proposing assignments, checking constraints, detecting contradictions, and revising failed branches.SMTrap therefore treats SMT conflict count as a cheap external estimate of induced LRM search, with the relationship tested empirically rather than assumed exact.
  • I.5 Z3 and the Conflict Count Used in This Work: Z3 is a general-purpose CDCL(T)-style SMT solver, and its reported conflict count summarizes conflicts encountered while resolving failed Boolean or theory assignments.Each conflict triggers analysis, learning, backtracking, and continuation along another branch.
  • I.5 Z3 and the Conflict Count Used in This Work: The conflict count is not solver-independent or universal, so SMTrap evaluates all instances under a fixed SMT encoding and solver configuration.Under this controlled setting, it serves as a low-cost, model-feedback-free guidance signal for testing longer LRM search trajectories.
Loading 2608.18921v1…