Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

Dit paper introduceert Delta1 met LLM, een neuro-symbolisch raamwerk dat de formele strengheid van de Automatische Theorema Generator Delta1 combineert met de verbaal vermogens van grote taalmodellen om betrouwbare en uitlegbare redenering te realiseren.

De kern

Stel je voor dat je een zeer slimme, maar soms wat chaotische vertaler hebt (een LLM, of "Groot Taalmodel"). Deze vertaler kan prachtige verhalen vertellen, maar hij maakt soms fouten in de logica of verzonnen feiten. Aan de andere kant heb je een wiskundige die onfeilbaar is, maar die alleen in droge formules spreekt en geen menselijke uitleg kan geven.

Dit paper introduceert ∆1–LLM: een team-up van deze twee, zodat je de beste van beide werelden krijgt. Het is alsof je een onfeilbare architect (de wiskundige) en een charmante gids (de vertaler) samenwerkt om een huis te bouwen dat zowel stevig is als makkelijk te begrijpen.

Hier is hoe het werkt, in gewone taal:

1. Het Probleem: De "Gouden Kooi" van de Waarheid

Stel je voor dat je een set regels hebt voor een ziekenhuis, een wetboek of een contract. Soms zijn deze regels in strijd met elkaar.

• Regel A zegt: "Als je koorts hebt, moet je antibiotica nemen."
• Regel B zegt: "Als je een virus hebt, mag je géén antibiotica nemen."
• Regel C zegt: "Je hebt koorts én een virus."

Een gewone computer of AI kan hierin verwarren raken of een willekeurig antwoord geven. Een traditionele wiskundige computer kan zeggen: "Dit is onmogelijk!" maar kan niet uitleggen waarom of wat je moet doen om het op te lossen.

2. De Oplossing: De "Onfeilbare Architect" (∆1)

De eerste helft van het systeem is ∆1. Denk aan ∆1 als een super-precieze architect die alleen werkt met een specifieke bouwmethode (genaamd FTSC).

• Hoe het werkt: In plaats van te gissen of te zoeken naar een oplossing (zoals een mens die probeert een puzzel op te lossen), bouwt ∆1 de regels op een manier die per definitie perfect is.
• De Analogie: Stel je voor dat je een set Lego-blokjes hebt. ∆1 pakt deze blokjes en bouwt er een structuur mee die per definitie instabiel is als je één specifiek blokje verwijdert.
• Het resultaat: ∆1 vindt automatisch de kleinste groep regels die samen een "bom" vormen (een tegenstrijdigheid). Omdat hij dit op een vaste, wiskundige manier doet, is hij 100% zeker dat zijn conclusie klopt. Er is geen gokken bij betrokken.

3. De Vertaler: De "Charmante Gids" (LLM)

Nu hebben we een wiskundige conclusie: "Regel 3 is de bom." Maar wat betekent dat voor een dokter of een jurist?

• Hier komt de LLM (het taalmodel) om de hoek kijken.
• De Analogie: De architect (∆1) geeft de blauwdruk van de instabiele muur. De gids (LLM) kijkt naar die blauwdruk en zegt tegen de bewoner: "Kijk, deze muur valt om als je dit raam openzet. Het probleem is dat dit raam te groot is voor deze muur. Als je het raam kleiner maakt of de muur versterkt, is het huis veilig."
• De LLM vertaalt de droge wiskundige "bom" naar een begrijpelijke uitleg: "Je kunt niet tegelijkertijd antibiotica voorschrijven en een virus hebben. Je moet eerst testen of het een bacterie is."

4. Het Samenwerkingsproces: "Uitleg door Bouwen"

Het mooie aan dit systeem is dat de uitleg niet na het denken komt, maar tijdens het bouwen.

1. Invoer: Je geeft de regels in (bijv. "Als koorts, dan antibiotica").
2. Bouwen (∆1): De architect bouwt direct de "onmogelijke situatie" op en vindt precies welk blokje de oorzaak is. Hij doet dit in een fractie van een seconde en zonder fouten.
3. Vertalen (LLM): De gids neemt die exacte oorzaak en vertaalt het naar mensentaal, inclusief een advies: "Pas deze regel aan door een test toe te voegen."

Waarom is dit belangrijk?

In het verleden moesten we kiezen tussen:

• AI die slim klinkt maar fouten maakt (zoals een acteur die een script voorleest zonder de plot te begrijpen).
• Wiskunde die perfect is maar onbegrijpelijk (zoals een recept in een vreemde taal).

Met ∆1–LLM krijgen we:

• Vertrouwen: Omdat de wiskundige kant (∆1) de basis is, weten we dat de conclusie klopt. Geen hallucinaties.
• Begrip: Omdat de taal-kant (LLM) de uitleg geeft, weten mensen waarom het zo is en wat ze moeten doen.

Een Praktijkvoorbeeld uit het Paper

Stel je een ziekenhuis voor.

• De Regels: "Als koorts -> antibiotica", "Als virus -> géén antibiotica", "Patiënt heeft koorts en virus".
• ∆1 (De Architect): Zegt: "Als je deze drie regels samenzet, krijg je een onmogelijke situatie. Het 'antibiotica'-blokje is de oorzaak van de instabiliteit."
• LLM (De Gids): Zegt: "Dit is gevaarlijk. De regels zeggen dat je antibiotica moet geven, maar de patiënt heeft een virus, dus dat is verkeerd. Advies: Voeg een regel toe: 'Geef alleen antibiotica als er een bacteriële infectie is bevestigd'."

Conclusie

Dit paper beschrijft een manier om AI te maken die niet alleen "slim" klinkt, maar ook waarheid spreekt en dat begrijpelijk maakt voor mensen. Het is als het geven van een kompas (de wiskunde) en een gids (de taal) aan iemand die door een wirwar van regels probeert te navigeren. Zo bouwen we AI-systemen die we kunnen vertrouwen, controleren en begrijpen.

Technische samenvatting

Titel

∆1–LLM: Symbolische-Neurale Integratie voor Betrouwbare en Verklaarbare Redenering

1. Het Probleem

De huidige neuro-symbolische redenering (de combinatie van symbolische logica en neurale netwerken) kampt met een fundamenteel spanningsveld:

• Symbolische systemen (zoals geautomatiseerde theorema-proevers) bieden formele geldigheid (soundness) en transparante inferentiestructuren, maar missen vaak linguïstische expressiviteit en kunnen geen natuurlijke taalverklaringen genereren.
• Neurale modellen (zoals Large Language Models of LLM's) bieden vloeiheid, aanpassingsvermogen en menselijke begrijpelijkheid, maar missen garanties voor correctheid; hun redenering is vaak stochastisch en niet verifieerbaar.

Bestaande hybride systemen proberen deze kloof te overbruggen, maar leveren vaak alleen benaderende redeneringen of ontberen formele garanties. Er is een behoefte aan een architectuur waar logische validiteit en natuurlijke taal-verklaringen per constructie naast elkaar bestaan, zonder afhankelijkheid van stochastische zoekprocessen.

2. Methodologie: Het ∆1 + LLM Framework

Het artikel introduceert een end-to-end pipeline genaamd ∆1 + LLM, die een deterministische symbolische generator koppelt aan een neurale interpretatielaag.

A. De Symbolische Kern: ∆1 (Automated Theorem Generator)

∆1 is een deterministische theorema-generator gebaseerd op het concept van Full Triangular Standard Contradiction (FTSC).

• Invoer: Een verzameling van $n$ niet-complementaire, unieke atomaire predikaten ($L = \{x_1, ..., x_n\}$).
• Constructie: ∆1 bouwt een specifieke clausuleverzameling $S$ op volgens het FTSC-schema:
  • $D_1 = x_1$
  • $D_2 = x_2 \lor \neg x_1$
  • ...
  • $D_{n+1} = \neg x_1 \lor \neg x_2 \lor ... \lor \neg x_n$
• Werkingsprincipe: Deze verzameling is per definitie onbevredigbaar (unsatisfiable). ∆1 genereert voor elke clausule $C$ in de verzameling een theorema van de vorm $S \setminus \{C\} \vdash \neg C$. Dit betekent dat het verwijderen van één clausule de verzameling bevredigbaar maakt, maar die verwijderde clausule door de rest van de verzameling wordt weerlegd.
• Garanties:
  • Deterministisch: Geen zoekprocessen, geen backtracking, geen probabilistische keuzes.
  • Minimaal: Elke gegenereerde theorema vertegenwoordigt een Minimal Unsatisfiable Subset (MUS).
  • Compleet: Het systeem genereert exact $n!$ niet-equivalente theorema's voor een invoer van grootte $n$.
  • Complexiteit: De constructie van een enkel FTSC kost $O(n^3)$ tijd.

B. De Neuraal-Linguïstische Laag: LLM

De LLM fungeert als een semantische vertaler en rangschikker:

1. Predikaatextractie: De LLM converteert natuurlijke taal (bijv. beleidsregels) naar formele atomaire predikaten in TPTP-syntaxis.
2. Verbaal maken (Verbalization): De LLM vertaalt de formele bewijstraces en theorema's van ∆1 naar samenhangende natuurlijke taalverklaringen.
3. Rangschikking: De LLM beoordeelt de relevantie, nieuwswaarde of contextuele urgentie van de geïdentificeerde tegenstrijdigheden.
4. Remediatie: De LLM stelt concrete oplossingen voor om de logische inconsistentie op te lossen.

C. De Pipeline ("Explainability by Construction")

In tegenstelling tot post-hoc interpretatie (waarbij men probeert een "black box" te verklaren), is hier de interpretatie ingebouwd in het bouwproces:

1. Natuurlijke taal invoer $\rightarrow$ LLM $\rightarrow$ Predikaten.
2. Predikaten $\rightarrow$ ∆1 $\rightarrow$ Deterministische theorema's en bewijstraces.
3. Theorema's $\rightarrow$ LLM $\rightarrow$ Menselijke verklaringen en actiepunten.

3. Belangrijkste Bijdragen

1. Integratiepijplijn: Een nieuw neuro-symbolisch raamwerk dat de deterministische theorema-generatie van ∆1 koppelt aan de interpretatieve capaciteiten van LLM's.
2. Theoretische en Empirische Validatie: Bewijs dat ∆1 + LLM zowel formele geldigheid als menselijke begrijpelijkheid levert in hoog-risico domeinen (gezondheidszorg, compliance, regelgeving).
3. Explainability by Construction: Een paradigmaverschuiving waar logische afleidingen inherent transparante, auditabele natuurlijke taalverklaringen produceren, zonder afhankelijkheid van stochastische zoekprocessen.
4. Nieuwe Benchmark: Het creëren van een reproduceerbare dataset van "waarheidsgetrouwe" tegenstrijdigheden die dient als referentiepunt voor de evaluatie van neuro-symbolische systemen.

4. Resultaten en Case Studies

De auteurs testen het systeem in diverse domeinen, waarbij het succesvol minimale tegenstrijdigheden identificeert en deze omzet in actiepunten:

• Gezondheidszorg (Medische Redenering):
  • Scenario: Regels over infecties, witte bloedcellen, koorts en antibiotica.
  • Resultaat: ∆1 identificeerde dat de combinatie van alle regels logisch onmogelijk is. De LLM legde uit dat "antibiotica vereist" in conflict staat met de causale keten zonder extra voorwaarden.
  • Oplossing: De LLM stelde voor om criteria voor antibiotica-voorschrijven te verfijnen (bijv. bevestigingstests).
• Compliance en Regelgeving:
  • Scenario: Conflict tussen privacy (GDPR) en transparantie, of tussen verschillende jurisdicties (GDPR vs. HIPAA).
  • Resultaat: Het systeem identificeerde "DataPortability" als de minimale bron van inconsistentie.
  • Oplossing: Voorstellen om bewaartermijnen aan te passen of uitzonderingen te maken.
• Contractbeheer:
  • Scenario: Inconsistenties in leveringsvoorwaarden, exclusiviteit en boeteclausules.
  • Resultaat: Het onthulde dat "ontbinding zonder oorzaak" logisch onverenigbaar is met "exclusiviteit" en "boetes".
  • Oplossing: Voorstellen om ontbindingsrechten te beperken tot gegronde oorzaken.

In alle gevallen leverde het systeem auditabele, logisch onderbouwde en klinisch/juridisch bruikbare inzichten.

5. Betekenis en Impact

• Vertrouwen in AI: Het systeem lost het "black box"-probleem op door elke verklaring te koppelen aan een formeel, verifieerbaar bewijs. Dit is cruciaal voor toepassingen waar fouten hoge kosten hebben (medische diagnoses, juridische compliance).
• Van Bewijzen naar Begrijpen: Het artikel markeert een transitie van geautomatiseerd theorema-bewijzen naar geautomatiseerd theorema-verstaan. Het maakt complexe logische structuren toegankelijk voor menselijke experts.
• Reproduceerbaarheid: Omdat ∆1 deterministisch werkt, zijn alle resultaten volledig reproduceerbaar, wat essentieel is voor wetenschappelijke validatie en regelgeving.
• Toekomstperspectief: Het werk opent de deur voor zelfreflecterende AI-agenten die kunnen genereren, bewijzen en verklaren, en biedt een basis voor het trainen van andere systemen in logisch redeneren via gestructureerde tegenstrijdigheden.

Kortom, ∆1 + LLM biedt een principieel fundament voor verifieerbare en mensgerichte neuro-symbolische AI, waarbij de strengheid van formele logica wordt gecombineerd met de intuïtie van natuurlijke taal.