Technische Samenvatting: Geluidige en Volledige Neurosymbolische Redenering met LLM-gegronde Interpretaties

Probleemstelling

Large Language Models (LLMs) beschikken over een enorme parametrische kennis, maar lijden aan inherente inconsistenties en onvolledigheid, waardoor ze als zelfstandige kennisbases voor formele redenering onbetrouwbaar zijn. Traditionele benaderingen van neurosymbolische redenering — zoals het prompten van LLMs om logische redeneringen uit te voeren, het gebruiken van hen om symbolische inputs voor externe solvers te genereren, of het finetunen van hen op bewijzen — falen in het bieden van formele garanties met betrekking tot de geluidheid (soundness) en volledigheid (completeness) van het redeneerproces wanneer de kennis van de LLM tegenstrijdig is. Bovendien leveren standaard methoden voor de evaluatie van feitelijkheid doorgaans een enkele waarheidswaarde, wat de epistemische staat van de LLM (bijv. of deze onzeker of werkelijk in conflict is) verbergt. De kernuitdaging is hoe de brede kennis van een LLM kan worden geïntegreerd in een formeel redeneersysteem terwijl de theoretische eigenschappen van de logica (geluidheid en volledigheid) behouden blijven en de inconsistenties die de LLM produceert effectief worden beheerd.

Methodologie

De auteurs stellen een raamwerk voor dat een LLM direct integreert in de interpretatiefunctie van een paraconsistente logica, specifiek Analytic Containment (AC), een bilaterale logica die in staat is om met inconsistente informatie om te gaan zonder logische explosie.

1. Bilaterale Feitelijkheidsevaluatie

In plaats van een LLM te vragen om een enkele waarheidswaarde toe te kennen (Waar/Onwaar), gebruikt het systeem een bilaterale evaluatiebenadering. Een LLM-beoordelaar wordt geprompt om onafhankelijk twee condities te beoordelen voor een atomaire formule $\phi$:

• Verificatie ($P^+$): Kan de LLM $\phi$ verifiëren?
• Refutatie ($P^-$): Kan de LLM $\phi$ weerleggen?

De outputs worden toegewezen aan zwakke Kleene-waarheidswaarden ($t$=waar, $f$=onwaar, $e$=ongedefinieerd/onbekend). Deze worden gekoppeld om een gegeneraliseerde waarheidswaarde $\langle u, v \rangle \in V_3 \times V_3$ te vormen. Dit resulteert in vier primaire toestanden:

• $\langle t, f \rangle$: Geverifieerd (Waar).
• $\langle f, t \rangle$: Weerlegd (Onwaar).
• $\langle t, t \rangle$: Glut (Zowel geverifieerd als weerlegd; inconsistentie).
• $\langle f, f \rangle$: Gap (Niet geverifieerd noch weerlegd; onzekerheid/onwetendheid).

Om de stabiliteit te garanderen die vereist is voor formele redenering, wordt een cachingmechanisme ($\zeta_c$) gebruikt, dat de waardering van atomaire formules onveranderlijk opslaat zodra deze is berekend.

2. LLM-gegronde Interpretaties

Het artikel definieert een LLM-gegronde interpretatie ($I$) waarbij de interpretatie van atomaire formules wordt bepaald door de gecachte bilaterale evaluatiefunctie $\zeta_c$.

• Theoretische Integratie: De auteurs bewijzen dat er voor elke LLM-gegronde interpretatie een equivalente standaardinterpretatie bestaat, en vice versa.
• Behoud van Eigenschappen: Ze demonstreren dat de geluidheid en volledigheid van het analytische tableau-systeem voor AC (specifiek $AC^{rQ}$) behouden blijven, zelfs wanneer de interpretatie gegrond is in een LLM. Dit betekent dat de redeneerder conclusies kan afleiden met dezelfde garanties als een standaardlogica, ondanks de potentiële inconsistentie van de LLM.

3. Implementatie: Een Belnap Computer

De auteurs hebben een proof-of-concept Belnap computer (een redeneerder ontworpen om met inconsistente informatie om te gaan) geïmplementeerd in Python.

• Architectuur: Het combineert forward-chaining inferentie (het afleiden van nieuwe feiten uit regels) met tableau-gebaseerde verzadigbaarheidstoetsing (satisfiability checking).
• LLM-evaluatieregel: Tijdens de tableau-constructie roept een llm-eval regel de LLM-beoordelaar aan voor de bilaterale waarheidswaarde van atomaire formules.
• Glut-afhandeling: Wanneer een glut wordt gedetecteerd (bijv. het systeem leidt $P(a)$ af, maar de LLM weerlegt het), sluit het tableau niet (explodeert niet). In plaats daarvan behoudt het zowel de bewering als de weerlegging, waardoor de tegenstrijdigheid wordt gelokaliseerd.

Belangrijkste Bijdragen

1. Bilaterale Feitelijkheidsevaluatie: Een nieuwe methode die de epistemische staat van de LLM (consistent, inconsistent of onzeker) naar boven brengt in plaats van een binaire beslissing af te dwingen, wat meer bruikbare diagnostiek oplevert dan unilaterale evaluatie.
2. LLM-gegronde Interpretaties: Een theoretisch raamwerk dat LLMs direct integreert in de formele semantiek van een paraconsistente logica, waarbij de geluidheid en volledigheid van het onderliggende redeneersysteem behouden blijven.
3. Empirische Validatie: Demonstratie dat bilaterale evaluatie de macro-F1-scores over unilateral baselines verbetert (met ongeveer 6 procentpunten) op feitelijkheidsbenchmarks (GPQA en SimpleQA), zij het met een lagere dekking door afzien van onzekere gevallen.
4. Praktisch Systeem: Een werkende implementatie van een Belnap computer die succesvol medisch significante fouten (gluts) in een kennisbank detecteert terwijl de algehele verzadigbaarheid behouden blijft.

Experimentele Resultaten

De auteurs hebben de aanpak geëvalueerd met behulp van datasets afgeleid van de GPQA en SimpleQA benchmarks met verschillende LLMs (flagship en gedestilleerde modellen).

• Nauwkeurigheid vs. Dekking: Bilaterale evaluatie bereikte een hogere macro-F1-score (ongeveer 0,699 voor flagship modellen op GPQA) vergeleken met unilaterale baselines (0,633), maar met een lagere dekking (0,589 vs. 1,000). Het systeem onthoudt zich van inconsistente ($\langle t, t \rangle$) of onzekere ($\langle f, f \rangle$) gevallen, wat leidt tot een hogere betrouwbaarheid op de gevallen waar het wel een antwoord geeft.
• Epistemische Staten: De experimenten toonden aan dat LLMs frequent gluts (inconsistenties) produceren in plaats van gaps. Bijvoorbeeld, op de SimpleQA-dataset vertoonden GPT-modellen een hoge neiging tot tegenstrijdigheid (glut-percentages ~59%), terwijl Claude-modellen voorzichtiger waren (hogere gap-percentages).
• Gebruiksscenario Medische Veiligheid: Het systeem werd toegepast op een kennisbank van 228 geëerdeerde en 712 geïnfereerde stellingen met betrekking tot medicijnveiligheid.
  • Het detecteerde 92 gluts die overeenkwamen met medisch significante fouten (bijv. het afleiden dat opioïden niet verslavend zijn of dat bètablokkers veilig zijn voor astmapatiënten).
  • Ondanks deze 92 tegenstrijdigheden bleef het systeem verzadigbaar (satisfiable), waarbij het de fouten succesvol lokaliseerde zonder een logische explosie te veroorzaken.
  • Computationele analyse toonde aan dat de latentie van de LLM de dominante bottleneck is, maar dat de aanpak schaalbaar is naar middelgrote kennisbanken (100k+ stellingen) met standaardoptimalisaties zoals parallellisatie en caching.

Betekenis en Claims

Het artikel beweert een theoretisch raamwerk met een praktische implementatie te bieden voor neurosymbolische redenering die de kennis van een LLM benut terwijl de geluidheid en volledigheid van de onderliggende logica behouden blijven.

• Paradigmaverschuiving: In tegen tegenstelling tot eerder werk dat probeert LLMs te laten redeneren met logica, maakt deze aanpak de logica redeneren met de LLM als een interpretatie-orakel.
• Robuustheid: Het systeem is ontworpen voor real-world scenario's waar kennisbronnen inherent inconsistent zijn. Het behandelt tegenstrijdigheden niet als fatale fouten die hersteld moeten worden, maar als gelokaliseerde epistemische staten (gluts) die kunnen worden geïdentificeerd en beheerd.
• Actiegerichte Diagnostiek: Door onderscheid te maken tussen "in conflict" (glut) en "onwetend" (gap) staten, biedt het systeem downstream toepassingen specifieke informatie over waarom een conclusie onzeker is, wat conservatievere en veiligere besluitvorming mogelijk maakt (bijv. in medische contexten).
• Schaalbaarheid: De auteurs stellen dat hoewel de latentie van de LLM API momenteel de primaire kostenpost is, de logische overhead minimaal is en het systeem tractabel is voor productie-schaal kennisbanken met behulp van bestaande optimalisatietechnieken uit description logic reasoners.