Back to today's list

By Their Fruits You Will Know Them: Comparing Formalizations of Law by the Decisions They Encode

Julius Vernie, Matthias Grabmair

Published Sep 18, 2026
Editorial review7.5
Relevance0.453
Freshness0.000

Why It Matters

What makes this one worth your time

This research addresses the critical challenge of ensuring reliable legal reasoning in automated systems, which is essential for the future of machine-accessible law.

A novel approach to evaluate legal formalizations through comparative analysis of case inferences.

Summary

The paper presents a method for systematically comparing different formalizations of legal provisions by analyzing their inferences on individual cases, revealing divergences that reflect genuine legal controversies.

Key contributions

  • Development of a systematic comparison method for legal formalizations.
  • Application of a SAT solver to derive edge cases of disagreement.
  • Identification of qualitatively distinct types of disagreement in legal interpretations.

Notable insights

  • The method utilizes a SAT solver to identify edge cases of disagreement between formalizations, which is a clever application of formal methods in legal contexts.
  • The finding that behavioral divergence is uncorrelated with structural agreement suggests deeper complexities in legal interpretation that may not be captured by traditional formalization methods.

Possible limitations

  • Not stated in the abstract.

Abstract

arXiv:2605.25186v2 Announce Type: replace-cross Abstract: Formalizing legal provisions promises machine-accessible law and automated legal reasoning, and recent LLMs make it tempting to generate such formalizations directly from statutory text. However, any formalization makes implicit interpretive choices whose consequences are hard to anticipate, especially if an LLM is the author. We present a method for systematically comparing different formalizations of the same legal provision by their inferences on individual cases. Given multiple formalizations of a provision, we match them at the node level, derive a shared interface for each pair from the matching, and use a SAT solver to enumerate the edge cases on which any two formalizations disagree. Selected edge cases are then verbalized into concrete factual scenarios that a legal expert can examine and act on. We apply our method to formalizations of ten EU provisions generated by nine frontier LLMs. We find that behavioral divergence between formalizations is essentially uncorrelated with their structural agreement and that the verbalized cases reveal qualitatively distinct types of disagreement, including divergences that mirror genuine controversies in the legal commentary.