Der Algorithmus: Wie DDIC Konflikte löst

Im letzten Beitrag ging es darum, wie Regeln in den Guard kommen: Formulare statt Freitext, das LLM füllt Felder, eine deterministische Funktion erzeugt die MELD-Syntax. Ich hatte am Ende versprochen, dass es dieses Mal um die Engine selbst geht. Also um die Stelle, an der zwei Regeln sich widersprechen, beide korrekt formuliert, beide aktiv sind, und die Engine trotzdem in Mikrosekunden eine Antwort liefern muss.

Wenn man “deontische Logik” hört, denkt man schnell an universitäre Seminare, an Modaloperatoren, an Beweise auf Tafel. Und dann an Laufzeit, an Millisekunden, die sich zu Sekunden summieren, wenn hundert Agenten gleichzeitig etwas wollen. Aber so schlimm ist es nicht. Der Algorithmus ist ein sortierter Listendurchlauf mit ein paar Paarvergleichen. Es steckt weder ein Theorem-Prover noch ein SAT-Solver wie Z3 dahinter.

Das Szenario

Zurück in unser Krankenhausbeispiel. Die Compliance-Beauftragte hat drei Regeln festgelegt:

1. Pflegekräfte dürfen Patientenakten nicht einsehen.
2. Im Nachtdienst, wenn kein Arzt erreichbar ist, dürfen Pflegekräfte die Patientenakte einsehen.
3. Medizinische Daten werden nie an Externe weitergegeben.

Die dritte Regel ist ein moralisches Axiom, sie steht über allem. Die ersten beiden sind kontextgebunden und in Konflikt. In MELD sieht das dann so aus:

; Regel 1: Allgemeine Hausregel
(forbiddenToDo-WRT KrankenhausCode pflege
    (lesenPatientenakte patientenakte))

; Regel 2: Ausnahme für den Nachtdienst
(permittedToDo-WRT NotfallCode pflege-nachtdienst
    (lesenPatientenakte patientenakte))

; Regel 3: Moralisches Axiom
(forbiddenToDo pflege
    (weitergebenDaten medizinisch extern))

Eine Pflegekraft im Nachtdienst ruft an: sie möchte die Patientenakte einsehen. Der Guard bekommt die Anfrage. Er muss jetzt entscheiden. PERMITTED, FORBIDDEN oder UNDECIDABLE. In dieser Reihenfolge läuft der Algorithmus.

Schritt 1: Wen betrifft die Regel überhaupt?

Bevor ich über Konflikte rede, filtert die Engine die Regeln, die überhaupt anwendbar sind. Eine Regel ist anwendbar, wenn sie den Agenten betrifft und die gefragte Aktion beschreibt. Die Engine fragt also: Welche Regeln sprechen über diese konkrete Anfrage?

applicable = [
    n for n in norms
    if n.matches_agent(agent)
    and self._proposition_matches(n, proposition)
]

matches_agent nutzt die Ontologie. Wenn die Regel für pflege gilt und der Agent pflege-nachtdienst ist, und in der Ontologie steht (genls pflege-nachtdienst pflege), dann passt die Regel. pflege-nachtdienst ist eine Spezialisierung von pflege. Die Vererbung wirkt nach unten.

Für unser Szenario bleiben nach dem Filter zwei Regeln übrig. Regel 1 und Regel 2. Regel 3 spricht über eine andere Aktion (weitergebenDaten) und ist nicht anwendbar.

Unter der Haube arbeitet proposition_matches mit Unifikation, nicht mit Stringvergleich. Eine Regel mit dem Pattern ("lesenPatientenakte",) matcht auch eine Anfrage mit zusätzlichen Parametern. Das ist Prolog-Technik aus den Siebzigern, neu angewandt. Der Filter selbst ist O(n). Bei zehntausend Regeln pro Domäne sind das immer noch Mikrosekunden, weil jede Regel mit einem Dictionary-Lookup und einem Tupelvergleich abgefrühstückt ist.

Schritt 2: Axiome gewinnen immer

Bevor ich irgendetwas anderes prüfe, sortiert die Engine die moralischen Axiome aus. In der NormFrame-Datenstruktur gibt es ein Flag defeasible: bool. True heißt überschreibbar, False heißt Axiom.

axioms = [n for n in applicable if not n.defeasible]
defeasible = [n for n in applicable if n.defeasible]

if axioms:
    # Gibt es widersprüchliche Axiome? Dann UNDECIDABLE.
    if detect_conflicts(axioms):
        return NormStatus(modality=None, reason="contradictory_axioms", ...)
    # Sonst: das Axiom gewinnt, Punkt.
    return NormStatus(modality=axioms[0].modality, reason="moral_axiom", ...)

Die Logik ist einfach. Ein anwendbares Axiom entscheidet, ohne Kontextabhängigkeit. Widersprechen sich zwei Axiome, gibt die Engine UNDECIDABLE zurück, und die Infrastruktur drumherum blockiert die Aktion. Fail-Closed. Ich lebe lieber mit einem False Positive als mit einer Aktion, die nie hätte passieren dürfen. In unserem Szenario gibt es kein Axiom in der Filtermenge. Regel 3 spricht über das Weitergeben von Daten, nicht über das Lesen. Die Engine geht weiter.

Schritt 3: Spezifität als Ordnungsprinzip

Regel 1 und Regel 2 widersprechen sich. Regel 1 verbietet, Regel 2 erlaubt. Beide sind überschreibbar, beide sind aktiv, und ich muss irgendwie entscheiden, welche gewinnt.

DDIC antwortet: die spezifischere. Spezifität ist dabei keine Intuition, sondern eine ganze Zahl. Jede Regel hat ein Feld specificity: int, das beim Einlesen der MELD-Datei aus der Tiefe in der Vererbungshierarchie berechnet wird. pflege hat Tiefe 2, pflege-nachtdienst hat Tiefe 3. Die Regel für pflege-nachtdienst ist spezifischer.

# Sortiere defeasible Normen nach Spezifität, absteigend
applicable_sorted = sorted(
    defeasible,
    key=lambda n: (n.specificity, code_rank, n.code, n.modality.value),
    reverse=True,
)

# Präemption: spezifischere Regel schlägt allgemeinere
for i, a in enumerate(sorted_norms):
    for j, b in enumerate(sorted_norms):
        if j <= i or not a.conflicts_with(b):
            continue
        if a.specificity > b.specificity:
            defeated.add(j)
        elif b.specificity > a.specificity:
            defeated.add(i)
            break

Ein Doppelschleifen-Vergleich. O(n²) im Pathologiefall, in der Praxis selten relevant, weil n (die Zahl der anwendbaren Regeln nach Filter) fast nie über Dutzend liegt. Für jede anwendbare Regel gegen jede andere: gibt es einen Konflikt, und wenn ja, welche ist spezifischer? Die weniger spezifische fliegt raus.

Regel 2 (specificity=3) schlägt Regel 1 (specificity=2). Die Engine antwortet PERMITTED.

Der Sortierschlüssel ist übrigens ein Tupel: (specificity, code_rank, code, modality_value). Die hinteren Felder sind Tiebreaker und garantieren Determinismus auch bei Gleichständen. Die Konfliktprüfung conflicts_with wiederum ist nichts anderes als ein Set-Vergleich der Modalitäten. PERMITTED und FORBIDDEN konfligieren, OBLIGATORY und PERMITTED nicht, weil Pflicht die Erlaubnis impliziert. Der Kern von Olsons Kalkül passt an dieser Stelle in drei Zeilen Python.

Schritt 4: Wenn Spezifität nicht reicht

Was mache ich, wenn zwei Regeln gleich spezifisch sind? Zum Beispiel stammt die eine aus dem KrankenhausCode, die andere aus dem DSGVOCode, beide gelten für arzt, beide betreffen lesenPatientenakte, eine erlaubt, die andere verbietet. Gleiche Tiefe in der Hierarchie, keine Präemption.

Hier greift die Kodex-Präzedenz. Die Engine bekommt beim Start eine Liste code_prevalence: ["DSGVOCode", "KrankenhausCode"]. Frühere Einträge gewinnen gegen spätere. Rechtsgrundlagen stehen über Hausregeln.

def _resolve_by_prevalence(self, norms):
    by_modality = group_by_modality(norms)
    best_modality, best_rank = None, -1
    for modality, mod_norms in by_modality.items():
        for n in mod_norms:
            rank = prevalence_rank(n.code)
            if rank > best_rank:
                best_rank, best_modality = rank, modality
    # Prüfen, ob der Rang eindeutig ist
    if tie_exists(best_rank, by_modality):
        return None  # UNDECIDABLE
    return by_modality[best_modality]

Wenn die Präzedenz klar ist, gewinnt der höhere Kodex. Wenn zwei Regeln aus demselben Kodex stammen und immer noch widersprüchlich sind, oder wenn zwei Kodizes gleichrangig sind, bleibt nur ein Weg.

Schritt 5: UNDECIDABLE, nicht “irgendwas”

return NormStatus(
    modality=None,
    reason="unresolved_conflict",
    justification_chain=tuple(chain),
)

modality=None. Die Engine sagt nicht “ich vermute FORBIDDEN”. Sie sagt nicht “ich nehme die erste Regel”. Sie sagt: ich kann es nicht entscheiden. Die umgebende Infrastruktur interpretiert diesen Zustand als Fail-Closed. Die Aktion findet nicht statt. Ein Mensch schaut drauf.

Ich glaube, das ist der Teil, den viele Entwickler unterschätzen, wenn sie Regelwerke bauen. Die meisten Systeme haben einen impliziten Default: wenn unklar, erlauben, oder wenn unklar, verbieten. Beides ist in kritischen Kontexten falsch. Der erste Weg öffnet Lücken, die niemand dokumentiert hat, der zweite produziert Fehlalarme, die niemand mehr ernst nimmt. UNDECIDABLE ist ein dritter Zustand, der explizit sagt: das Regelwerk ist hier unvollständig. Nicht die Engine hat ein Problem, sondern die Spezifikation.

Woher weiß man, dass das alles stimmt?

Ein Algorithmus, der über das Verhalten von KI-Systemen entscheidet, darf nicht “sieht richtig aus” sein, er muss nachweislich korrekt sein. Ich habe echt unterschätzt, wie viel Arbeit dieser Nachweis bedeutet. Nicht die Engine selbst, sondern das Drumherum, das zeigt: sie tut, was sie soll.

AEGIS hat dafür eine vierstufige Nachweiskette. Jede Stufe fängt eine andere Klasse von Fehlern. Von konkreten Beispielen aus der Forschungsliteratur bis zu einem maschinengeprüften Modell.

Stufe 1: Die Beispiele aus Olsons Dissertation

Der gesamte Algorithmus ist aus Taylor Olsons Arbeit an der Northwestern University abgeleitet. Seine Dissertation “Eine formale Theorie der Normen” aus dem Juni 2025 ist die Referenz. Darin stehen vier konkrete Beispielszenarien, an denen Olson seinen Kalkül erklärt. Eine Patientin namens Karli, die einem Pflegeroboter Regeln mitteilt, welche Informationen er an wen weitergeben darf.

• Karli sagt “Du darfst meinem Mann sagen, welche Medikamente ich einnehme.” Eine einzige Erlaubnis, kein Verbot. Der Roboter darf das Rezept nennen. Fragt man ihn nach der gesamten Krankenakte, gibt es keine passende Regel. Der Roboter muss antworten: ich weiß nicht. Das ist der Fail-Closed-Fall.
• Karli sagt “Du musst meinen Gesundheitszustand mit den Kindern teilen.” Später: “Meine Krankenakte darf nicht weitergegeben werden.” Das spätere, spezifischere Verbot unterläuft die frühere Pflicht. FORBIDDEN gewinnt.
• Erlaubnis für die gesamte Krankenakte, aber explizites Verbot für die Medikamentenliste an den Mann. Bei allgemeinen Anfragen greift die Erlaubnis. Bei der spezifischen Anfrage greift das Verbot. Die Reihenfolge der Regeln ist dabei egal.
• Erlaubnis, die Krankenakte weiterzugeben. Verbot, den Mann zu verärgern. Zwei Regeln, die sich an einem Schnittpunkt treffen, wo weder die eine die andere subsumiert.

Diese vier Szenarien sind als Python-Tests abgebildet. Wenn einer davon scheitert, hat die Implementierung Olsons Kalkül an dieser Stelle nicht verstanden.

Stufe 2: Olsons vollständige Konfliktmatrix

Olson listet für jede denkbare Kombination aus Normtyp und Subsumptionsrelation das erwartete Ergebnis auf. Es ist seine eigene Zusammenfassung dessen, was sein Kalkül tun muss.

Stufe 3: Exhaustive Kombinatorik

Olsons Tabelle deckt die Konfliktfälle ab, die er theoretisch beschreibt. Aber eine reale Engine bekommt nicht nur die Fälle, an die der Autor gedacht hat. Sie bekommt alles, was Menschen oder LLMs in ein Regelwerk hineinschreiben.

Also gibt es eine dritte Teststufe, die nicht mehr an Olsons Theoremen hängt, sondern am Parameterraum der Engine selbst. Der Algorithmus hat vier Eingabedimensionen, die das Ergebnis bestimmen:

• Modalität-Paar: Welche beiden Modalitäten stehen sich gegenüber? (Permitted vs. Forbidden, Forbidden vs. Obligatory, und so weiter.)
• Spezifitäts-Relation: Ist die erste Regel spezifischer, die zweite, oder sind beide gleich tief in der Hierarchie?
• Defeasibility-Kombination: Sind beide Regeln überschreibbar, ist eine ein Axiom, sind beide Axiome?
• Code-Relation: Stammen beide Regeln aus demselben Kodex, oder aus unterschiedlichen, und wenn unterschiedlich, welcher hat Vorrang?

Sechs mal drei mal vier mal drei ergibt zweihundertsechzehn Kombinationen. Das erwartete Ergebnis wird aus Olsons Regeln programmatisch abgeleitet.

Zweihundertsechzehn ist die vollständige Aufzählung des relevanten Parameterraums. Wenn hier eine Zelle kippt, weiß ich nicht nur, dass etwas falsch ist, sondern genau welche Konstellation das Problem verursacht.

Stufe 4: Das TLA+-Modell

Tests prüfen konkrete Eingaben. Sie prüfen nicht, dass es keine Eingabe gibt, die ein Problem erzeugt. Dafür braucht es etwas anderes: ein formales Modell.

Das TLA+-Modell (eine formale Spezifikationssprache von Leslie Lamport, gedacht um Nebenläufigkeit und Zustandsmaschinen maschinenprüfbar zu beschreiben) beschreibt den sechsstufigen Algorithmus als Zustandsmaschine. Jeder Schritt ist eine Transition zwischen Zuständen. Dazu werden Invarianten formuliert. Aussagen, die in jedem erreichbaren Zustand wahr sein müssen. Zum Beispiel:

• Wenn ein widerspruchsfreies Axiom existiert, ist das Ergebnis immer die Modalität dieses Axioms. Ein moralisches Axiom darf nie von einer überschreibbaren Regel besiegt werden.
• Wenn alle anwendbaren Regeln FORBIDDEN sind, ist das Ergebnis FORBIDDEN.
• Wenn eine spezifischere Erlaubnis auf ein allgemeineres Verbot trifft, gewinnt die Erlaubnis.
• Wenn eine spezifischere Prohibition auf eine allgemeinere Permission trifft, gewinnt die Prohibition.
• Bei gleicher Spezifität und gleichem Kodex und Konflikt ist das Ergebnis UNDECIDABLE.
• Der Algorithmus terminiert für jede Eingabe.

Der TLC Model Checker (das Werkzeug, das eine TLA+-Spezifikation ausführt und den Zustandsraum absucht) probiert alle erreichbaren Zustände durch. Für jeden Zustand prüft er, ob die Invarianten halten. Wenn er einen Gegenbeispielpfad findet, zeigt er ihn an. Für bis zu vier gleichzeitig aktive Normen mit drei Modalitäten, vier Spezifitätsstufen und zwei Kodizes ist das eine endliche, aber große Menge. TLC prüft sie vollständig.

Ergänzende Eigenschaftstests

Dazu kommen Tests, die einzelne Eigenschaften der Engine gezielt prüfen. Keine neuen Szenarien, aber sie härten den Algorithmus gegen Regressionen. Die wichtigste ist die Axiom-Monotonie, die Garantie, dass ein Axiom nie von einer überschreibbaren Regel besiegt wird. Mit Hypothesis (eine Python-Bibliothek für property-based testing, die statt festen Beispielen automatisch zufällige Inputs generiert und nach Gegenbeispielen sucht) werden vierhundert zufällige Szenarien generiert, jeweils zwischen einer und fünfzig überschreibbaren Regeln plus ein Axiom. Die Invariante: das Axiom gewinnt. In keinem Durchlauf ein Gegenbeispiel.

Der Rest ist Buchhaltung, aber wichtig: Determinismus (gleiche Eingabe, gleiches Ergebnis, auch über parallele Threads und zufällig umsortierte Normen), Totality (der Algorithmus terminiert, immer), die Dualität forbidden(X) ↔ ¬permitted(X), die Closed World Assumption für registrierte Aktionen ohne Erlaubnisregel. Jede dieser Eigenschaften hat einen eigenen Testsatz, und jeder davon läuft grün. Das klingt nach Fleißarbeit, und das ist es auch. Aber es ist die Sorte Fleißarbeit, die einem später das Vertrauen gibt, eine Änderung am Algorithmus zu committen, ohne nachts wach zu liegen.

Was die Nachweiskette leistet

Man kann die einzelnen Stufen als Filter sehen, jede fängt eine andere Klasse von Fehlern. Stufe eins fängt Missverständnisse der Theorie: wenn Olsons Beispiele nicht reproduziert werden, wurde sein Kalkül schlicht nicht verstanden. Stufe zwei fängt Lücken zwischen den Beispielen, weil Olsons Tabelle Fälle abdeckt, die er in den Einzelbeispielen nicht explizit durchgeht. Stufe drei, die Kombinatorik, fängt dann die Lücken zwischen den Tabellenzeilen, also nicht-konfliktierende Paare und Defeasibility-Kombinationen, über die Olson theoretisch nichts sagt. Und Stufe vier, das TLA+-Modell, fängt die Fehler, die von keiner konkreten Eingabe getriggert werden, Invarianten eben, die in allen Zuständen halten müssen. Die ergänzenden Tests sind das Sicherheitsnetz darunter gegen Regressionen in einzelnen Eigenschaften.

Zusammen sind das über dreihundertsechzig formale Tests, plus das TLA+-Modell und die Äquivalenztests zwischen den beiden Evaluatoren. Nichts davon ersetzt einen universellen Beweis. Aber jede Stufe schließt Fehlerklassen aus, und das ist mehr, als die meisten produktiven Systeme an Nachweis haben.

Das Vertrauen in den Algorithmus kommt daher, dass er Olsons publizierte Beispiele reproduziert, seine Tabelle Zeile für Zeile erfüllt, den gesamten Parameterraum erschöpft durchläuft und unter TLC gegen die formalen Invarianten hält. Das ist eine Nachweiskette, die dokumentiert ist, reproduzierbar ist und die jederzeit nachvollzogen werden kann.

Was das in Mikrosekunden bedeutet

Die Engine läuft bei unserem Szenario in unter zehn Mikrosekunden. Nicht weil Python schnell ist, sondern weil der Algorithmus so wenig tut. Filter über eine Liste, ein bisschen Sortieren, ein paar Paarvergleiche.

Und das heißt: man kann jede einzelne Aktion eines KI-Agenten durch diesen Guard jagen, ohne dass der Agent spürbar langsamer wird. Der Guard ist nicht der Flaschenhals. Der Agent selbst ist es, weil ein LLM-Roundtrip mehrere Größenordnungen länger dauert als die DDIC-Auswertung.