Technische Samenvatting: Ken je grenzen: Over de getrouwheid van LLM's als oplosders en autoformaliseerders in juridische redenering

Probleemstelling

De adoptie van Large Language Models (LLM's) in hoogwaardige juridische domeinen wordt gehinderd door het gebrek aan getrouwe en verifieerbare redenering. Hoewel technieken zoals Chain-of-Thought de prestaties verbeteren, blijven LLM's vatbaar voor hallucinaties en een afhankelijkheid van heuristische benaderingen in plaats van strikte logische inferentie. Er bestaat een kritieke ambiguïteit in juridische teksten: correcte conclusies hangen vaak af van impliciete aannames die niet expliciet in het contract staan vermeld. Dit creëert een kloof tussen pragmatische juridische interpretatie (wat mensen afleiden) en strikte formele implicatie (wat logisch afleidbaar is).

Bestaande neuro-symbolische benaderingen, die LLM-gebaseerde autoformalisering combineren met symbolische solvers, worden geconfronteerd met een fundamentele beperking: formele redenering vereist expliciete aannames, terwijl juridische tekst inherent ondergespecificeerd is. Voorgaand werk heeft aangetoond dat door LLM gegenereerde formaliseringen incompleet of inconsistent kunnen zijn, maar het blijft onduidelijk of prestatiewinsten in "LLM-gebaseerde formele redenering" ten koste gaan van de getrouwheid aan de onderliggende symbolische logica.

Methodologie

De auteurs evalueren drie redeneerparadigma's op een opnieuw geannoteerde subset van de ContractNLI dataset (afgeleid van echte Non-Disclosure Agreements) over vijf LLM's (GPT-OSS-120B, Claude-Sonnet-4-6, Meta-Llama-3.1-8B, DeepSeek-V3.2, en Qwen2.5-72B):

1. Pure LLM Classificatie: Directe classificatie van natuurlijke taal premissen en hypothesen.
2. LLM-gebaseerde Formele Redenering: De LLM autoformaliseert tekst naar Eerste-Orde Logica (FOL) en voert vervolgens de classificatie zelf uit, waarbij een solver wordt gesimuleerd.
3. Solver-gebaseerde Formele Redenering: De LLM autoformaliseert tekst naar FOL (specifiek SMT-LIB), die vervolgens wordt uitgevoerd door de Z3 SMT solver om verzadigbaarheid (SAT/UNSAT) te bepalen en implicatie, contradictie of neutraliteit te classificeren.

Dataset Constructie

De auteurs hebben 400 voorbeelden uit ContractNLI opnieuw geannoteerd om aan te sluiten bij strikte formele semantiek:

• Implicatie (Entailment): $P \land \neg H$ is onvervulbaar.
• Contradictie (Contradiction): $P \land H$ is onvervulbaar.
• Neutraal (Neutral): Omvat semantisch irrelevante gevallen en gevallen waar de premisse onvoldoende is zonder aanvullende aannames.

Deze her-annotatie onthulde een systematische verschuiving: veel oorspronkelijke "Entailment" en "Contradiction" labels werden geherclassificeerd als "Neutral" omdat ze vertrouwden op niet-gestelde aannames. De dataset werd uitgebreid naar 610 voorbeelden door minimale paren te creëren die expliciet ontbrekende aannames leveren om de rol van impliciete kennis te testen.

Neuro-Symbolische Pipeline

De pipeline scheidt taalbegrip van logische redenering:

1. Autoformaliseerder: Gebruikt gestructureerde prompting (clausule-identificatie, predicaat-normalisatie en expliciete aanname-encodering) om juridische tekst naar FOL te vertalen.
2. Solver: Gebruikt Z3 om verzadigbaarheidstests uit te voeren op de gegenereerde FOL.
3. Vergelijking: De auteurs vergelijken de classificatie van de LLM van de FOL-inputs met de output van de Z3 solver om te identificeren waar de LLM afwijkt van de formele logica.

Belangrijkste Bijdragen

1. Prestatie vs. Getrouwheid Gap: De studie toont aan dat het toevoegen van een formele structuur de benchmark-nauwkeurigheid verbetert (waarbij LLM-gebaseerde Formele Redenering de hoogste scores behaalt), maar dat dit niet impliceert dat er spetrouwwe redenering plaatsvindt.
2. Identificatie van Foutmodi: De auteurs identificeren drie terugkerende foutmodi in LLM's die formele redenering proberen uit te voeren:
   • Scope Laundering (Scope-witwassen): LLM's rapporteren classificaties die consistent zijn met een solver (bijv. Implicatie) zonder de onderliggende formele redenering daadwerkelijk uit te voeren. Ze produceren plausibele outputs die logisch gegrond lijken te zijn, maar niet zijn afgeleid van de symbolische executie. Dit komt voor bij alle modellen (variërend van 15,3% bij GPT tot 52,5% bij Qwen).
   • Blindheid voor Impliciete Constraints: LLM's negeren logische restricties die aanwezig zijn in de formele representatie (bijv. universalen gecodeerd binnen existentiële structuren), wat leidt tot onjuiste inferenties ondanks de aanwezigheid van de formele input.
   • Programmasynthese Fouten: LLM's genereren frequent incorrecte Z3-code (syntaxfouten, type-mismatches, scope-fouten), waardoor de uitvoering door de solver wordt verhinderd.
3. Aanname Ambiguïteit: Het werk benadrukt dat de grens tussen een geldige inferentie en een ongegronde aanname vaak onduidelijk is, zelfs voor menselijke annotatoren (de inter-annotator overeenstemming was substantieel, maar de onenigheid concentreerde zich tussen Entailment en Neutral).
4. Data Gap: De studie onthult een fundamentele kloof tussen benchmark-labels (die pragmatische interpretatie reflecteren) en formele logische semantiek in real-world juridische data.

Resultaten

• Nauwkeurigheid: LLM-gebaseerde Formele Redenering behaalde de hoogste nauwkeurigheid (bijv. 83,0% voor Claude), waarmee zowel pure LLM-classificatie als solver-gebaseerde redenering werd overtroffen.
• Getrouwheid: Solver-gebaseerde redenering was het meest conservatief en classificeerde vaak gevallen als Neutraal waar LLM's Implicatie voorspelden. Dit geeft aan dat LLM's informatiekloven overbruggen met impliciete aannames die de solver verwerpt.
• Foutanalyse: De dominante foutmodus over alle modellen was Neutral $\to$ Entailment, wat bevestigt dat LLM's systematisch ongegronde aannames introduceren.
• Scope Laundering: Dit werd geïdentificeerd als een kritiek probleem waarbij modellen beweren formele redenering te gebruiken, maar eigenlijk vertrouwen op heuristische benadering, wat de betrouwbaarheid van "LLM-gebaseerde formele redenering" als proxy voor symbolische executie ondermijnt.

Betekenis en Claims

Het paper betoogt dat benchmark-nauwkeurigheid een slechte proxy is voor logische getrouwheid in juridische redenering. De primaire betekenis ligt in het blootleggen van het "black box"-karakter van LLM's, zelfs wanneer ze worden geprompt om formele instrumenten te gebruiken.

• Getrouwheid vs. Prestatie: De auteurs claimen dat de prestatieverbetering gezien bij LLM-gebaseerde formele redenering ten koste gaat van de getrouwheid. Modellen "faken" vaak de executie van symbolische solvers (scope laundering) of falen in het vastleggen van noodzakelijke restricties.
• De Rol van Aannames: De studie stelt dat de kernuitdaging niet de keuze van de formalisme (bijv. FOL) is, maar het onvermogen van huidige modellen om betrouwbaar de minimale set aannames te identificeren en te coderen die nodig zijn om van Neutraal naar Entailment/Contradiction te gaan.
• Human-in-the-loop: De auteurs concluderen dat AI alleen de inherente ambiguïteit van juridische teksten niet kan oplossen. In plaats daarvan moeten systemen worden ontworpen om Minimal Correction Subsets (MCS) te presenteren — de specifieke aannames die nodig zijn om een classificatie te verschuiven — waardoor menselijke juridische experts gerichte beslissingen kunnen nemen op die specifieke ambiguïteiten in plaats van een volledige documentverificatie uit te voeren.

Het werk dient als een waarschuwing voor de inzet van LLM's in hoogwaardige juridische settings, waarbij wordt benadrukt dat "gestructureerde" redenering geen "getrouwe" redenering garandeert zonder rigoureuze verificatie van de onderliggende symbolische executie.