通过LLM代理和形式推理实现可信的法律AI
Towards Trustworthy Legal AI through LLM Agents and Formal Reasoning
AI总结：
L4L通过LLM代理与形式推理实现法律AI的可信性，通过四个阶段确保法律推理的逻辑性和可验证性。
摘要：
法律决定应当具有逻辑性并基于法定法律。尽管大语言模型（LLMs）在理解法律文本方面表现出色，但它们无法提供可验证的论证依据。我们提出了L4L，一个以求解器为中心的框架，该框架强制在基于LLM的法律推理和法定法律之间实现形式上的对齐。该框架整合了角色不同的LLM代理与基于SMT的验证，结合了自然语言的灵活性与符号推理的严谨性。我们的方法分为四个阶段：（1）法律知识构建，其中LLMs将法律条款自动形式化为逻辑约束，并通过案例级测试验证它们；（2）双事实与法律条文提取，其中检察官和辩护方对齐的代理独立地将案件叙述映射到论点元组；（3）以求解器为中心的裁决，其中SMT求解器检查论点的法律可接受性和一致性，以符合形式化的法律知识；（4）司法裁决，其中法官代理整合求解器验证的推理与法律解释和类似先例，以产生基于法律的裁决。在公共法律基准上的实验表明，L4L在性能上始终优于基线，同时提供可审计的论证，从而实现可信的法律AI。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
