Closing the Loop: Formally Verified Law as a Reward Signal for Self-Improving Legal AI
Summary
This paper presents an architecture that uses formally verified law as a reward signal for training legal AI, adaptively autoformalizing legal rules into a formal calculus and employing a verifier to ensure provable correctness, demonstrated on German and US law examples.
View Cached Full Text
Cached at: 06/24/26, 07:49 AM
# Closing the Loop: Formally Verified Law as a Reward Signal for Self-Improving Legal AI Source: [https://arxiv.org/abs/2606.23913](https://arxiv.org/abs/2606.23913) [View PDF](https://arxiv.org/pdf/2606.23913) > Abstract: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\. ## Submission history From: Torben Leowald \[[view email](https://arxiv.org/show-email/40f6527b/2606.23913)\] **\[v1\]**Mon, 22 Jun 2026 20:21:49 UTC \(309 KB\)
Similar Articles
Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems
This paper proposes techniques that combine formal methods (Linear Temporal Logic) with LLMs for auditing, monitoring, and intervening in AI systems to ensure compliance with behavioral constraints, showing that even small-model labelers can match frontier LLM judges in detecting violations.
Which Changes Matter? Towards Trustworthy Legal AI via Relevance-Sensitive Evaluation and Solver-Grounded Reasoning
This paper introduces a relevance-sensitive evaluation suite for legal AI, demonstrating that LLMs are overly sensitive to legally irrelevant perturbations, and proposes LexGuard, an adversarial multi-agent framework using formal reasoning to improve legal reasoning reliability.
Beyond Solver Verdicts: Generative Reward Models for Autoformalization
This paper proposes Generative Verification (GenV), a method using generative reward models to detect reference-equivalence failures in autoformalization, addressing vulnerabilities in neurosymbolic systems and improving verification accuracy.
Bridging Legal Interpretation and Formal Logic: Faithfulness, Assumption, and the Future of AI Legal Reasoning
This paper identifies a systematic gap between legal interpretation and formal logic in AI legal reasoning, proposes a neuro-symbolic approach to bridge it, and demonstrates substantial label shifts when re-annotating legal NLI data under strict formal entailment.
LLM-as-a-Verifier (GitHub Repo)
LLM-as-a-Verifier is a general-purpose verification framework that provides fine-grained feedback for AI agents, achieving state-of-the-art performance on benchmarks like Terminal-Bench and SWE-Bench.