PaperlayerView exact revision on arXiv

Source-linked AI summary

Beyond Surface Forms: Symbolic Edits as a Test for Logical Reasoning with LLMs

Ramya Keerthy Thatikonda, Wray Buntine, Ehsan Shareghi

arXiv:2608.30256v1cs.CLcs.AI

TL;DR

LLM reasoning can be sensitive to surface changes, but logical operators are difficult to manipulate systematically while preserving task labels. The paper introduces a solver-verified framework for symbolic operator edits and back-translation, finding inconsistent model behavior under controlled interventions. The results support structural stress tests and evaluation measures beyond standard accuracy.

  • Problem

    Existing logical-reasoning evaluations lack systematic, scalable ways to isolate structural changes while preserving or tracking deductive outcomes.

  • Method

    A tool-driven framework edits symbolic representations of first-order logic and constraint-satisfaction problems, verifies interventions with solvers, and translates them back into natural language.

  • Results

    LLM behavior under controlled operator edits is inconsistent, with models not reliably grounding reasoning in symbolic structure.

  • Takeaways & Limitations

    Structural-edit stress tests can assess reasoning reliability beyond traditional final-answer accuracy and motivate benchmarks explicitly probing symbolic reasoning.

  • Takeaways & Limitations

    The methodology depends on available symbolic and natural-language translations, and back-translation can introduce errors, especially for complex logical expressions.

Abstract

from arXiv · show

Logical reasoning with large language models (LLMs) is a critical capability, as it reflects a system's ability to correctly deduce hypotheses from a given context using faithful deductive processes. However, LLM reasoning has often been shown to be sensitive to small surface-level variations in problem formulation, raising questions about whether models truly follow the underlying logical structure. Studying this behavior is challenging because the symbolic components of logical problems, such as operators and predicates, are difficult to systematically manipulate in natural language. We introduce a tool-driven framework for generating controlled, label-preserving edits to logical reasoning problems. Our method operates on symbolic representations of first-order logic and constraint satisfaction problem tasks, enabling targeted modifications to logical operators and other structural components before translating them back into natural language. Using this framework, we evaluate various LLMs under cumulative and individual operator edits and analyze their behavior in response to these changes. Our quantitative and qualitative analyses show that LLM reasoning behavior under controlled operator edits is inconsistent, regardless of model size or family: models sometimes adapt correctly to structural changes but often fail to track their logical consequences. The results from this automated stress test enable an evaluation of language models across different dimensions and help measure the reliability of their reasoning.

1 Introduction

The paper introduces controlled symbolic edits to test whether LLMs track logical structure rather than surface patterns. Across models and reasoning strategies, behavior under operator interventions is inconsistent, motivating evaluation beyond final-answer accuracy.

  • Logical reasoning benchmarks are increasingly scrutinized because apparent gains may reflect distribution effects, contamination, or leakage rather than robust reasoning.
  • Small changes to logical operators, predicates, constants, or constraints can alter both the reasoning process and deduction outcome.
  • The proposed framework decomposes problems into symbolic components and applies targeted operator interventions while preserving the final deductive outcome.
  • The evaluation compares cumulative label-preserving edits with individual edits that can change the ground-truth answer across deductive reasoning and constraint-satisfaction tasks.
  • Across recent LLMs, reasoning changes rapidly and unpredictably under operator interventions, while label-changing edits expose possible reliance on original question-answer patterns.

2 Related Work

Prior work tests LLM sensitivity through surface, contextual, ordering, paraphrase, and counterfactual changes, but generally does not isolate logical operators automatically. This paper addresses that gap with symbolic, template-based interventions.

  • Perturbation studies reveal memorization and sensitivity but do not explicitly control structural factors across interventions.
  • Logical-deduction studies vary premise order and paraphrases, while mathematical studies use irrelevant context to probe performance degradation.
  • Mathematical intervention methods primarily edit numerical values, whereas this work targets operators in logical forms.
  • Counterfactual generation and metamorphic testing construct related inputs using counterfactual variants or predefined relations.
  • The paper focuses on natural-language reasoning and automated template generation grounded in symbolic structure rather than translation ability.

3 Methodology

The methodology edits symbolic logical representations, verifies valid interventions with solvers, and translates the edited forms back into natural language. It evaluates cumulative and individual changes under separately defined accuracy measures.

  • The framework intervenes on predicates, operators, variables, and values through symbolic representations, using a theorem prover as a wrapper.
  • Label-preserving edits are accepted only when the final deductive outcome remains unchanged, and each sentence is processed without revisiting earlier modifications.
  • Cumulative Edits: Cumulative-edit performance is indexed by k, with baseline predictions substituted when a record lacks a valid k-th edit.
  • Cumulative Edits: Normalized accuracy compares predictions after k edits with the baseline, rather than with the preceding edit.
  • Individual Edits: Individual interventions separately preserve or change outcomes, storing new ground-truth labels for label-altering cases and aggregating multiple variants by question.
  • Figure 2 summarizes operator editing, solver validation, back-translation, and downstream evaluation as the framework’s processing stages.
  • Back-translation: Edited symbolic forms are translated back sentence-by-sentence using the original statements as references to limit semantic drift.

4 Experiments

Experiments evaluate logical deduction and constraint-satisfaction benchmarks using controlled operator edits and multiple prompting strategies. The setup spans several model families and distinguishes label-preserving from label-changing interventions.

  • The evaluation uses FOLIO, Logical Deduction, and AR-LSAT, solved respectively with Prover9, a Python constraint solver, and Z3.
  • Operator edits: For first-order logic, operator mappings are applied selectively because some substitutions could make statements ill-formed or substantially alter their meaning.
  • Operator edits: FOL edits are applied sequentially, while CSP interventions use analogous swaps such as less-than with greater-than and equal with not-equal.
  • Operator edits: An operator edit is retained when the corresponding FOL or CSP solver returns a valid solution, and the number of validated edits is recorded per representation.
  • Back-translation: Back-translations use Gemini 2.5 Flash with task-specific instructions and five in-context examples, conditioning edits on both original text and altered symbolic forms.
  • Model evaluation: Cumulative-edit experiments compare CoT, test-time scaling, and symbolic CoT across Gemma3-1B–27B, LLaMA3-8B, Phi-4-Mini, and Qwen3-4B.

5 Results and Discussion

Controlled operator edits reveal that stable aggregate accuracy can conceal substantial instance-level and reasoning-level instability. Models differ in their sensitivity to edits, with label-changing mutations exposing answer retention and performance declines.

  • 5.1 Cumulative Edits: Accuracy often remains stable across cumulative label-preserving edits because correct-to-incorrect and incorrect-to-correct transitions balance out.Record-level predictions can continue changing even when aggregate performance shows minimal impact.
  • 5.1 Cumulative Edits: Flip rate measures the proportion of instances whose correctness changes between the original question and an edited version.It counts both incorrect-to-correct and correct-to-incorrect transitions, while unchanged predictions remain in the denominator.
  • 5.1 Cumulative Edits: Smaller Gemma models are highly unstable with chain-of-thought prompting, while inference-time scaling substantially stabilizes them on FOLIO and AR-LSAT.Qwen shows lower flip rates than Gemma on FOLIO and Deduction among 4B–12B models, whereas Gemma 4B is more stable on AR-LSAT.
  • 5.1 Cumulative Edits: Qualitative reasoning scores decline as the number of label-preserving edits increases, but the qualitative analysis covers only a small subset of records.The authors present this analysis as an initial application intended to motivate broader use in future LLM evaluation.
  • 5.1 Cumulative Edits: High final-answer accuracy can coexist with reasoning instability, as shown by Qwen3-4B on AR-LSAT.Under label-preserving edits, answer alignment decreases as variation increases even though accuracy does not decrease.
  • 5.2 Individual Edits: Label-changing operator edits reduce performance on FOLIO, while models also retain the original answer after altered labels.Except for Qwen, all models show some original-answer retention on FOLIO; retention decreases with model size on Logical Deduction.

6 Conclusion

The paper introduces controlled symbolic edits to stress-test whether LLMs follow logical structure, finding inconsistent reasoning under these edits. The framework may also support broader benchmark construction and evaluation beyond standard accuracy.

  • The framework generates controlled, label-preserving edits by operating on symbolic representations of logical reasoning problems.It enables precise operator-level interventions while preserving the original deductive outcome.
  • LLMs reason inconsistently when logical problems undergo controlled structural edits.The findings suggest that current models do not reliably ground reasoning in symbolic structure.
  • The findings highlight the need to benchmark structural reasoning and use evaluation metrics beyond standard accuracy.
  • Stability under structural variations could serve as a future training or evaluation signal to reduce reliance on pattern matching.
  • Symbolic editing may support more diverse benchmarks that expose models to broader reasoning patterns during training and evaluation.

Limitations

The study is constrained by translation coverage and fidelity, as well as the reproducibility limits of proprietary, nondeterministic models. These limitations affect which problems can be analyzed and how exactly results can be replicated.

  • Unavailable tool-supported translations prevent the analysis from being performed as-is for some problems.Parsable translation availability limits the number of translations, particularly for FOLIO.
  • Latent semantic errors may remain undetected when they do not affect the underlying reasoning chain.
  • Back-translation may introduce errors, especially for complex logical expressions, and earlier translation errors can propagate into it.The back-translation process uses a nondeterministic language model.
  • Proprietary models limit exact replication because they are nondeterministic and subject to undisclosed version updates.The authors report open-source models with explicit version identifiers to mitigate this limitation.

A Symbolic Translations

The study constructs symbolic translations and applies sentence-level back-translation to create edited natural-language problems. Translation coverage, fidelity checks, and prompt configurations determine which edited records enter the analysis.

  • Logical Deduction and AR-LSAT representations are generated with two-shot prompting adapted to structured JSON outputs.The format enforces constraints and guides the model toward well-formed symbolic representations.
  • Translation sampling is incrementally scaled to reduce inference cost while expanding the number of valid translations.Using Gemini 2.5 Flash, the procedure extracts translations for approximately 88% of records.
  • After symbolic edits, logical forms are back-translated using the corresponding natural-language text, including sentence fragments embedded within longer questions.This issue occurs, for example, in AR-LSAT.
  • Records lacking the required back-translate-and-replace procedure are removed, and later cumulative edits are discarded after the first unavailable translation.
  • Back-translation prompts the model to correct an original sentence while preserving the question’s semantic structure.The prompts are provided separately for AR-LSAT, Logical Deduction, and FOLIO.
  • Some Logical Deduction transformations are difficult to generalize because relational changes can admit multiple semantic interpretations.For example, changing “less than” to “greater than” may correspond to different interpretations such as older versus newer or left versus right.
  • Human evaluation sampled 90 examples and achieved 94.5% inter-annotator agreement, with one majority-rejected FOLIO example.The evaluation covered short and long sentences and logical forms.

E Complete Results

Across cumulative edits, final accuracy changes little because record-level prediction transitions balance out, although individual behavior can vary substantially. Label-changing edits produce larger accuracy declines and provide a test of whether models track changed answers.

  • Cumulative operator edits have minimal impact on performance across evaluated open-source models.The number of affected records at each edit level is reported separately while total evaluated records remain constant through fallback to base questions.
  • Gemini 2.5 Flash broadly matches Gemma-27B and is more stable than smaller open models, but AR-LSAT still produces prediction flips.Logical Deduction remains more stable, showing that consistency depends on dataset type.
  • Label-changing edits are fewer than label-preserving edits and coincide with a drastic accuracy drop, offering a way to test continued reasoning on altered answers.The analysis is intended for datasets approaching performance saturation.

F Variation in proof

The study examines whether changes in proof or reasoning length under logical edits correspond to changes in model predictions. Evidence is limited and does not show a consistent relationship across models.

  • F Variation in proof: Only 15 records showed changed proof length under cumulative edits, limiting conclusions about proof variation.Proof length is available only for examples with deterministic True/False labels.
  • F Variation in proof: Across Gemma models, only Gemma-4B showed a noticeable trend linking larger proof-length changes with prediction flips.The authors avoid strong conclusions because few proofs exhibited changed lengths.
  • F Variation in proof: For reasoning-length changes exceeding 250 tokens, no two models consistently flipped on the same examples.The analysis includes both increases and decreases in token count.
  • F Variation in proof: At least one model remained prediction-stable despite reasoning-length changes in both LogicalDeduction and AR-LSAT.This pattern indicates that altered reasoning length did not uniformly produce prediction changes.
  • F Variation in proof: Qualitative analysis codes reasoning using Premise Fidelity, Inference Validity, Answer Completion, and Answer Alignment.The evaluator receives the original question and generated reasoning path.
  • F Variation in proof: Qualitative findings are estimated judgments because the analysis depends on the verification capability of an evaluator LLM.Further study is needed to validate these observations.

H Qualitative Analysis- Findings

The qualitative analysis identifies recurring reasoning failures across models, including low fidelity, invalid inferences, incomplete derivations, and contradictions between reasoning and final answers. It also presents LogicEdit as the framework underlying controlled operator edits.

  • H Qualitative Analysis- Findings: Smaller models generally show low Premise Fidelity and Inference Validity, while Gemma3-1B also shows very low Answer Completion and Answer Alignment.High alignment with low completion can indicate reliance on incorrect assumptions; the opposite pattern suggests answer changes without complete reasoning.
  • H Qualitative Analysis- Findings: Negative justification tokens expose recurring failure patterns, including distorts, misinterprets, invents, invalid, skips, incomplete, and contradicts.Tokens are analyzed for criteria receiving a score of 0.
  • H Qualitative Analysis- Findings: The qualitative evaluation reports overall reasoning and correct final outputs across models, datasets, and label-preserving edit levels.Tables show results for level 0 and the maximum available edit level, relative to each dataset’s record count.
  • H Qualitative Analysis- Findings: Models sometimes invent premises or orders that contradict the problem, such as placing the falcon fourth despite a premise requiring it to be second from the left.The example illustrates failures of premise fidelity.
  • H Qualitative Analysis- Findings: Some reasoning skips necessary intermediate steps, reaches premature conclusions, and jumps unsupported to a correct final answer.This pattern concerns Answer Completion even when the final conclusion is correct.
  • H Qualitative Analysis- Findings: A model’s final answer can contradict both its derived sequence and its own evaluation of an option.In the example, the answer identifies the robin as rightmost although the derived sequence places the falcon rightmost.
  • H Qualitative Analysis- Findings: The qualitative analysis is presented as a starting point for studying LLM tendencies and developing more rigorous evaluation methods.The authors state that these behaviors require further detailed study.
  • H Qualitative Analysis- Findings: LogicEdit uses symbolic reasoning solvers to generate single-edit and cumulative-edit variations from formal logical representations.The accompanying pipeline supports translation, editing, and back-translation for logically verified benchmark variations.

J Models and Configurations

The study evaluates open-source models using specified inference configurations and prompt-based translation and qualitative-analysis procedures. Resource limits and output constraints affect parts of the experimental setup.

  • J Models and Configurations: Seven open-source models are obtained from Hugging Face repositories.The models are used for the reported evaluation experiments.
  • J Models and Configurations: Gemma models use API-based Chain-of-Thought and Symbolic CoT inference, while scaling experiments run on A100 GPUs.Other models also use A100 GPUs with 100GB memory and temperature 0.1 unless otherwise specified.
  • J Models and Configurations: Gemma 27B scaling uses at most 8 samples, whereas other models use 32 samples at temperature 0.7.The different sample counts reflect memory and resource constraints.
  • J Models and Configurations: CoT generations allow up to 10,000 tokens, while the other two prompting strategies allow 2,000 tokens.The smaller limit may distort performance, as observed for Qwen, by producing incomplete inferences.
  • J Models and Configurations: Gemini 2.5 Flash generates symbolic data, back-translations, and qualitative analyses; datasets and models are publicly available.The datasets contain no sensitive information according to the paper.
  • J Models and Configurations: Figure 5 depicts the pipeline integrating LogicEdit to generate alternative benchmark variants for robust-reasoning tests.The pipeline connects the editing framework with benchmark generation.
  • J Models and Configurations: Figures 6–8 show shortened prompts for translating logical representations into natural-language statements for AR-LSAT, Deduction, and FOLIO.These prompts support dataset-specific translation procedures.
  • J Models and Configurations: Figure 9 shows the shortened prompt for evaluating model-generated reasoning paths with four binary qualitative coding dimensions.The evaluation prompt operationalizes the qualitative analysis.
Loading 2608.30256v1…