Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Evaluating Robustness of Reasoning Models on Parameterized Logical Problems

Naïm Es-sebbani, Esteban Marquer, Yakoub Salhi, Zied Bouraoui

TL;DR

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, is introduced.

Abstract

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.

Evaluating Robustness of Reasoning Models on Parameterized Logical Problems

TL;DR

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, is introduced.

Abstract

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.
Paper Structure (41 sections, 2 theorems, 8 equations, 10 figures, 6 tables, 2 algorithms)

This paper contains 41 sections, 2 theorems, 8 equations, 10 figures, 6 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related work
  3. Problem setting
  4. UNSAT Generator using Implication Cycles
  5. SAT Generator via Free Variables
  6. Backbone-based Method
  7. Monotone Split with Moving Cross-Polarity Bridge
  8. Symmetry/Redundancy Probe
  9. Dataset construction
  10. Experiments
  11. Impact of each difficulty parameters
  12. Impact of non-core variables
  13. Sensitivity to clause order
  14. Ability to handle repeated patterns
  15. Verbalization strategy
  16. ...and 26 more sections

Key Result

Theorem 1.3

A $2$--CNF formula is unsatisfiable iff it admits a proof cycle.

Figures (10)

  • Figure 1: Main three difficulty parameters for Backbone at $|\mathcal{C}|=75$. Shade corresponds to 95% confidence interval. For $\pi$, $\pi=0$ for a negative and $\pi=1$ for a positive monotonous part, while at $\pi=0.5$ the sign is randomly chosen.
  • Figure 2: Main three difficulty parameters for MonoBridge at $|\mathcal{C}|=75$. Shade corresponds to 95% confidence interval.
  • Figure 3: Main difficulty parameter for EquivalenceCore at $|\mathcal{C}|=20$. Shade corresponds to 95% confidence interval.
  • Figure 4: Main difficulty parameter for implication cycle at $|\mathcal{C}|=75$. Shade corresponds to 95% confidence interval.
  • Figure 5: Comparison of decision accuracy on satisfiability (UNSAT problems) and SAT witness validity (SAT problems), between the construction order and a shuffling of the clauses. All difficulty parameters are set at $0.5$. Error bars are 95% confidence intervals across models and verbalization templates.
  • ...and 5 more figures

Theorems & Definitions (6)

  • Definition 1.1: Implication Graph
  • Definition 1.2: Proof Cycle
  • Theorem 1.3
  • Example 1: UNSAT core with $m{=}5$, $k{=}3$
  • Example 2
  • Proposition 5.1: Satisfiable by construction