Technical Summary: Are LLMs Stable Formal Logic Translators in Logical Reasoning Across Linguistically Diversified Texts?

1. Problem Definition

Logical reasoning systems utilizing Large Language Models (LLMs) often employ a neuro-symbolic paradigm where the LLM translates natural language (NL) into formal logic, which is then processed by a symbolic solver. While effective, this approach relies heavily on the translation step being faithful and consistent. A critical, yet under-explored, vulnerability is symbol drift: the failure of LLMs to map semantically equivalent expressions to the same logical symbol when those expressions appear in different linguistic forms (e.g., synonyms, paraphrases, or syntactic variations).

Existing benchmarks for logical reasoning typically use highly uniform language, often repeating identical surface forms for the same concepts. Consequently, they fail to evaluate whether LLMs can maintain symbol consistency across realistic linguistic variations. This gap leads to an overestimation of LLM robustness, as real-world text frequently expresses the same concept through diverse phrasing, which can break the reasoning chain and cause solver errors.

2. Methodology

2.1 SoLT: A Benchmark for Linguistic Diversity

To address the lack of evaluation for translation stability, the authors introduce SoLT (Stability of Logical Translation). SoLT is not a new dataset from scratch but a systematic transformation of existing reasoning datasets (LogicDeduction, ProntoQA, FOLIO, ProofWriter, ProverQA) using a Logic-invariant Linguistic Diversification method.

The diversification pipeline operates in three stages:

1. Repeated Concept Identification: The system identifies surface expressions appearing multiple times within a problem ($freq_q(e) \ge 2$).
2. Diversification Strategy Construction: For each repeated concept, the system generates variants at three levels:
   • Word-level: Synonym substitution (using WordNet).
   • Phrase-level: Paraphrasing (using PPDB).
   • Sentence-level: Syntactic rewrites (e.g., active-passive alternation, third-person reformulation) using LLMs.
3. Candidate Generation under Semantic Filtering: Generated candidates are filtered using strong sentence embedding models (e.g., BGE-large-en-v1.5) to ensure semantic similarity exceeds a threshold ($\theta = 0.90$). An LLM then assembles the final diversified problem, selecting candidates that maximize surface diversity while minimizing repeated forms for identical concepts.

Validation via embedding similarity scores and human/LLM logical invariance scoring (1–5 scale) confirms that SoLT preserves semantic meaning and logical structure while significantly increasing linguistic variation.

2.2 MenTaL: A Mental Representation-Guided Framework

To mitigate symbol drift, the authors propose MenTaL (Mental Representation Table-guided Translation). Inspired by cognitive theories of mental representation, MenTaL explicitly guides the LLM to construct and maintain a Mental Representation Table (MRT) during the translation process.

The MRT maps semantically equivalent expressions to a unified logical symbol ($\sigma$). The framework defines three update operations for the table:

• Extending: Assigning a new symbol to a previously unseen concept.
• Reusing: Mapping a new expression to an existing symbol if it is semantically equivalent ($e^{(i)} \equiv e^{(j)}$).
• Checking & Refining: Adjusting mappings for partial overlaps or subsumptions (e.g., mapping "popular show" to a refined atomic symbol).

MenTaL can be implemented via:

• In-Context Learning: Providing examples of MRT construction in the prompt for closed-source models.
• Supervised Fine-Tuning (SFT): Training smaller open-source models (e.g., LLaMA-3-8B) on reasoning traces generated by high-performance models using MenTaL.

3. Key Contributions

1. SoLT Benchmark: A general method and resulting benchmark that rewrites reasoning datasets into diverse, logically equivalent forms to systematically evaluate translation stability under linguistic variation.
2. MenTaL Framework: A lightweight, generalizable approach that enforces consistent symbol mapping by explicitly organizing concept-symbol relationships in a mental representation table.
3. Empirical Analysis: Extensive experiments demonstrating that current LLMs suffer from pervasive symbol drift under linguistic diversity and that MenTaL effectively mitigates this issue.

4. Experimental Results

4.1 Instability of Current LLMs

Experiments on SoLT using four LLMs (GPT-3.5, GPT-4, DeepSeek-V3, DeepSeek-R1) and three symbolic solvers reveal significant performance degradation:

• Accuracy Drop: Under direct prompting, accuracy drops substantially on diversified inputs (e.g., from 0.51 to 0.24 on average across tasks).
• Symbol Dispersion Score (SDS): A new metric quantifying symbol drift. SDS rises sharply on SoLT inputs (indicating inconsistent mapping) while remaining near zero on original datasets.
• Error Analysis: The primary failure mode is logic errors caused by inconsistent symbol assignment, rather than parsing or execution errors. Even mild linguistic variations (e.g., synonym substitution) cause clear accuracy degradation.
• Prompt Tuning Limitations: Simple prompt adjustments or few-shot examples encouraging consistency failed to significantly improve performance or reduce SDS on diversified tasks.

4.2 Effectiveness of MenTaL

Applying MenTaL yields consistent and stable performance gains:

• In-Context Learning: For high-performance models, MenTaL reduced SDS to near-zero on SoLT tasks and improved accuracy by up to 40.74% (e.g., on ProntoQA).
• Supervised Fine-Tuning: For the smaller LLaMA-3-8B model, standard SFT improved accuracy but failed to reduce symbol drift on diversified data. In contrast, MenTaL-based SFT achieved near-zero SDS and significantly higher accuracy on both original and diversified datasets, demonstrating strong generalization across solvers and tasks.
• Error Attribution: Manual analysis confirmed that approximately 50% of errors corrected by MenTaL were specifically due to improved symbol consistency, validating the mechanism's targeted efficacy.

4.3 Diversification Intensity

Experiments varying the "diversification intensity" (the number of sentences modified per problem) showed a smooth, continuous decline in LLM accuracy as intensity increased. This indicates a cumulative effect where processing more semantic variants progressively erodes the model's ability to maintain consistent symbol alignment.

5. Significance and Claims

The paper claims that overlooking linguistic diversity in current benchmarks obscures a critical weakness in LLM-based logical translators: the inability to maintain consistent symbol mapping across varied expressions. This "symbol drift" breaks logical coherence in real-world scenarios where synonyms and paraphrases are common.

The significance of this work lies in:

1. Diagnosis: Providing a systematic tool (SoLT) to identify and measure translation instability that standard benchmarks miss.
2. Solution: Offering a practical, generalizable method (MenTaL) to enhance the robustness of neuro-symbolic reasoning systems without requiring architectural changes to the solvers.
3. Reliability: Moving the field toward more reliable logical reasoning in real-world applications by ensuring that translation stability is maintained despite linguistic variation.

The authors conclude that while MenTaL significantly improves stability, the challenge of consistent symbol mapping remains a key area for future research, particularly as LLMs are deployed in complex, linguistically diverse environments.