用可验证的法律规则训练法律AI，让模型自我改进。
Closing the Loop: Formally Verified Law as a Reward Signal for Self-Improving Legal AI
- 将数学证明中的自动生成+验证范式移植到法律领域
- 在德国民事程序、美国宪法商事条款等案例中实现可验证推理
- 为法律AI提供闭环训练机制，适合司法智能与合规系统研发
本文提出一种架构，通过形式化可验证的奖励信号训练法律AI，将数学人工智能中的LLM生成+验证范式适配至法律特殊需求。该架构包含基于LLM的自动形式化（扩展Catala形式法律演算）、验证内核及基于形式证明轨迹的解释生成。对法律计算部分提供可证明正确性；对开放性法律分析提供结构保障：所有论证阶段均被覆盖，论证仅在适当阶段进行，且步骤间演绎关系有效。我们在德国程序期限计算、美国宪法商事条款分析以及跨司法管辖区制裁比例性问题上验证了该架构。进一步表明，同一架构具备结构优势：确定性外部验证器可提供可验证的法律问题结果，从而弥补法律领域强化学习中的传统闭环缺失。
原文摘要 · Abstract (English)
This article develops an architecture that creates a formally verifiable reward signal to train legal AI, adapting the LLM proposes, verifier disposes paradigm from mathematical AI to the distinctive demands of law. We present an architecture comprising LLM-driven autoformalization into a formal legal calculus extending Catala, a verification kernel, and explanation generation grounded in formal proof traces. For the computational components of law, the architecture provides provable correctness. For open-textured legal analysis, it provides structural guarantees: every required stage of the legal argument is addressed, argumentation is exercised at the correct stages and not omitted, and the deductive links between steps are valid. We demonstrate the architecture on procedural deadline calculations in German law, Commerce Clause analysis in U.S. constitutional law, and cross-jurisdictional sanction proportionality. We further show that the same architecture has a structural advantage for legal AI training: a deterministic external verifier supplies verifiable outcomes for legal problems and thereby closes the traditional reinforcement-learning loop gap in law.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。