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

arXiv: https://arxiv.org/abs/2605.25186 · HTML: https://mlsanity.com/paper/2605.25186/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning for agents, planning and code, one of 17 directions in LLM reasoning.
- Builds on 9 of its 35 references that are in the map.
- First posted on arXiv 24 May 2026.

## Placed in

- LLM reasoning / [Reasoning for agents, planning and code](https://mlsanity.com/lr/reasoning-for-agents-planning-and-code/)

## Builds on (most cited first, 9 of 9)

- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [Catala: A Programming Language for the Law](https://mlsanity.com/paper/2103.03198/) (2021)
- [Schema Matching with Large Language Models: an Experimental Study](https://mlsanity.com/paper/2407.11852/) (2024)
- [From Text to Structure: Using Large Language Models to Support the Development of Legal Expert Systems](https://mlsanity.com/paper/2311.04911/) (2023)
- [The Legislative Recipe: Syntax for Machine-Readable Legislation](https://mlsanity.com/paper/2108.08678/) (2021)
- [Pacta sunt servanda: legal contracts in Stipula](https://mlsanity.com/paper/2110.11069/) (2021)
- [A systematic literature review on counterexample explanation](https://mlsanity.com/paper/2201.03061/) (2022)
- [Automated Consistency Analysis for Legal Contracts](https://mlsanity.com/paper/2504.18422/) (2025)
- [From Legal Text to Executable Decision Models: Evaluating Structured Representations for Legal Decision Model Generation](https://mlsanity.com/paper/2604.17153/) (2026)

## Abstract (arXiv)

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.