Technische Samenvatting: Aan Hun Vruchten Zult Gij Ze Kennen

Probleemstelling

De formalisering van wettelijke bepalingen in machine-leesbare structuren belooft geautomatiseerd juridisch redeneren en machine-toegankelijke wetgeving. Met de opkomst van Large Language Models (LLM's) is het haalbaar geworden om deze formalisaties rechtstreeks uit wetteksten te genereren. Elke formalisering houdt echter inherent impliciete interpretatieve keuzes in. Wanneer een LLM als auteur optreedt, zijn deze keuzes ondoorzichtig en zijn de gevolgen van afwijkende interpretaties moeilijk te anticiperen. Een formalisering die structureel correct lijkt, kan in randgevallen die niet door de opsteller werden voorzien, onrechtvaardige of onjuiste vonnissen opleveren.

De kernuitdaging die wordt aangepakt, is hoe men systematisch meerdere formalisaties van dezelfde wettelijke bepaling kan vergelijken om te identificeren waar ze divergeren in hun logische uitkomsten, in plaats van enkel hun structurele gelijkenis te vergelijken. Bestaande methoden vertrouwen vaak op structurele matching of vergelijking met een "gouden standaard", maar de auteurs betogen dat het vergelijken van formalisaties met elkaar, zonder een grondwaarheid aan te nemen, noodzakelijk is om echte interpretatieve ambiguïteiten en fouten aan het licht te brengen.

Methodologie

De auteurs stellen een vierfasenpijplijn voor om door LLM's gegenereerde formalisaties van wettelijke bepalingen te vergelijken:

1. Formalisering:
   Negen toonaangevende LLM's krijgen de opdracht om formalisaties te genereren voor tien verschillende EU-wettelijke bepalingen (variërend van AVG, AI-wet, DMA, enz.). Elke formalisatie wordt weergegeven als een gewortelde, gelabelde boom waarbij de bladknopen invoervariabelen (feiten) zijn en de interne knopen logische operatoren (EN, OF, NAND, NOR). De wortel vertegenwoordigt de binaire juridische consequentie (bijvoorbeeld "verboden" of "toegestaan").

2. Matching (Constructie van een Graaf van Equivalentieklassen):
   Om bomen met mogelijk verschillende structuren te vergelijken, identificeert de methode knopen in verschillende formalisaties die hetzelfde juridische concept vertegenwoordigen. Een LLM (specifiek Claude Opus 4.6, geselecteerd omwille van consistentie) groepeert knopen uit alle formalisaties in Equivalentieklassen (EK's). Dit creëert een gedeelde vocabulaire (interface) voor vergelijking. Het matchingproces zorgt ervoor dat elke formalisatie maximaal één knoop bijdraagt aan een gegeven EK, waardoor een gerichte acyclische graaf (DAG) van concepten ontstaat.

3. Randgevalanalyse (SAT-gebaseerde Enumeratie):
   Voor elk paar formalisaties definieert de methode een gedeelde interface op basis van de diepste EK's die aan beide gemeenschappelijk zijn. Het vertaalt de sub-bomen boven deze interface naar Booleaanse functies ($f_A$ en $f_B$).

   • Het systeem berekent de disagree-functie $f_A \oplus f_B$.
   • Met behulp van een SAT-oplosser (Z3) worden primaire implicanten van deze disagree-functie geënumereerd. Een primaire implicant vertegenwoordigt een minimale set invoercondities (een gedeeltelijke toewijzing) die de twee formalisaties dwingt tot onenigheid, ongeacht de waarden van andere niet-toegewezen variabelen.
   • Deze primaire implicanten worden behandeld als "randgevallen".

4. Verbalisering:
   Ruwe primaire implicanten zijn niet menselijk interpreteerbaar. De auteurs passen een selectiepijplijn toe om de set randgevallen te reduceren tot een representatieve subset (groepering op basis van "oorzaken" van onenigheid). Deze geselecteerde gevallen worden vervolgens door een LLM verbaal uitgewerkt tot concrete, realistische feitelijke scenario's. De verbalisering omvat het scenario, de specifieke juridische vraag en een analyse van de interpretatieve divergentie, waardoor juridische experts het specifieke punt van geschil kunnen beoordelen.

Belangrijkste Bijdragen

Het artikel levert drie primaire bijdragen:

1. Een Kader voor Comparatieve Formalisering: Een methode om systematisch verschillende formalisaties van dezelfde wettelijke bepaling te vergelijken door de specifieke invoergevallen te enumereren waarop ze het oneens zijn, in plaats van te vertrouwen op aggregate structurele gelijkenis.
2. Verbalisering van Randgevallen: Een techniek om uit SAT afgeleide logische randgevallen (primaire implicanten) om te zetten in concrete feitelijke scenario's die juridische experts kunnen evalueren, waardoor de kloof tussen formele verificatieartefacten en menselijk juridisch redeneren wordt overbrugd.
3. Empirische Studie van LLM-Formalisaties: Een toepassing van deze methode op negen toonaangevende LLM's die tien EU-bepalingen formaliseren. De studie onthult dat gedragsdivergentie grotendeels ongecorreleerd is met structurele overeenstemming en dat verbaal uitgewerkte gevallen kwalitatief verschillende soorten onenigheid blootleggen, waaronder die welke echte controverses in juridische commentaren weerspiegelen.

Resultaten

De studie genereerde 90 formalisaties (9 modellen $\times$ 10 bepalingen) en analyseerde 360 paren.

• Structurele versus Gedragsdivergentie: De auteurs vonden dat hoge structurele overeenstemming (gemeten aan de dekking van de gedeelde interface) geen logische equivalentie garandeert. Zelfs wanneer formalisaties goed overeenkwamen op concepten (hoge dekking), waren ze vaak het oneens over uitkomsten. Omgekeerd waren paren met lage dekking vaak triviaal equivalent, simpelweg omdat ze geen gedeelde structuur hadden om over het oneens te zijn.
• Modellvariatie: De onenigheidspercentages varieerden aanzienlijk tussen modellen (variërend van ongeveer 32% tot ongeveer 71% van de paren die niet-equivalent waren), maar geen enkel model was uniform "grensoverschrijdend". Het gedrag was sterk afhankelijk van de bepaling, waarbij sommige modellen varieerden van 0% tot 100% onenigheid over verschillende bepalingen.
• Kwalitatieve Bevindingen:
  • Interpretatieve Ambiguïteit: In het geval van Artikel 5 van de AI-wet (betreffende biometrische categorisering voor handhaving) splitsten de modellen zich gelijk (4 tegen 4) over de vraag of een specifieke uitzondering van toepassing was. Deze divergentie weerspiegelde een echte, aanhoudende controverse in juridische commentaren over de reikwijdte van de uitzondering.
  • Formalisatiefouten: In het geval van Artikel 3 van de Richtlijn oneerlijke bedingen in consumentovereenkomsten (UCTD) codeerde één model (Kimi K2.5) een procedurele bewijslastregel onjuist als een aanvullende materiële vereiste (conjunction in plaats van disjunction), wat leidde tot een te beperkende definitie.
  • Beperkingen: De pijplijn brengt alleen onenigheden aan het licht; het kan geen fouten detecteren die door alle modellen worden gedeeld (bijvoorbeeld als alle modellen een kruisverwijzing in de wet missen).

Betekenis en Claims

Het artikel beweert dat "de wet kennen betekent haar vonnissen kennen". De betekenis ligt in de verschuiving van de evaluatie van juridische formalisaties van statische structurele analyse naar dynamische, op uitkomsten gebaseerde vergelijking.

• Auditsteun, geen Automatisering: De auteurs stellen expliciet dat hun pijplijn bedoeld is als een "mens-in-de-lus auditsteun", en niet als een component van een geautomatiseerd juridisch beslissingsysteem. De formalisaties zijn niet gevalideerd voor autonoom gebruik.
• Blootleggen van Verborgen Divergentie: De methode demonstreert dat puur structurele vergelijking ontoereikend is. Twee formalisaties kunnen er vergelijkbaar uitzien maar in specifieke randgevallen radicaal verschillende juridische uitkomsten opleveren.
• Weerspiegeling van Juridisch Discours: De verbaal uitgewerkte randgevallen hebben succesvol onenigheden aan het licht gebracht die overeenkomen met echte, onopgeloste debatten in de juridische wetenschap, wat suggereert dat LLM's niet willekeurig hallucineren, maar worstelen met dezelfde ambiguïteiten waar menselijke experts mee geconfronteerd worden.

De auteurs concluderen dat hoewel hun methode beperkingen heeft (afhankelijkheid van LLM-matching, gebrek aan externe juridische context en het onvermogen om correctheid te verifiëren zonder een gouden standaard), het een noodzakelijk mechanisme biedt om de wet te "kennen" via de beslissingen die zijn formalisaties coderen.