Evaluating Robustness of Reasoning Models on Parameterized Logical Problems

SAI replication review · Referee report

Summary

The paper introduces a diagnostic 2-SAT benchmark built from five parameterized 2-CNF families (contradiction-cycle UNSAT cores, free-variable equivalences, planted backbones, monotone-split with a moving cross-polarity bridge, and a symmetry/duplication probe) plus a suite of semantics-preserving perturbations (clause reordering, filler clauses, and cross-copy renaming). The conceptual move is to exploit the tractability of 2-SAT — where satisfiability is fully characterized by the implication graph and SCC structure — as a feature rather than a limitation: because the verification objective is fixed and the label is solver-certified, structural properties (cycle length, imbalance, backbone fraction, bridge position, monotone density) can be varied one at a time without confounding logical difficulty with search hardness or surface presentation. The evaluation goes beyond decision accuracy by also scoring witness validity (a satisfying assignment) and by measuring how much decisions and assignments move under semantics-preserving transformations. Across seven open-weight reasoning models (14-120 B), three proprietary reasoning models, and several ablations (reasoning-effort levels, tool-calling with pysat, template vs. LLM verbalization), the paper reports sharp performance transitions and generator-specific brittleness even when instance size is held fixed, and a large SAT-prediction bias in one model (Llama-3.3-70B). This is a well-motivated, thoughtful benchmark that fills a genuine gap between prose-heavy logical benchmarks and aggregate SAT accuracy. The main conceptual limitation is that "presentation-invariant structural reasoning" is inferred from sensitivity in either direction — including cases (EquivalenceCore) where shuffling helps, which is at least as consistent with construction order leaking a solving shortcut as with brittleness. Statistical power per cell is modest (10 formulas), some notation and construction details are off, and code coverage does not extend to the significance testing, the tool-calling ablation, or the reasoning-effort sweep. Execution on the shipped code additionally revealed a silent-failure mode (the default litellm model prefix produces bad_format on every item while the run reports success), which is a substantial obstacle to independent reproduction rather than a defect of the paper's methodology.

Strengths

Conceptual contribution. Using 2-SAT's implication-graph characterization as a structural controllability lever — rather than treating tractability as a limitation — cleanly separates logical structure from search hardness, and the five generator families each target a distinct competency (long-range implication tracking, propagation from a small free set, planted backbones, late coupling / clause revision, symmetry/duplication).
Decision vs. witness metric. Reporting witness validity alongside SAT/UNSAT decision accuracy exposes a real gap — some models can classify SAT correctly but cannot construct a valid assignment — that aggregate SAT accuracy would hide. Under partial re-execution, this gap reproduces in the expected direction (pooled decision accuracy 94.4% vs. witness validity 61.1%; EquivalenceCore at $|C|=50$ collapses to 100% decision accuracy and 0% witness validity). The SAT-prediction-on-UNSAT diagnostic (Table 5) also usefully identifies Llama-3.3-70B's SAT-bias mode.
Breadth of controlled perturbations. Clause reordering, filler clauses, cross-copy renaming, and repetition are all implemented as explicit semantics-preserving transforms with paired variants in the released configs, which is unusually complete for a benchmark of this kind.
Model coverage across scales and providers. Seven open-weight reasoners at 14-120 B, three proprietary reasoners, a GPT-OSS reasoning-effort sweep, and a tool-calling ablation collectively give a broader picture than most single-benchmark evaluations.
Verbalization comparison. The six template verbalizers plus the LLM narrative verbalizer, with a two-step validator and fallback, isolate wording sensitivity from structural sensitivity. Table 7's prompt-length figures reproduce essentially exactly under re-execution (48/48 cells within one token), and the template-invariance finding in Figure 8 is a genuinely useful null result.
Solver-certified labels. Independent re-solving with pysat of the 1,320 generated formulas found 0 mismatches with the shipped labels — a small but real confidence signal about the data-generation half of the pipeline.

Weaknesses

"Presentation-invariant reasoning" claim is asymmetric. The headline conclusion is that models fail presentation invariance because they are sensitive to reorderings, but for EquivalenceCore shuffling improves performance. That is at least as consistent with construction order leaking solution structure (contiguous equivalence chains) as with brittleness, and the two directions should not be aggregated into a single verdict without a mechanistic story.
Confusion-matrix denominators are not comparable across models. Row totals in Table 9 vary from 918 to 1,318, roughly consistent with the Table 4 truncation rates, i.e., truncated items are excluded from Table 9 while Table 1 counts them as incorrect. Under this inconsistency, statements like Qwen3-Next-80B has "the most balanced error profile" and 96.3% accuracy are not directly comparable to Llama-3.3's 70.9%.
Phi-4-reasoning-plus results are entangled with truncation. A 30.5% truncation rate under a 16,384-token cap (vs. 0-3.6% for the 32,768-token models) means a large slice of Phi-4-plus's Table 1 accuracy is a budget effect, not a reasoning effect. This is disclosed but not surfaced at the reader-facing tables and confounds several ImplicationCycle collapses.
Statistical power per cell is small. Ten independent formulas per (generator, $|C|$ , parameter) cell, with six correlated verbalizations, caps the power for the many "not significant" verdicts (bridge position, some $k/L$ sweeps), and makes several borderline p-values in Table 6 hard to distinguish from noise.
Contradictory statistical framing. The EquivalenceCore free-to-bound-ratio effect is called "strong and consistent" and "significant both overall and in the 7-point sweep," yet the parenthetical overall p-value is 0.31. Similarly, the backbone-fraction $\beta$ effect is simultaneously "the most significant" and "marginal" — clean separation of effect size from significance would help.
LLM-verbalizer degradation attribution is confounded with prompt length. The reported 25-point drop is attributed "mainly" to contextual noise and weaker cues, but Table 8 shows LLM prompts are 4-10 $\times$ longer at matched $|C|$ . A length-matched control (template prompts padded with logically inert filler) is needed to separate the two drivers.
Tool-calling comparison confounds solver access with reasoning mode. In the "with tools" condition, reasoning is disabled due to an API constraint, so the $+17$ / $+60$ pp gains reflect the joint effect of adding pysat and removing the reasoning trace. This weakens the paper's specific claim that ImplicationCycle's residual failure is NL $\to$ CNF parsing rather than reasoning.
Interpretive attribution for the bridge-position null is unverified. The suggested mechanism ("models restate the problem as an unordered set of constraints") is presented as an explanation but not backed by trace-level analysis; this matters because it is the only interpretive move against a key design axis of the MonoBridge generator.
Implication-graph edge definition and small technical slips. Definition A.1 as written does not encode the standard 2-SAT edge rule ( $\neg\ell_1 \to \ell_2$ and $\neg\ell_2 \to \ell_1$ ) — the central formal object the generators depend on. The " $\ell_1 \to \ell_1$ " claim in the UNSAT cycle description drops the negation; the bridge insertion range is written as $s \in \{1, \ldots, M+1\}$ in Section E but $s \in [1, |C|-1]$ in Section 3.4; the ImplicationCycle split parameter is written as $k/m$ in Section 5.1 but defined as $k/L$ in Section 3.1; the same generator is called both "SAT Generator via Free Variables" and "EquivalenceCore"; and Example 1 lists only three clauses where the generic construction predicts six.
Sample-value story does not match the intervals. The parameter grid 0.2 / 0.5 / 0.8 is described as "close to the center" of the thirds $[0, 1/3]$ , $[1/3, 2/3]$ , $[2/3, 1]$ , but the actual centers are $1/6$ , $1/2$ , $5/6$ . Either the sampling scheme or the framing should change.
Section-ordering compilation artifact. Section 5.4's heading appears before Section 5.2's content, and the discussion under 5.4 refers back to 5.2 before it has been introduced.

Reproducibility & code

Executing the released harness end-to-end was possible only on a small corner of the paper's grid: on a shared A100 with ~46 GB held by another tenant, only one of seven open-weight models (microsoft/Phi-4-reasoning) could be served, and even that model completed only 24 of the planned $\sim$ 9,240 evaluations. Consequently 19 of 27 identified claims were not_attempted (see the environment-limitation groupings below). Within that scope:

What replicated cleanly. Table 7's prompt-length figures reproduce essentially exactly (48/48 cells within one token, letter longest at every $|C|$ , logic/room alternating as shortest). The dataset generator matches the paper: pysat re-solving of all 1,320 generated formulas found 0 label mismatches. The witness-validity gap reproduces directionally (pooled decision accuracy 94.4% vs. witness validity 61.1%; EquivalenceCore $|C|=50$ collapses to 100/0). The one Phi-4-reasoning confusion-matrix row lands at 83.3% accuracy (paper: 86.3%), and ImplicationCycle at $|C| \in \{5, 10, 50\}$ falls monotonically $100 \to 50 \to 0$ %, close to the paper's $83.3 \to 83.3 \to 3.3$ %. At $n=2$ per cell, none of these matches is quantitatively tight, but the qualitative pattern survives.
Headline aggregates could not be verified end-to-end. Table 1 (259 numeric cells) had only 21 cells produced, all in the Phi-4-reasoning column at $n=2$ per cell. Cross-model claims — the widening gap between Phi-4 variants and Qwen3-Next-80B, the "most balanced error profile" of Qwen3-Next-80B in Table 9, Llama-3.3-70B's 88.3% SAT-on-UNSAT rate, and the "consistently harder" ranking of ImplicationCycle — are entirely untestable in this run because six of the seven table models never ran. This is an environmental limitation of the reproduction, not a fault of the paper, but it does mean the strong quantitative claims of the paper rest on runs that no external group has independently verified in the released code.
Harness has a silent-failure defect that inflates reproduction risk. The README's litellm model string (hf/<model>) is rejected by current litellm, and batch_completion returns the provider error text as the completion string instead of raising. Every item scores bad_format and the run tree looks complete — an initial reproduction attempt produced 1,018 of 1,020 items as bad_format while reporting success. Combined with eval.py checkpointing only after a full litellm batch returns (so batch_size is the effective durability knob and 11 min of A100 generation ended with zero files on disk), it is easy for a reproducer to publish an entirely spurious accuracy table under the paper's own protocol. Neither defect is critical to the paper's numbers as reported, but both are load-bearing for whether an external group can verify them.
Statistical-testing pipeline is not shipped. There is no implementation of Friedman's test or Benjamini-Hochberg correction, and no aggregation script that produces Table 6's p-values or the significance annotations on Figures 5-7 or the paired t-tests in Sections 5.2-5.4. About 1,380 lines of aggregation and statistics code had to be written from scratch, and the exact family definitions used for BH correction had to be guessed.
7-point sweep configurations are not laid out. The released configs cover a coarse 3-point sweep; the 7-point grid $\{0, 0.2, 1/3, 0.5, 2/3, 0.8, 1\}$ used for Figures 1-4 and the "7-point" rows of Table 6 is not encoded as explicit generator-parameter tuples, and the mapping from the normalized $[0, 1]$ parameter to the underlying integer parameters is not documented.
Tool-calling and reasoning-effort ablations are not exposed by the harness. The tool-use scaffold, execute_python handler, 110-item logic-verbalizer subset, and pysat tool schema needed for Table 12 do not exist in the released code. The ChatHelper does not forward a reasoning_effort field to the vLLM chat endpoint, so Table 11 requires patching the harness.
Story-LLM identity for the LLM verbalizer is not pinned. The narrative pipeline is implemented (themes, three-step validation, fallback), but neither the paper nor the configs name the exact model / provider / version used to generate the augmented paragraphs. This affects the 95.4% / 3.3% validation statistics and the 4-10 $\times$ prompt-length ratios in Table 8, and can drift silently across model releases.
No aggregation / plotting scripts and no raw model outputs. The harness produces per-item JSON, but nothing in the repo assembles Tables 1, 5, 9, 10, 11, 12 or the accuracy-vs-parameter figures, and there is no released dump of per-item completions. A reproducer must re-run every model (open-weight + proprietary) to obtain the numbers behind the paper's headline aggregates.
Redundant-condition traces are missing from the release. The paper's "models rarely detect or exploit repeated patterns" claim rests on inspection of traces from the Backbone $(50 \times 2)$ redundant condition. Under execution, all 120 redundant-config result files stored the litellm connection-error string as the completion (a downstream consequence of the harness defect above), so the corpus needed to support the claim is empty rather than merely small in the shipped code path.

Recommended Changes

Essential

Reconcile Tables 1 and 9 denominators. State whether truncated/unparsable items are counted or excluded per table, and if the two differ, add a version of Table 9 that follows the Table 1 protocol so cross-model accuracy numbers are directly comparable. This addresses the confusion-matrix mismatch and the Llama-vs-Qwen "balanced error profile" claim.
Surface Phi-4-reasoning-plus's truncation caveat in Table 1. Either add a per-cell truncation-rate footnote next to the Phi-4-plus column or add a companion table that excludes truncated items, so that ImplicationCycle collapses at $|C| \ge 50$ are not silently attributable to a smaller output budget.
Fix Definition A.1 and the identity-implication typo. Restate the implication-graph edge set as the standard 2-SAT rule ( $\neg\ell_1 \to \ell_2$ and $\neg\ell_2 \to \ell_1$ ), correct the unit-clause disjunct ( $l' = \neg l$ ), and put the negation back on the target literal in the UNSAT cycle sentence.
Reconcile the remaining notation and construction mismatches. Unify the bridge-position range between Section 3.4 and Appendix E; use $k/L$ (or $k/m$ ) consistently between Section 3.1 and Section 5.1; fix Example 1 so its clauses match the general construction; and choose one name — "EquivalenceCore" or "SAT Generator via Free Variables" — throughout.
Rework the "presentation-invariant reasoning" framing to account for EquivalenceCore shuffling helping. When shuffling helps, that is evidence that construction order leaks a solving shortcut, not necessarily brittleness; either separate the two mechanisms explicitly or restrict the invariance claim to the generators where shuffling degrades performance.
Report a length-matched control for the LLM-verbalizer drop. Add a template-verbalizer condition padded with inert filler to match LLM prompt-token counts (or an LLM condition compressed to template length), so the 25-point drop can be split into a length effect and a wording effect.
Rerun the tool-calling ablation with reasoning enabled or with a matched no-reasoning baseline. The current Table 12 confounds "solver access" with "reasoning off"; either fix would make the "NL $\to$ CNF parsing is the residual bottleneck for ImplicationCycle" claim defensible.
Ship the statistical-testing pipeline. Release the Friedman + BH-correction code and the exact family definitions, plus the aggregation that turns per-item JSON into Table 6's p-values and the significance stars on Figures 5-7. This is the single largest reproducibility obstacle in the current release.
Ship the 7-point sweep configurations and the $[0, 1] \to$ generator-parameter mapping. Encode the 7-point grid as explicit generator-parameter tuples so Figures 1-4 and the "7-point" rows of Table 6 are reproducible without guessing.
Fix the harness silent-failure defect. Correct the default litellm model prefix (hf/ $\to$ openai/), raise on provider errors instead of writing them into results as bad_format, and decouple eval.py checkpointing from batch size so that reducing batch_size is not the only way to avoid losing an entire batch on interruption.
Ship aggregation/plotting scripts and a raw per-item model-output dump. This would let readers verify the aggregates in Tables 1, 5, 9, 10, 11, 12 without re-running every model, and would remove a major class of divergence between paper and re-runs. It would also let a reader independently check the "models rarely detect repetition" claim by inspecting the redundant-condition traces.
Pin the story-LLM. Name the exact model / provider / version used for the LLM verbalizer, or (ideally) ship the augmented paragraphs as a static dataset so Section 5.5 and Table 8 do not drift.

Suggested

Expose reasoning-effort and add tool-calling code. Add a one-line reasoning_effort pass-through in ChatHelper and a documented execute_python handler with the pysat tool schema and the 110-item logic-verbalizer subset, so Tables 11 and 12 are reproducible without harness patching.
Report effect sizes alongside p-values in Table 6 and Section 5.1. $\eta^2$ or partial $\eta^2$ would make "most significant but marginal" (backbone $\beta$ ) and "strong and consistent … but overall $p = 0.31$ " (EquivalenceCore ratio) cleaner to interpret. In the same paragraph, please clean up the duplicated "β β", "for for", and "and and" tokens.
Reword the "close to the center of each interval" description. State the actual grid values and drop the "center" framing (or move the grid to the actual thirds if that was the intent).
Back the bridge-position null with trace-level evidence. Report the fraction of MonoBridge traces in which the model reorders clauses in the first few CoT steps; otherwise mark the "unordered set of constraints" explanation as a hypothesis rather than an explanation.
Support the "density 0.6-0.8 recovery" claim with specific numbers. Either annotate the corresponding sweep values or point to the subplot in Figure 2 that contains them.
Clarify the micro-average definition in Table 10's caption. Say explicitly that ImplicationCycle is the UNSAT generator and therefore contributes decision accuracy rather than witness validity to the micro-average.
Fix the Section 5.4 / 5.2 header ordering so 5.2's content is not preceded by 5.4's title.
Report per-formula and per-template variance. Given $n = 10$ formulas per cell, add confidence intervals or a mixed-effects analysis with formula and template as crossed random effects, so the many "not significant" verdicts can be distinguished from underpowering. Also state exactly how the six verbalizations are collapsed into one per-formula measurement.