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

Die Arbeit stellt Delta1 vor, ein neuro-symbolisches Framework, das einen deterministischen, polynomialen Theoremgenerator mit Large Language Models kombiniert, um in Bereichen wie Gesundheitswesen und Compliance durch konstruktive Beweise glaubwürdige und vollständig erklärbare Schlussfolgerungen zu ermöglichen.

Das Wesentliche

Stellen Sie sich vor, Sie haben zwei sehr unterschiedliche Experten, die zusammenarbeiten müssen, um ein riesiges, verwirrendes Puzzle zu lösen.

Der eine Experte ist ein supergenauer Mathematiker (nennen wir ihn „Delta-1").
Er liebt Regeln, Logik und absolute Sicherheit. Er kann beweisen, dass etwas wahr oder falsch ist, ohne auch nur einen einzigen Fehler zu machen. Aber er ist wie ein Roboter: Er spricht nur in strengen Formeln und kann dem normalen Menschen nicht erklären, warum das Ergebnis so ist. Er sagt nur: „Falsch. Ende."

Der andere Experte ist ein sehr eloquenter Übersetzer (ein „Großes Sprachmodell" oder LLM).
Er kann fließend Deutsch, Englisch und alle anderen Sprachen sprechen. Er kann komplexe Ideen in einfache, verständliche Geschichten verwandeln. Aber er ist manchmal etwas träumerisch und macht gelegentlich Fehler in der harten Logik. Er könnte sagen: „Vielleicht ist es falsch, weil es sich so anfühlt", was für einen Mathematiker kein Beweis ist.

Das Problem:
In der echten Welt (z. B. in Krankenhäusern, bei Gesetzen oder Verträgen) brauchen wir beides: Die absolute Sicherheit des Mathematikers und die verständliche Erklärung des Übersetzers. Wenn ein Computer sagt „Dieser Vertrag ist ungültig", wollen wir nicht nur ein rotes Kreuz sehen, sondern eine klare Erklärung: „Warum? Weil Klausel A gegen Klausel B verstößt."

Die Lösung: Das Team „Delta-1 + LLM"
Diese Forschung stellt ein neues Team vor, das diese beiden Experten vereint. Hier ist, wie es funktioniert, mit ein paar einfachen Bildern:

1. Der „Logik-Maschinenbau" (Delta-1)

Stellen Sie sich Delta-1 als einen perfekten Architekt vor, der ein Haus baut.

• Die Aufgabe: Er nimmt eine Liste von Regeln (z. B. „Wenn es regnet, bleibt das Dach trocken" und „Wenn das Dach nass ist, ist es nicht trocken").
• Die Magie: Anstatt raten zu müssen oder durch tausende Möglichkeiten zu suchen (wie ein Detektiv, der alle Spuren verfolgt), nutzt Delta-1 eine spezielle Bauanleitung (die „vollständige dreieckige Standardwiderspruch"-Methode).
• Das Ergebnis: Er baut sofort ein Modell, das garantiert zusammenbricht, wenn die Regeln falsch sind. Er findet den kleinstmöglichen Fehler. Er sagt nicht nur „Es gibt einen Fehler", sondern zeigt genau: „Wenn wir diesen einen kleinen Stein (eine Regel) entfernen, steht das Haus wieder."
• Der Vorteil: Es ist zu 100 % bewiesen. Keine Zufälle, keine „Vielleicht".

2. Der „Geschichtenerzähler" (Das LLM)

Jetzt kommt der Übersetzer ins Spiel.

• Die Aufgabe: Der Architekt (Delta-1) reicht ihm den blauen Plan des zusammengebrochenen Hauses und sagt: „Hier ist der Stein, der alles zum Einsturz gebracht hat."
• Die Magie: Der Übersetzer nimmt diesen trockenen technischen Plan und schreibt daraus eine klare Geschichte für den Hausbesitzer.
• Das Ergebnis: Statt „Klausel 4 widerspricht Klausel 1" sagt er: „Achtung! Sie haben versprochen, das Haus nur bei Regen zu streichen, aber gleichzeitig gesagt, dass es bei Sonnenschein gestrichen werden muss. Das geht nicht. Wenn Sie die Regel für den Regen ändern, funktioniert alles."

Ein konkretes Beispiel aus dem Papier: Das Krankenhaus

Stellen Sie sich vor, ein Arzt hat eine Liste von Regeln für die Behandlung von Patienten:

1. Wenn der Patient eine Infektion hat, ist das Blutbild hoch.
2. Wenn das Blutbild hoch ist, hat der Patient Fieber.
3. Wenn Infektion und Fieber da sind, braucht er Antibiotika.

Was passiert im System?

• Delta-1 nimmt diese Regeln und baut daraus ein logisches Modell. Es stellt fest: „Moment mal! Wenn wir alle diese Regeln gleichzeitig anwenden, ergibt das keinen Sinn. Es gibt einen versteckten Konflikt."
• Es findet heraus, welcher genaue Teil der Regelkette den Konflikt verursacht (z. B. vielleicht die Annahme, dass jeder mit hohem Blutbild sofort Fieber hat, was nicht immer stimmt).
• Das LLM übersetzt das dann für den Arzt: „Herr Doktor, Ihre Regelkette ist zu streng. Sie zwingt uns, jedem Patienten mit hohem Blutbild sofort Antibiotika zu geben, auch wenn er vielleicht gar kein Fieber hat. Das ist gefährlich. Lassen Sie uns die Regel für das Fieber etwas flexibler gestalten."

Warum ist das so wichtig?

Bisherige KI-Systeme waren wie ein Glaskugelschreiber: Sie sagten oft etwas Richtiges, aber man konnte nicht nachvollziehen, wie sie darauf kamen. Oder sie waren wie ein starrer Taschenrechner: Sie waren genau, aber man konnte sie nicht fragen, warum.

Dieses neue System ist wie ein weise alter Lehrer mit einem Computer im Rücken:

1. Der Computer (Delta-1) garantiert, dass die Mathematik stimmt.
2. Der Lehrer (LLM) erklärt es so, dass ein Mensch es versteht und weiß, was er tun muss.

Zusammenfassung in einem Satz:
Dieses Papier beschreibt ein System, das logische Fehler nicht nur findet (wie ein strenger Richter), sondern auch erklärt, wie man sie behebt (wie ein verständnisvoller Berater), und das alles auf einer Basis, die zu 100 % beweisbar ist. Es verbindet die Härte der Mathematik mit der Weichheit der menschlichen Sprache.

Technische Zusammenfassung

1. Problemstellung

Die aktuelle Forschung im Bereich des neuro-symbolischen Denkens (Neuro-Symbolic Reasoning) steht vor einem fundamentalen Dilemma:

• Symbolische Ansätze (z. B. automatische Theorembeweiser) bieten formale Korrektheit (Soundness), transparente Inferenzstrukturen und mathematische Beweise, leiden aber oft unter mangelnder sprachlicher Ausdrucksfähigkeit und sind für Menschen schwer interpretierbar.
• Neuronale Modelle (Large Language Models, LLMs) zeichnen sich durch hohe sprachliche Flüssigkeit und Anpassungsfähigkeit aus, liefern jedoch keine Garantien für logische Richtigkeit und ihre Schlussfolgerungen sind oft stochastisch und nicht verifizierbar.

Bisherige hybride Systeme versuchen, diese Lücke zu schließen, scheitern jedoch oft daran, sowohl formale Garantien als auch menschliche Interpretierbarkeit gleichzeitig zu bieten. Es fehlt an einem Framework, das logische Validität und natürliche Spracherklärung durch Konstruktion (by design) vereint.

2. Methodik: Das ∆1 + LLM Framework

Das Papier stellt einen End-to-End-Pipeline vor, die einen deterministischen Theoremgenerator (∆1) mit einem LLM zur semantischen Interpretation koppelt.

A. Der ∆1-Theoremgenerator (Symbolischer Kern)

• Grundlage: ∆1 basiert auf dem Konzept der Full Triangular Standard Contradiction (FTSC).
• Funktionsweise:
  • Aus einer Menge von $n$ atomaren Prädikaten (ohne komplementäre Paare) konstruiert ∆1 deterministisch eine Klauselmenge $S$, die eine FTSC bildet.
  • Die FTSC besteht aus einer Kette von Klauseln ($D_1$ bis $D_{n+1}$), die logisch widersprüchlich sind.
  • Theorembildung: Für jede Klausel $C \in S$ generiert ∆1 ein Theorem der Form $S \setminus \{C\} \vdash \neg C$. Das bedeutet: Wenn man eine Klausel entfernt, wird die Menge erfüllbar, aber die entfernte Klausel wird durch die verbleibenden Klauseln widerlegt.
  • Eigenschaften:
    • Deterministisch: Kein Suchprozess, kein Backtracking, keine Zufälligkeit.
    • Minimale Unerfüllbarkeit (MUS): Jede generierte Klauselmenge ist eine minimal unerfüllbare Teilmenge (MUS) per Konstruktion.
    • Komplexität: Die Generierung einer einzelnen FTSC erfolgt in $O(n^3)$ Zeit. Die vollständige Enumeration aller Permutationen führt zu $n!$ nicht-äquivalenten Theoremen, ist aber vollständig und redundantfrei.
    • Beweispfad: Da die Abhängigkeitskette bekannt ist, liefert ∆1 explizite Beweispfade ohne externe SAT-Löser.

B. Die LLM-Schicht (Neuronale Interpretation)

• Vorverarbeitung: Ein Frontend-LLM extrahiert atomare Prädikate und logische Formen aus natürlichen Spracheingaben (z. B. medizinischen Richtlinien oder Verträgen) und wandelt sie in TPTP-Syntax um.
• Nachverarbeitung: Ein Backend-LLM nimmt die von ∆1 generierten Theoreme und Beweispfade entgegen.
  • Es übersetzt die formalen logischen Strukturen in kohärente, natürliche Sprache.
  • Es bewertet die Relevanz (Salience) der Theoreme.
  • Es formuliert konkrete Handlungsempfehlungen (Remediation) zur Behebung der identifizierten Widersprüche.

C. Architektur des Pipelines

1. Prädikat-Extraktion: Natürliche Sprache $\rightarrow$ Logische Prädikate.
2. Deterministische Theoremgenerierung: ∆1 konstruiert alle minimalen unerfüllbaren Klauselmengen und Theoreme.
3. Beweispfad-Konstruktion: ∆1 erstellt explizite Ableitungssequenzen.
4. Erklärung und Ranking: LLM verbalisiert die Beweise und priorisiert sie basierend auf Kontext.

3. Hauptbeiträge

1. Neuro-symbolische Integrationspipeline: Eine neue Architektur, die die deterministische Theoremgenerierung von ∆1 mit der interpretativen Kraft von LLMs verbindet.
2. Erklärbarkeit durch Konstruktion (Explainability-by-Construction): Im Gegensatz zu post-hoc-Erklärungen wird die Interpretierbarkeit hier inhärent in den Generierungsprozess integriert. Jeder Schritt ist logisch verifizierbar und sprachlich erklärbar.
3. Theoretische und empirische Validierung: Der Nachweis, dass das System sowohl formale Soundness (durch ∆1) als auch menschliche Interpretierbarkeit (durch LLM) in hochriskanten Domänen liefert.
4. Erste formal garantierte Entdeckungsmaschine: Das System ist laut Autoren der erste Ansatz, der symbolische und natürliche Sprachlogik verbindet und dabei formale Garantien für die Korrektheit der abgeleiteten Theoreme bietet.

4. Ergebnisse und Fallstudien

Das Framework wurde in mehreren Domänen getestet, um seine Fähigkeit zur Aufdeckung und Erklärung von Widersprüchen zu demonstrieren:

• Medizinische Diagnostik:
  • Szenario: Regeln zu Infektionen, Leukozyten, Fieber und Antibiotika.
  • Ergebnis: ∆1 identifizierte minimale Widersprüche (z. B. dass eine automatische Antibiotika-Verschreibung unter bestimmten Bedingungen logisch inkonsistent ist). Das LLM erklärte dies als „Überverpflichtung" und schlug vor, Kriterien für die Verschreibung zu präzisieren.
• Compliance und Regulierung:
  • Szenario: Konflikte zwischen Datenschutz (GDPR) und Offenlegungspflichten (HIPAA) oder zwischen Transparenz und Privatsphäre.
  • Ergebnis: Das System isolierte spezifische Klauseln (z. B. „Datenportabilität") als minimale Inkonsistenzquellen und lieferte sprachliche Begründungen, warum diese unter den aktuellen Regeln nicht erfüllbar sind.
• Vertragsanalyse:
  • Szenario: Inkonsistenzen in Lieferverträgen (z. B. Exklusivität vs. fristlose Kündigung).
  • Ergebnis: Das System deckte auf, dass bestimmte Kombinationen von Klauseln (Exklusivität + Strafen + Kündigung ohne Grund) logisch unmöglich sind, und schlug spezifische Vertragsänderungen vor, um die Erfüllbarkeit wiederherzustellen.
• Erweiterung auf Prädikatenlogik (First-Order Logic):
  • Die Methode wurde erfolgreich auf Szenarien mit Variablen und Relationen (z. B. Patientendaten, Bankenregulierung) angewendet, wobei die logische Struktur erhalten blieb.

In allen Fällen konnte das System nicht nur Fehler finden, sondern auch zielgerichtete Abhilfemaßnahmen (Remediation) vorschlagen, die die logische Konsistenz wiederherstellen.

5. Bedeutung und Ausblick

• Paradigmenwechsel: Das Papier markiert einen Übergang von der „automatischen Theorembeweisung" (Proof) zur „automatischen Theorem-Verstehung" (Understanding).
• Vertrauenswürdige KI: Durch die Kombination von formaler Verifizierbarkeit und menschlicher Lesbarkeit bietet das Framework eine Grundlage für vertrauenswürdige, auditierbare KI-Systeme in kritischen Bereichen wie Gesundheitswesen, Recht und Finanzen.
• Benchmarking: Die generierten Theoreme dienen als „Ground Truth" für die Bewertung von Neuro-Symbolic-Systemen und als Datensatz für das Training von Beweisführern.
• Zukünftige Richtungen: Die Autoren planen Optimierungen zur Reduzierung der faktoriellen Komplexität (Symmetrie-Breaking), die Integration in kontinuierliche Vektorräume für Ähnlichkeitssuchen und die Erweiterung auf Multi-Agenten-Systeme.

Fazit: ∆1 + LLM stellt einen bedeutenden Fortschritt dar, da es die Lücke zwischen der Starrheit formaler Logik und der Flexibilität natürlicher Sprache schließt, ohne dabei die mathematische Korrektheit zu opfern. Es ermöglicht eine „erklärbar durch Konstruktion" (explainability-by-construction) Philosophie, bei der Transparenz und Auditierbarkeit inhärente Eigenschaften des Systems sind.