Technical Summary: Bridging Legal Interpretation and Formal Logic

Problem Statement: The Divergence of Correctness

The paper identifies a fundamental misalignment between the goals of legal professionals and AI researchers in the context of Large Language Model (LLM) adoption. While legal interpretation relies on background knowledge and contextual inference to derive conclusions, formal logic demands that all inferences be explicitly grounded in the source text.

The core problem is not merely that LLMs hallucinate facts, but that they systematically draw inferences beyond what the source text supports, presenting assumption-laden conclusions as logically grounded. Current legal AI systems typically either mimic legal interpretation (via language model training) or enforce formal validity (via symbolic methods), failing to acknowledge that these two modes of reasoning regularly diverge. This gap renders AI-assisted legal reasoning untrustworthy in high-stakes environments where rigor is paramount.

Methodology and Experimental Design

1. Re-annotation of ContractNLI

The authors investigate this gap using the ContractNLI dataset, originally annotated by legally trained experts. They re-annotate these examples under a strict formal definition of entailment:

• Entailment: A hypothesis $H$ is entailed by premise $P$ if and only if $P \land \neg H$ is unsatisfiable.
• Contradiction: $H$ is contradicted if $P \land H$ is unsatisfiable.
• Neutral: Otherwise.

This process transforms the "opaque gap" between pragmatic interpretation and strict logic into a measurable object. The authors construct minimal pairs for divergent cases—modifying hypotheses minimally to supply missing assumptions explicitly, thereby making them formally entailed.

2. Evaluation of Three Paradigms

The study evaluates three reasoning paradigms across five LLMs (GPT, Claude, LLaMA, DeepSeek, Qwen):

1. Pure LLM Classification: Standard prompting without formal constraints.
2. LLM Reasoning over Formal Representations: LLMs generating logical structures.
3. Neuro-Symbolic Pipeline: A system combining LLM formalization with an SMT solver (Z3) for verification.

3. The "Solver-in-the-Loop" Approach

When the SMT pipeline encounters a lack of explicit grounding, it does not simply fail; it computes the minimal set of additional axioms required to shift the classification from Neutral to Entailment or Contradiction. These minimal assumptions are presented to a legal reviewer as targeted questions (e.g., "Does standard contract law implicitly establish this assumption?"), allowing human expertise to validate or reject the implicit norms.

Key Findings

Label Shifts and Systematic Gaps

Re-annotation revealed a substantial proportion of label shifts, primarily from ENTAILMENT to NEUTRAL. This indicates that many conclusions deemed valid by legal experts rely on background knowledge or contextual assumptions absent from the text.

Failure Modes

The study identifies three recurring failure modes in current models:

1. Assumption Injection: Silently bridging gaps with unstated inferences.
2. Scope Laundering: Presenting informal conclusions as formally grounded.
3. Implicit Constraint Blindness: Overlooking constraints present in formal representations.

Performance Analysis

• Accuracy vs. Faithfulness: High-performing models succeed by mimicking legal interpretation (including implicit assumptions) rather than reasoning formally. Accuracy does not imply faithful reasoning.
• The SMT Advantage: The neuro-symbolic pipeline is more conservative, returning "Neutral" when explicit grounding is lacking. It surfaces the gap rather than "papering over it."
• Dominant Error: The most common error across all models is NEUTRAL $\to$ ENTAILMENT misclassification, reflecting systematic assumption injection. Confusions between Entailment and Contradiction are rare, suggesting the issue is insufficient grounding, not logical inconsistency.

Proposed Contributions and Research Agenda

1. A New Benchmark Dataset

The authors propose a benchmark for stance misrepresentation in legal and academic text. Unlike existing benchmarks that focus on fabricated citations, this dataset targets cases where sources exist and are retrieved correctly, but the model's claim overstates, understates, or mischaracterizes the source. It utilizes the three-way framework and minimal pair methodology established in their research.

2. Solver-in-the-Loop Training

Instead of relying on LLM judges or human preferences for feedback, the authors propose using a formal verification tool as a reward signal.

• The system teaches models to distinguish between formally supportable inferences and assumption-laden ones.
• When a claim is flagged as insufficiently grounded, the solver computes the minimal axioms needed to ground it.
• This feeds directly into targeted human review at the precise points where legal interpretation and formal grounding diverge.

Significance and Vision

The paper argues that understanding where and why current legal AI systems fail is not a limitation but the foundation for a trustworthy future. The proposed vision is an AI legal reasoning system that operates transparently across both frameworks:

• Capable of legal interpretation when appropriate.
• Capable of formal grounding when required.
• Able to surface the minimal assumptions connecting the two for targeted legal review.

By honestly characterizing failure modes, the authors aim to build systems that proactively surface interpretive uncertainty, reducing the burden of manual verification without sacrificing the accountability demanded by legal practice. This approach shifts the paradigm from asking lawyers to verify conclusions after the fact to integrating human expertise precisely where formal methods reach their limits.