Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Das Paper stellt Elenchus vor, ein dialogbasiertes System, das mithilfe von Inferentialismus und der NMMS-Logik Wissensbasen durch die strukturierte Auflösung von Spannungen zwischen einem Experten und einem LLM-gestützten Skeptiker konstruiert und dabei die Inferenzbeziehungen formal verifiziert.

Das Wesentliche

Elenchus: Wie man Wissen nicht abfängt, sondern gemeinsam baut

Stell dir vor, du versuchst, das Wissen eines Experten (z. B. eines Ontologen oder Ingenieurs) in einen Computer zu bekommen.

Das alte Problem:
Bisher dachte man, das Wissen eines Experten sei wie ein fertiger Schatz in einer Höhle. Der Computer (oder ein Wissensingenieur) muss nur die Höhle betreten, den Schatz finden und ihn in eine Kiste (eine Datenbank) packen. Das Problem ist: Experten haben diesen „fertigen Schatz" oft gar nicht im Kopf. Ihr Wissen ist eher wie ein fließender Fluss – es entsteht erst, wenn sie darüber sprechen, diskutieren und sich gegenseitig Fragen stellen. Wenn man versucht, diesen Fluss einfach in eine Kiste zu schütten, bleibt er stecken oder verdirbt.

Die neue Lösung: Elenchus
Das Papier stellt „Elenchus" vor. Das ist kein Werkzeug zum „Ausschöpfen" von Wissen, sondern ein Werkzeug zum „Klären" von Wissen.

Stell dir Elenchus wie ein Dialog zwischen zwei Figuren vor:

1. Der Experte (der Prover): Er hat eine Meinung oder eine Idee.
2. Die KI (der Skeptiker): Sie ist nicht da, um zu behaupten, sie wüsste alles. Sie ist wie ein neugieriger, manchmal etwas störrischer Sparringspartner.

Wie funktioniert das Spiel?

Stell dir vor, du baust ein Haus (das ist dein Wissen).

• Der Experte sagt: „Hier ist eine Wand."
• Die KI fragt: „Warte, wenn du hier eine Wand baust und dort ein Fenster, passt das zusammen? Oder stößt die Wand gegen das Fenster?" (Die KI sucht nach Spannungen oder Widersprüchen).

Jetzt passiert das Magische:

• Wenn der Experte merkt: „Oh, du hast recht, das passt nicht," zieht er die Wand zurück oder baut sie anders.
• Wenn der Experte sagt: „Nein, das passt doch, hier ist eine spezielle Tür," dann wird diese Regel festgehalten.

Die KI schlägt also nur mögliche Probleme vor. Der Experte entscheidet, ob sie wirklich Probleme sind. Die KI ist wie ein Wettervorhersage-System: Sie sagt „Es könnte regnen", aber der Experte muss entscheiden, ob er einen Regenschirm nimmt oder nicht. Wenn die KI sich irrt (eine falsche Warnung ausspricht), macht der Experte einfach „Nein" und das Spiel geht weiter. Die KI verdirbt also nichts, sie hilft nur, Schwachstellen zu finden.

Das Ergebnis: Ein lebendiges Regelwerk

Am Ende des Gesprächs haben sie nicht einfach eine Liste von Fakten. Sie haben ein Regelwerk erstellt, das zeigt:

• „Wenn A gilt, dann darf B nicht gelten."
• „Wenn C passiert, dann ist D möglich, aber nur, wenn E nicht da ist."

Das ist besonders wichtig, weil echtes Wissen oft nicht starr ist. In der klassischen Logik gilt: Wenn A wahr ist, ist B immer wahr. Aber in der echten Welt (und bei Expertenwissen) gilt das oft nicht.

• Beispiel: „Wenn es regnet, wird die Straße nass." (Das ist meist wahr).
• Aber: „Wenn es regnet UND jemand hat eine Plane über die Straße gespannt, ist die Straße trocken."

Elenchus schafft ein System, das diese Ausnahmen und Bedingungen genau so speichert, wie ein Experte sie denkt. Es ist wie ein Garten, in dem man nicht nur Pflanzen (Fakten) pflanzt, sondern auch die Regeln für das Gießen und Beschneiden (die Logik) festlegt.

Der Fallbeispiel: Die PROV-O-Regeln

Um zu beweisen, dass das funktioniert, haben die Autoren das System mit einem echten Standard für „Datenherkunft" (PROV-O) getestet. Das ist wie ein riesiges Regelbuch für die Dokumentation von Daten.

Sie gaben dem System nur einen kurzen Text (350 Wörter) und ließen den Experten mit der KI diskutieren.

• Das Ergebnis: Das System fand genau die gleichen „Schwierigkeiten" und „Entscheidungen", die die ursprünglichen Entwickler des Standards Jahre zuvor in tausenden E-Mails diskutiert hatten.
• Der Beweis: Das System hat nicht nur Fakten gesammelt, sondern die tiefen logischen Strukturen verstanden. Es hat gezeigt, dass bestimmte Regeln nicht einfach aufeinander aufbauen (nicht-transitiv), sondern dass man vorsichtig sein muss, wenn man neue Informationen hinzufügt (nicht-monoton).

Warum ist das revolutionär?

Früher dachte man: „Der Experte hat das Wissen, wir müssen es nur abschreiben."
Elenchus sagt: „Das Wissen entsteht erst im Gespräch."

• Die KI ist der Spiegel, der zeigt, wo die Gedanken des Experten hängen bleiben oder widersprüchlich sind.
• Der Experte ist der Architekt, der entscheidet, wie das Gebäude am Ende aussieht.
• Das Ergebnis ist keine statische Datenbank, sondern ein nachvollziehbarer Dialog, bei dem jede Regel auf einen bestimmten Moment im Gespräch zurückgeführt werden kann.

Zusammenfassend:
Elenchus ist wie ein intelligentes Gespräch, das am Ende nicht nur eine Zusammenfassung liefert, sondern ein funktionierendes, logisches Regelwerk baut. Es nutzt die KI nicht als allwissenden Gott, sondern als einen klugen, manchmal kritischen Gesprächspartner, der uns hilft, unser eigenes Denken klarer zu machen. Und das Beste: Wenn die KI sich irrt, ist es kein Fehler im System, sondern nur ein Moment im Gespräch, den wir korrigieren können.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues" von Bradley P. Allen auf Deutsch.

1. Problemstellung: Das Wissensakquisitions-Problem

Das Paper adressiert das seit Jahrzehnten bestehende „Wissensakquisitions-Problem" in der Wissensengineering-Disziplin. Traditionelle Ansätze gehen von einem repräsentationalistischen Verständnis aus: Es wird angenommen, dass Experten formales Wissen bereits in ihrem Kopf besitzen und dieses lediglich extrahiert und transkribiert werden muss. Dies führt jedoch zu einem Engpass, da Expertenwissen oft nicht als fertige, formale Struktur vorliegt, sondern durch Praxis und Ausdruck konstituiert wird.

Das Ziel ist es, eine Methode zu entwickeln, die Wissen nicht als „Extraktion" aus Experten oder Texten behandelt, sondern als Explikation (Explicitation) durch Dialog. Dabei soll das inferentielle Verhältnis zwischen Aussagen (was folgt woraus, was ist unvereinbar) in den Vordergrund gestellt werden, anstatt nur den Wahrheitsgehalt von Aussagen zu erfassen.

2. Methodik: Das Elenchus-Protokoll

Die vorgestellte Lösung ist Elenchus, ein bilaterales dialektisches Protokoll, das auf der inferentialistischen Semantik (basierend auf den Arbeiten von Robert Brandom und Ulf Hlobil) aufbaut.

• Akteure:

  • Der Respondent (Experte): Ein menschlicher Fachexperte, der eine Position (eine Menge von Verpflichtungen/Behauptungen und Ablehnungen) zu einem Thema entwickelt.
  • Der Opponent (LLM): Ein Large Language Model, das als „defeasible derivability oracle" (widerlegbares Ableitungs-Orakel) fungiert. Seine Aufgabe ist es nicht, Wissen zu generieren, sondern Spannungen (Tensions) im Gedankengebäude des Experten aufzudecken.

• Der Dialogprozess:

  1. Der Experte formuliert eine initiale Position (Commitments und Denials).
  2. Der LLM-Opponent prüft die Kohärenz und schlägt Spannungen (Tensions) vor. Eine Spannung ist ein Sequenz $\Gamma \vdash \Delta$, die besagt, dass die gleichzeitige Behauptung von $\Gamma$ und die Ablehnung von $\Delta$ inkohärent ist.
  3. Der Experte muss diese Spannungen auflösen durch:
     • Rücknahme (Retraction): Eine Behauptung oder Ablehnung wird verworfen.
     • Verfeinerung (Refinement): Die Proposition wird präzisiert, um den Konflikt aufzulösen.
     • Bestreitung (Contestation): Der Experte lehnt die vom LLM behauptete Inkohärenz ab.
  4. Nur akzeptierte Spannungen werden in die finale Wissensbasis aufgenommen.

• Architektur: Das System ist als Claude Code-Agent implementiert, der den Dialogzustand persistent in einem GitHub-Repository speichert (Commitments, Denials, Tensions werden als Issues mit Labels verwaltet). Dies ermöglicht eine vollständige Nachverfolgbarkeit (Traceability) jedes inferentiellen Schritts.

3. Theoretische Grundlagen und Schlüsselbeiträge

Der Hauptbeitrag liegt in der formalen Abbildung des dialektischen Prozesses auf eine logische Struktur:

• Von Dialektischem Zustand zu Materiellem Basis:
  Der Dialogzustand $S = \langle [C:D], T, I \rangle$ (Position, offene Spannungen, akzeptierte materielle Implikationen) wird auf eine Materielle Basis (Material Base) $B = \langle L_B, \vdash_B \rangle$ in der NonMonotonic MultiSuccedent (NMMS) Logik (Hlobil & Brandom 2025) abgebildet.

  • Die Basis besteht aus einer atomaren Sprache und einer Konsequenzrelation.
  • Die Relation $\Gamma \vdash_B \Delta$ gilt, wenn die Position, $\Gamma$ zu behaupten und $\Delta$ zu verneinen, inkohärent ist.
  • Containment-Eigenschaft: Die Basis erfüllt die Bedingung, dass das Behaupten und Verneinen desselben Satzes immer inkohärent ist. Dies wird durch die Vereinigung von zwei Komponenten erreicht:
    1. $I$: Materielle Implikationen, die durch den Dialog entdeckt wurden (substantive Inkohärenzen).
    2. $Cont$: Strukturelle Inkohärenzen (Behaupten und Verneinen desselben Satzes), die als pragmatische Norm des Dialogs vorausgesetzt werden.

• Explikation durch logische Vokabeln:
  Ein weiterer Beitrag ist die Nutzung des NMMS-Kalküls, um aus der materiellen Basis eine logische Vokabel (Konnektoren wie $\to, \land, \lor, \neg$) zu entwickeln. Dies ermöglicht es, die im Dialog verhandelten materiellen Inferenzbeziehungen explizit zu machen, ohne die substrukturellen Eigenschaften (Nicht-Monotonie, Nicht-Transitivität) der Basis zu zerstören.

• Rolle des LLM:
  Das Paper redefiniert die Rolle des LLM: Es ist keine Wissensquelle (die Halluzinationen produziert), sondern ein dialektischer Partner. Fehlerhafte Spannungen (False Positives) werden durch den Experten herausgefordert und verworfen. Die Autorität liegt beim Menschen; der LLM dient nur als Katalysator zur Aufdeckung impliziter Inkonsistenzen.

4. Ergebnisse: Fallstudie mit PROV-O

Die Methode wurde an der W3C PROV-O Ontologie (Provenance) getestet. Ein Experte führte einen Dialog über den Abschnitt 3.1 der Spezifikation (350 Wörter Text).

• Prozess: Ausgehend von 10 initialen Commitments generierte der LLM 7 Herausforderungen (Challenges), die Underspezifikationen in der Spezifikation aufdeckten.
• Ergebnis: Der Dialog führte zu einer finalen materiellen Basis mit 19 Commitments und 9 akzeptierten materiellen Implikationen.
• Validierung mit pyNMMS:
  • Die Autoren verwendeten den automatisierten Reasoner pyNMMS, um die strukturellen Eigenschaften der generierten Basis zu verifizieren.
  • Nicht-Transitivität: Die Inferenzkette wurde korrekt als nicht-transitiv erkannt (z.B. folgt aus $p2$ nicht automatisch $p23$, obwohl $p2 \to p18$ und $p18 \to p23$ gelten). Dies entspricht dem Design-Entscheid, dass das Kern-Modell von PROV nicht automatisch Erweiterungen impliziert.
  • Nicht-Monotonie: Das Hinzufügen neuer Informationen (z.B. Kontextdetails) kann frühere Inferenzen widerlegen. Dies spiegelt den Übergang von „scruffy" (einfach) zu „proper" (qualifiziert) Provenance wider.
  • Unabhängigkeit: Die Inferenzketten der verschiedenen Design-Entscheidungen (z.B. zwischen Entity, Activity und Agent) blieben voneinander unabhängig, was die Modularität der Ontologie bestätigt.
  • Korrespondenz: Die strukturellen Eigenschaften der generierten Basis stimmten exakt mit den Design-Rationale überein, die in einer retrospektiven Analyse von Moreau et al. (basierend auf 8820 E-Mails und 152 Telefonkonferenzen) dokumentiert wurden.

5. Bedeutung und Fazit

Das Paper demonstriert einen Paradigmenwechsel im Wissensengineering:

1. Von Extraktion zu Explikation: Wissen wird nicht aus dem Kopf des Experten „gelesen", sondern durch dialektische Auseinandersetzung explizit gemacht.
2. Formale Verifizierbarkeit: Das Ergebnis ist keine bloße Sammlung von Aussagen, sondern eine formal verifizierbare materielle Basis mit nachweisbaren logischen Eigenschaften (Substruktur, Nicht-Monotonie).
3. Robustheit gegenüber LLM-Fehlern: Durch die menschliche Kontrolle über die Akzeptanz von Spannungen wird das Problem der LLM-Halluzinationen strukturell gelöst. Fehlerhafte Vorschläge werden herausgefiltert, ohne die Integrität der Wissensbasis zu gefährden.
4. End-to-End-Integration: Es wird ein vollständiger Workflow von natürlichem Sprachdialog über die Konstruktion einer materiellen Basis bis hin zur formalen logischen Inferenz demonstriert.

Zusammenfassend bietet Elenchus einen neuen, inferentialistischen Ansatz, um komplexe, expertenbasierte Wissensstrukturen zu formalisieren, die die Nuancen und Unsicherheiten realer Domänen (wie Nicht-Transitivität und Kontextabhängigkeit) besser abbilden als klassische, monotonische Ontologien.