Technical Summary: Towards Trustworthy Legal AI via Relevance-Sensitive Evaluation and Solver-Grounded Reasoning

1. Problem Statement

Legal reasoning fundamentally requires distinguishing between changes that are legally material and those that are irrelevant. In rule-of-law systems, judicial outcomes must satisfy formal rationality: conclusions should be justified by explicit, general, and logically coherent rules traceable to governing statutes. However, current Large Language Models (LLMs) applied to legal tasks (e.g., question answering, opinion summarization, bar-exam reasoning) exhibit critical failures in this distinction. They are often:

• Unstable under irrelevant perturbations: Their decisions change based on legally irrelevant attributes (e.g., demographics, stylistic reformulations, procedural background) or adversarial framing.
• Insensitive to material changes: They fail to update predictions when statutory elements, mental states, or applicable exceptions are altered.
• Vulnerable to confusion: They struggle to distinguish between similar statutes with overlapping surface facts but different applicability conditions.

Existing evaluations often study these phenomena in isolation (e.g., fairness or robustness separately). There is a lack of a unified framework that evaluates whether a model remains invariant under "should-not-change" perturbations while correctly updating under "should-change" perturbations.

2. Methodology

The paper proposes a two-pronged approach: a new evaluation framework and a novel reasoning architecture.

2.1 Legal-Relevance-Sensitive Evaluation

The authors formulate trustworthy legal reasoning as a legal-relevance-sensitive evaluation problem. This framework unifies judicial fairness, robustness, adversarial framing, and statute-confusion evaluation into a single suite.

• Perturbation Taxonomy: The evaluation categorizes perturbations into two types:
  1. Label-Preserving (Should-Not-Change): Perturbations that alter legally irrelevant information (e.g., demographic attributes, paraphrasing, irrelevant expert opinions, fabricated legal authorities) while preserving material facts. A trustworthy model must satisfy $f(x) = f(\tau(x))$.
  2. Label-Changing (Should-Change): Perturbations that modify legally material conditions (e.g., conduct, mental state, harm severity, statutory exceptions). A trustworthy model must satisfy $f(\tau(x)) = y_{\tau}$, where $y_{\tau}$ is the new legally correct label.
• Metrics: The framework measures Invariance (stability under irrelevant changes), Change Alignment (correct updates under material changes), Bias Magnitude, and Statute Correctness.

2.2 LexGuard: Solver-Grounded Adversarial Multi-Agent Framework

To address the failures of standard LLMs, the authors introduce LexGuard, a framework that separates legal proposal from legal checking using formal reasoning.

• Law Formalization: Statutes and judicial interpretations are auto-formalized into a formal legal knowledge base ($K$) consisting of executable constraints. Each rule is represented as a conditional constraint: $ARTICLEGUARD \land CLAUSEGUARD \Rightarrow PENALTY$. These guards check for subject, object, conduct, intent, harm, causation, and exceptions.
• Adversarial Agents: Two role-differentiated LLM agents (Prosecutor and Defense) independently extract structured fact-statute argument tuples from the same case narrative.
  • The Prosecutor focuses on facts supporting liability.
  • The Defense focuses on missing elements, exceptions, and alternative interpretations.
  • Agents debate confusing provisions within similarity clusters to refine candidate statutes.
• Solver-Centered Adjudication:
  1. The system searches $K$ for constraints corresponding to proposed statutes.
  2. Extracted facts are refined and matched against required legal elements.
  3. The refined facts and constraints are encoded into an SMT (Satisfiability Modulo Theories) formula ($\Phi$).
  4. An SMT solver (Z3) checks the satisfiability of article guards, clause guards, and exception guards.
  5. Conflict Resolution: If the solver finds a contradiction (e.g., conflicting facts or incompatible guards), it returns an "unsat core" identifying the conflict, triggering fact re-grounding or constraint repair.
  6. The final judgment is produced only by solver-verified legal applicability, filtering out irrelevant facts and hallucinated statutes.

3. Key Contributions

1. Evaluation Framework: The formulation of trustworthy legal reasoning as a legal-relevance-sensitive problem, instantiated with a unified suite of "should-change" and "should-not-change" perturbations covering fairness, robustness, adversarial attacks, and statute confusion.
2. LexGuard Architecture: A solver-grounded, adversarial multi-agent framework that formalizes statutes into executable constraints, uses adversarial agents to extract competing arguments, and employs an SMT solver to verify logical consistency and statutory satisfaction.
3. Empirical Validation: Comprehensive experiments demonstrating that existing legal LLMs are systematically sensitive to irrelevant variations and fail to distinguish related legal elements, whereas LexGuard significantly improves reliability, fairness, and robustness.

4. Experimental Results

The authors evaluated LexGuard on public legal datasets (LeCaRDv2, LEEC) and their custom perturbation suite.

• Standard Prediction Performance: LexGuard achieved the best F1 scores for both general and specific provision prediction on LeCaRDv2 and LEEC. The gains were primarily driven by higher precision, indicating the solver effectively suppresses irrelevant statute predictions.
• Sentencing Accuracy: LexGuard achieved the lowest Root Mean Square Error (RMSE) in sentencing predictions, both with and without "golden" (ground truth) statutes, while maintaining high legal validity (solver-verified).
• Relevance Sensitivity (RQ3 & RQ4):
  • Should-Change: LexGuard showed superior ability to update predictions when statutory elements were modified, outperforming baselines in "Change Alignment."
  • Should-Not-Change: LexGuard demonstrated strong robustness against adversarial framing (e.g., fabricated authorities, role hijacking) and benign reformulations, maintaining high invariance and attack-aware F1 scores where baselines failed.
• Statute Confusion (RQ5): In tasks involving confusing statute clusters (e.g., theft vs. fraud), LexGuard achieved significantly higher "Positive Exactness" (88.71% vs. 58.57% for baselines) and lower rates of omission and wrong similar-statute selection.
• Ablation Study: Removing the Z3 reasoner caused the largest degradation in performance, highlighting the necessity of symbolic consistency checking. Removing the adversarial debating module also significantly reduced accuracy, confirming the value of fine-grained competition among confusable provisions.

5. Significance and Claims

The paper claims that legal trustworthiness requires not only accuracy but also calibrated sensitivity to legally material changes.

• Beyond Accuracy: High accuracy alone is insufficient for legal AI if the model is unstable under irrelevant perturbations or insensitive to material changes. Trustworthiness is defined by the ability to distinguish relevant from irrelevant changes.
• Auditable Reasoning: By grounding decisions in formal constraints and SMT verification, LexGuard produces symbolic justifications that are auditable against explicit statutory rules, addressing the "black box" nature of standard LLMs.
• Robustness Mechanism: The results suggest that robustness to adversarial attacks and irrelevant perturbations cannot be achieved solely through prompt engineering (e.g., Chain-of-Thought or few-shot prompting) but requires a structural separation of proposal and verification via formal solvers.

Limitations Acknowledged:
The authors note that the framework's formalization quality depends on the accuracy of the LLMs used to generate initial facts and rules. The current system is limited to statutory rules and does not yet fully capture case law, open-textured norms, or evolving jurisprudence. Additionally, the multi-stage process introduces moderate computational overhead, though the cost per case remains practically affordable.