让AI判案像法官一样有法可依，还能自证清白。
Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning
- 用角色分工的AI代理+逻辑验证，把法律条文转成可计算规则
- 在公开数据集上准确率超越基线，且每步推理都可审计
- 适合需要可解释法律AI的司法科技、合规审查场景
法律判决应基于法定条文并具备逻辑一致性。尽管大语言模型（LLMs）擅长理解法律文本，却难以提供可验证的推理依据。我们提出L4L——一种以求解器为核心的框架，确保基于LLM的法律推理与法定条文之间实现形式化对齐。该框架融合角色分工的LLM代理与基于SMT的验证机制，结合自然语言灵活性与符号推理严谨性。流程分为四阶段：(1) 法律知识构建，由LLM自动将法律条文形式化为逻辑约束，并通过案例级测试验证；(2) 双向事实与法条提取，检方与辩护方代理独立将案件叙事映射为论证三元组；(3) 求解器驱动裁判，利用SMT求解器检验论证是否符合形式化法条及内部一致性；(4) 司法裁决生成，法官代理整合经求解器验证的推理、法条解释与先例，输出合法根基的判决。在多个公开法律基准上的实验表明，L4L持续优于基线模型，同时提供可审计的推理链，推动可信法律AI发展。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。