Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning

TL;DR

This paper introduces L4L, a framework combining large language models and formal reasoning to produce verifiable, trustworthy legal decisions with auditable justifications, improving legal AI reliability.

Contribution

L4L is the first framework to integrate role-specific LLM agents with SMT-based formal verification for legal reasoning, ensuring logical consistency and transparency.

Findings

L4L outperforms existing baselines on legal benchmarks.

Provides auditable and legally grounded verdicts.

Enables verifiable legal AI with formal reasoning.

Abstract

Legal decisions should be logical and based on statutory laws. While large language models(LLMs) are good at understanding legal text, they cannot provide verifiable justifications. We present L4L, a solver-centric framework that enforces formal alignment between LLM-based legal reasoning and statutory laws. The framework integrates role-differentiated LLM agents with SMT-backed verification, combining the flexibility of natural language with the rigor of symbolic reasoning. Our approach operates in four stages: (1) Statute Knowledge Building, where LLMs autoformalize legal provisions into logical constraints and validate them through case-level testing; (2) Dual Fact-and-Statute Extraction, in which the prosecutor-and defense-aligned agents independently map case narratives to argument tuples; (3) Solver-Centric Adjudication, where SMT solvers check the legal admissibility and consistency of the arguments against the formalized statute knowledge; (4) Judicial Rendering, in which a judge agent integrates solver-validated reasoning with statutory interpretation and similar precedents to produce a legally grounded verdict. Experiments on public legal benchmarks show that L4L consistently outperforms baselines, while providing auditable justifications that enable trustworthy legal AI.