Evaluating Robustness of Reasoning Models on Parameterized Logical Problems

Logic provides a controlled testbed for evaluating LLM-based reasoners, yet standard SAT-style benchmarks often conflate surface difficulty (length, wording, clause order) with the structural phenomena that actually determine satisfiability. We introduce a diagnostic benchmark for 2-SAT built from parameterized families of structured 2-CNF formulas, where satisfiability is characterized by the implication graph and can be tuned along interpretable axes. Our generators isolate distinct competencies and failure modes: (i) contradiction-cycle UNSAT cores with controllable size and imbalance, (ii) SAT instances with a prescribed fraction of free variables to control solution multiplicity, (iii) planted backbones that modulate propagation, (iv) late bridge clauses that couple otherwise monotone regions to probe sensitivity to ordering and revision, and (v) symmetry/duplication variants that test abstraction under renaming and redundant structure. We evaluate LLM-based reasoners on decision accuracy and assignment validity, and quantify robustness under semantics-preserving perturbations such as clause reordering, filler clauses, and variable renaming. Across models, we observe sharp performance transitions under targeted structural interventions even when surface statistics are held fixed, revealing brittleness regimes that are invisible to aggregate SAT accuracy.

Large language models are increasingly used for tasks that require reasoning, such as solving puzzles, writing code, or checking whether a set of constraints is consistent. However, it is often unclear whether these models are genuinely following the underlying logical structure of a problem, or whether they are relying on surface patterns such as wording, order of presentation, or familiar templates. This paper introduces a controlled benchmark for testing this distinction. We focus on a simple but structurally rich class of logical problems called 2-SAT, where each problem can be represented as a graph and checked exactly by a conventional solver. This lets us generate problems whose logical difficulty can be varied in precise ways, while also applying transformations that should not change the answer, such as reordering clauses, renaming variables, adding irrelevant clauses, or duplicating parts of the problem. We evaluate several reasoning-oriented language models on these problems. We measure not only whether a model correctly says that a problem is satisfiable or unsatisfiable, but also whether it can provide a valid assignment when it claims that a solution exists. Our results show that models can be brittle: their performance can change sharply under transformations that preserve the logical answer, and correct yes/no decisions can hide failures to construct valid solutions. Overall, the benchmark provides a diagnostic tool for studying when language models track logical structure robustly and when they are sensitive to presentation details. This can help build more reliable evaluations for reasoning systems, especially in settings where logical consistency and verifiable outputs matter.