Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Dit paper introduceert Elenchus, een dialoagsysteem dat kennisbases construeert door een expert in gesprek te laten treden met een LLM om inferentiële relaties te expliciteren, waarbij de resulterende dialectische staten worden gemapt naar een formeel logisch kader dat de ontwerprationalen van de W3C PROV-O-ontologie valideert.

De kern

Hier is een uitleg van het paper over Elenchus, vertaald naar eenvoudig Nederlands met behulp van creatieve analogieën.

Wat is Elenchus? (De "Socratische AI")

Stel je voor dat je een expert bent, bijvoorbeeld een meester-bakker. Je hebt jarenlang brood gebakken en weet precies hoe het moet. Maar als iemand je vraagt: "Hoe maak je precies dat perfecte brood?", dan is het lastig om dat in een strak recept te zetten. Je denkt misschien: "Nou, je doet meel, water, gist... en dan wacht je." Maar wat als je vergeet te zeggen dat je de temperatuur van het water moet controleren?

Traditionele methoden voor kennis verzamelen proberen die expert gewoon te "ontnemen" (extractie). Ze denken: "De expert heeft het recept al in zijn hoofd, we moeten het er maar uithalen."

Elenchus doet het anders. Het gaat uit van het idee dat kennis niet zomaar in je hoofd ligt, maar ontstaat door het gesprek zelf. Het is als een spelletje "Vraag en Antwoord" met een slimme AI.

Hoe werkt het? (De Bakker en de Kritische Keurmeester)

In dit systeem zijn er twee spelers:

1. De Expert (Jij): Je bent de "Prover" (de bewijzer). Je stelt dingen op als waar (bijv. "Brood moet in een oven").
2. De AI (De Skepticus): Dit is de "Skepticus". De AI is niet hier om je te verslaan, maar om te kijken of je verhaal klopt.

Het spelverloop:

• Jij zegt: "Brood moet in een oven."
• De AI denkt na en zegt: "Wacht even. Als je zegt dat brood in een oven moet, maar ook dat het koud moet zijn, heb je een probleem. Dat kan niet samen."
• De AI noemt dit een spanning (een tegenstrijdigheid).
• Jij moet nu reageren. Je kunt drie dingen doen:
  1. Terugtrekken: "Ah, ja, je hebt gelijk, ik bedoelde dat het warm moet zijn."
  2. Verfijnen: "Nee, ik bedoel dat het koud moet zijn voordat het de oven in gaat."
  3. Aanvechten: "Nee, dat klopt niet, in mijn wereld kan brood koud zijn en toch in de oven."

Als je het met de AI eens bent, wordt die tegenstrijdigheid opgelost en wordt het een vaststaande regel in jullie gezamenlijke "receptenboek". Als je het oneens bent, blijft het een discussiepunt.

Waarom is dit slim? (De AI als "Proefpersoon", niet als "God")

Normaal gesproken hebben we angst voor AI: "Zegt de AI wel de waarheid? Maakt hij geen fouten?"

Bij Elenchus is de AI niet de autoriteit. De AI is als een proefpersoon die suggesties doet.

• De AI zegt: "Misschien is dit een probleem?"
• Jij (de mens) bent de baas. Jij beslist of het echt een probleem is.
• Als de AI een fout maakt en een valse spanning suggereert, zeg jij gewoon: "Nee, dat klopt niet." De fout wordt dan genegeerd.
• Als de AI een echte fout in jouw redenering vindt die jij zelf niet zag, help jij die op te lossen.

Dit noemen ze een "defeasible derivability oracle". Dat is een moeilijke term voor: "Een slimme gids die suggesties doet, maar die jij altijd kunt afwijzen als ze niet kloppen."

Het Resultaat: Een "Levend" Recept

Aan het einde van het gesprek heb je geen gewoon lijstje met feiten. Je hebt een Material Base (een materiële basis).

Stel je voor dat je een gewoon recept hebt: "Doe bloem en water bij elkaar."
Een Elenchus-recept ziet er zo uit: "Als je bloem en water doet, moet je ook gist toevoegen, anders wordt het geen brood. Maar als je het koud hebt, mag je de gist weglaten."

Het systeem houdt niet alleen bij wat waar is, maar ook waarom het waar is en wat er gebeurt als je iets verandert. Het legt de verborgen regels bloot die experts normaal gesproken niet uitspreken, maar wel gebruiken.

De Proef: Het PROV-O Ontologie-project

In het paper testen ze dit met een echte expert die werkt aan een wereldwijd standaard voor "provenance" (waar komt data vandaan?).

• Ze gaven de AI alleen een korte tekst van 350 woorden.
• De AI en de expert hadden een gesprek.
• Het resultaat was een strakke set regels die precies overeenkwam met de complexe beslissingen die de experts in het verleden hadden genomen (die ze normaal gesproken pas na jaren van vergaderen hadden vastgelegd).

Het bewijst dat je met één gesprek een heel complex systeem kunt bouwen dat logisch klopt, zonder dat je duizenden pagina's hoeft te lezen of te coderen.

Samenvatting in één zin

Elenchus is een systeem waarbij een mens en een AI samen een gesprek voeren om kennis te bouwen; de AI zoekt naar gaten in het verhaal, en de mens vult die gaten, waardoor er aan het einde een logisch perfect "recept" ontstaat dat niet alleen zegt wat waar is, maar ook hoe alles met elkaar samenhangt.

Het is alsof je niet meer probeert een boek uit je hoofd te schrijven, maar samen met een spiegelbeeld een verhaal bedenkt dat perfect klopt.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues" van Bradley P. Allen, weergegeven in het Nederlands.

Probleemstelling

Het paper adresseert het klassieke kennisacquisitieprobleem in de kennisengineering. Traditionele benaderingen gaan ervan uit dat expertkennis een deterministische, interne inhoud is die slechts "onttrokken" (extracted) moet worden uit experts of teksten. Dit leidt echter tot een bottleneck: experts hebben vaak geen formele structuren in hun hoofd die direct getranscribeerd kunnen worden. Bestaande methoden (zoals CommonKADS of OWL-ontologieën) behandelen kennis als representatie van de wereld, waarbij de kennisengineer fungeert als vertaler tussen de expert en een formeel formalisme. Het paper stelt dat dit een verkeerd concept is; kennis is niet vooraf gevormd, maar wordt geconstitueerd door expressie en onderhandeling.

Methodologie: Elenchus en Inferentialisme

De auteur presenteert Elenchus, een dialoogprotocol dat kennisengineering herdefinieert als explicitering (explicitation) in plaats van extractie. De methode is gebaseerd op inferentialistische semantiek (Brandom, Hlobil), waarbij de betekenis van een zin wordt bepaald door zijn inferentierol (wat eruit volgt, wat erin onverenigbaar is) en niet door waarheidswaarden.

Het Protocol:

1. Rolverdeling: Een menselijke expert (de Respondent) voert een bilaterale dialoog met een Large Language Model (LLM) als tegenstander (de Skepticus).
2. Positie: De expert bouwt een "positie" op, bestaande uit een set van toezeggingen (asserties) en ontkenningen.
3. Spanningen (Tensions): De LLM fungeert als een weerlegbare afleidingsorakel (defeasible derivability oracle). Het LLM identificeert potentiële "spanningen" (incoherenties) in de positie van de expert (bijv. twee toezeggingen die onverenigbaar zijn).
4. Oplossing: De expert moet deze spanningen oplossen door:
   • Een toezegging of ontkenning in te trekken (retractie).
   • Een stelling te verfijnen (refinement).
   • De uitdaging van het LLM te betwisten (contestation).
5. Uitvoer: Alleen spanningen die door de expert worden aanvaard, worden opgenomen als materiële implicaties in de kennisbasis. Het LLM is dus geen bron van kennis, maar een instrument om de coherentie van de expertkennis te testen.

Formele Mapping:
De dialoogtoestanden worden gemappt naar materiële bases binnen de NonMonotonic MultiSuccedent (NMMS) logica van Hlobil en Brandom.

• Een materiële basis $B$ bestaat uit een taal $L_B$ en een consequentierelatie $| \sim_B$.
• De relatie $\Gamma | \sim_B \Delta$ geldt als de positie (alle $\Gamma$ bevestigen en alle $\Delta$ ontkennen) incoherent is.
• De mapping voldoet aan de Containment-voorwaarde (het is incoherent om een zin zowel te bevestigen als te ontkennen).
• De basis heeft twee componenten:
  1. I (Inferenties): Materiële implicaties die via de dialoog zijn ontdekt en aanvaard.
  2. Cont (Containment): De structurele regel dat een zin niet tegelijkertijd waar en onwaar kan zijn (een pragmatische norm van de dialoog).

Belangrijkste Bijdragen

1. Elenchus Protocol: Een werkend systeem dat experts helpt om hun impliciete inferentiële relaties expliciet te maken via een gestructureerde dialoog met een LLM, waarbij de menselijke autoriteit de onbetrouwbaarheid van het LLM structureel inperkt.
2. Formele Mapping: Een theoretische en technische mapping van dialoogtoestanden naar NMMS-logica. Dit vult een lacune in het inferentialistische programma door een computationele methode te bieden om materiële bases te produceren uit taalkundige praktijken.
3. End-to-End Implementatie: Een werkende implementatie (gebruikmakend van Claude Code en GitHub voor persistente opslag) die een case study uitvoert op de W3C PROV-O (provenance-ontologie).

Resultaten (Case Study: PROV-O)

De methode werd getest op de tekstuele specificatie van de PROV-O-ontologie (sectie 3.1).

• Proces: Een expert voerde een dialoog met het LLM over 350 woorden tekst. Het LLM stelde 7 uitdagingen (spanningen) die onvolledigheden in de specificatie blootlegden.
• Output: De dialoog resulteerde in een materiële basis met 19 toezeggingen en 9 aanvaarde materiële implicaties.
• Validatie met pyNMMS: Een geautomatiseerde NMMS-redeneraar (pyNMMS) werd gebruikt om de structuur van de gegenereerde basis te verifiëren. De resultaten toonden aan dat de basis de volgende eigenschappen bezit die overeenkomen met de ontwerprichtlijnen van PROV-O:
  • Niet-transitiviteit: De afleiding van "Entity" naar "Expanded Terms" is niet direct geldig, wat de scheiding tussen kern en extensie in PROV-O weerspiegelt.
  • Niet-monotonie: Het toevoegen van extra context (zoals het type keten) kan een eerdere afleiding weerleggen, wat overeenkomt met de evolutie van "scruffy" naar "proper" provenance.
  • Onafhankelijkheid: De drie perspectieven van PROV (Data-flow, Process-flow, Responsibility) zijn inferentieel onafhankelijk; er is geen "lek" van inferenties tussen deze domeinen.
  • Retractie: Een eerder ingetrokken toezegging liet geen sporen na in de inferentiële structuur, wat de zuiverheid van de basis bevestigt.

De structuur van de gegenereerde basis correspondeerde nauwkeurig met design-rationales die eerder door Moreau et al. (2015) waren afgeleid uit duizenden e-mails en vergaderingen, maar nu direct uit één dialoogsessie werden gegenereerd.

Significantie en Conclusie

Het paper biedt een paradigmaverschuiving in kennisengineering:

• Van Extractie naar Constitutie: Kennis wordt niet opgehaald, maar gevormd door het proces van dialoog en verdediging van posities.
• Rol van LLMs: In plaats van als een bron van hallucinaties te worden gezien, fungeert het LLM als een "Socratische" tegenpartij. De menselijke expert behoudt de epistemische autoriteit; fouten van het LLM (valse spanningen) worden gefilterd door betwisting, waardoor de kosten van hallucinatie beperkt blijven tot een verloren dialoogbeurt in plaats van een corrupte kennisbasis.
• Formele Garantie: Het systeem produceert niet zomaar een lijst van feiten, maar een materiële basis met bewezen logische eigenschappen (supraclassicaliteit, conservativiteit, explicitering). Dit maakt kennisengineering meetbaar en verifieerbaar via formele logica.

De studie toont aan dat inferentialistische principes, gecombineerd met moderne LLM-technologie, een robuust kader kunnen bieden voor het bouwen van complexe, goed onderbouwde kennisbasissen die de nuances van menselijke expertise behouden zonder ze te vereenvoudigen tot starre formele regels.