A Neuro-Symbolic Framework for Accountability in Public-Sector AI

Diese Dissertation schlägt ein neuro-symbolisches Framework vor, das eine gesetzliche Ontologie, Regelableitung und solverbasiertes Schlussfolgern integriert, um sicherzustellen, dass automatisierte Berechtigungsentscheidungen für CalFresh mit gesetzlichen Regeln übereinstimmen, wodurch eine nachvollziehbare und anfechtbare prozedurale Rechenschaftspflicht ermöglicht wird.

Das Wesentliche

Stellen Sie sich eine Regierungsbehörde vor, die entscheidet, wer Nahrungsmittelhilfe erhält. Wenn sie einem Antragsteller „Nein" sagt, senden sie einen Brief, der erklärt, warum. Normalerweise sind diese Briefe in verwirrendem juristischen Fachjargon verfasst. Der Antragsteller liest ihn, denkt: „Das klingt vernünftig", kann aber tatsächlich nicht prüfen, ob die Regierung die Regeln korrekt befolgt. Sie sind darauf angewiesen, dem Brief zu vertrauen, weil ihnen die rechtlichen Werkzeuge fehlen, um ihn zu verifizieren.

Dieser Artikel schlägt einen neuen „digitalen Schiedsrichter" vor, um diese Briefe zu überprüfen. So funktioniert es, aufgeteilt in einfache Konzepte:

Das Problem: Die „Black Box" der Bürokratie

Stellen Sie sich den Entscheidungsprozess der Regierung als eine Black Box vor. Sie geben Ihre Informationen ein, und eine Entscheidung kommt heraus. Manchmal ist die Box ein Computerprogramm; manchmal ist es ein Mensch, der einem komplexen Regelwerk folgt. Das Problem ist, dass der an Sie gesendete „Erklärungsbrief" auf den ersten Blick gut aussehen mag, aber heimlich gegen die Regeln verstoßen könnte.

Derzeit verlassen wir uns auf „Interpretierbarkeit" – den Versuch, das Denken des Computers sichtbar zu machen. Doch die Autoren argumentieren, dass in einem rechtlichen Kontext das bloße Sehen des Denkens nicht ausreicht. Sie benötigen Überprüfbarkeit (Auditierbarkeit). Sie müssen wissen, ob die Erklärung tatsächlich mit dem Gesetz übereinstimmt, ähnlich wie man prüft, ob eine Quittung mit den gekauften Artikeln übereinstimmt.

Die Lösung: Ein „Übersetzer" und ein „Regelprüfer"

Die Autoren haben ein System namens Neuro-Symbolisches Framework entwickelt. Man kann sich dies als ein Team aus zwei Personen vorstellen, die zusammenarbeiten:

1. Der Übersetzer (Der „Neuronale" Teil):
   Stellen Sie sich einen superschlauen Roboter vor, der die unordentlichen, komplexen Regierungsgesetze (auf Englisch geschrieben) und die unordentlichen Erklärungsbriefe an Antragsteller liest. Die Aufgabe dieses Roboters ist es, diese menschliche Sprache in eine strenge, mathematische Sprache zu übersetzen, die Computer perfekt verstehen können. Es ist wie ein Übersetzer, der ein Gedicht in eine präzise Reihe mathematischer Gleichungen verwandelt.

   • Im Artikel: Sie verwendeten ein Large Language Model (LLM), um Gesetze wie „Sie müssen weniger als 2.000 Dollar verdienen" in eine formale Regel zu verwandeln: Wenn Einkommen > 2000, Dann Nicht Berechtigt.

2. Der Regelprüfer (Der „Symbolische" Teil):
   Sobald die Gesetze und die Erklärungsbriefe in mathematische Gleichungen umgewandelt sind, greift eine strenge Logikmaschine (ein sogenannter SMT-Solver) ein. Diese Maschine rät nicht; sie berechnet. Sie fragt: „Beweist der Erklärungsbrief die Entscheidung mathematisch?"

   • Wenn der Brief sagt: „Sie werden abgelehnt, weil Sie zu viel verdienen", und die Mathematik zeigt, dass Sie tatsächlich zu viel verdienen, sagt die Maschine SAT (Erfüllbar/Gültig). Die Erklärung hält stand.
   • Wenn der Brief sagt: „Sie werden abgelehnt, weil Sie zu viel verdienen", aber die Mathematik zeigt, dass Sie nicht zu viel verdienen, sagt die Maschine UNSAT (Nicht erfüllbar/Ungültig). Die Erklärung ist eine Lüge oder ein Fehler, auch wenn sie für einen Menschen plausibel klingt.

Der Realwelt-Test: CalFresh

Das Team testete dieses System auf CalFresh, dem Nahrungsmittelhilfeprogramm Kaliforniens. Sie nahmen 50 reale Fälle, in denen Menschen ihre Leistungen verweigert oder gekürzt wurden.

• Das Setup: Sie gaben dem System das tatsächliche Gesetz, die Fakten des Antragstellers (Einkommen, Familiengröße) und den offiziellen Brief, den die Regierung gesendet hatte, ein.
• Das Ergebnis: Das System fand erfolgreich „rechtliche Unstimmigkeiten". In einem Test täuschten sie das System, indem sie eine „Abgelehnt"-Entscheidung in „Genehmigt" änderten, aber dieselbe Erklärung beibehielten (die besagte, dass die Person zu viel verdiene). Das System schrie sofort UNSAT und wies darauf hin, dass die Erklärung der neuen Entscheidung widersprach.
• Der „Rauchende Colt": Wenn das System einen Fehler fand, sagte es nicht nur „Fehler". Es wies auf die genaue Seite und den genauen Absatz des Gesetzes hin, der verletzt wurde. Es ist wie ein Schiedsrichter, der nicht nur pfeift, sondern auf die spezifische Regelbuchseite zeigt, die der Spieler gebrochen hat.

Warum das wichtig ist

Die Autoren argumentieren, dass wir aufhören müssen, nur zu versuchen, zu „erklären", wie KI denkt, und beginnen müssen, die von ihr erzeugten rechtlichen Begründungen zu überprüfen (zu auditieren).

• Aktuelle Methode: „Hier ist der Grund, warum der Computer Nein gesagt hat. Es basiert auf einem Muster, das es gelernt hat." (Dies ist vor Gericht schwer anzufechten).
• Neue Methode: „Hier ist der Brief. Unser System hat ihn gegen das Gesetz geprüft und festgestellt, dass er gegen Abschnitt 63-409.111 verstößt." (Dies ist vor Gericht leicht anzufechten).

Das Fazit

Dieser Artikel behauptet nicht, die Regierung zu ersetzen oder die endgültigen Entscheidungen zu treffen. Stattdessen baut er ein digitales Sicherheitsnetz. Es stellt sicher, dass der Brief, den die Regierung Ihnen schickt, wenn sie „Nein" sagt, tatsächlich ein gültiger rechtlicher Grund ist und nicht nur eine verwirrende Ausrede. Es verwandelt die „Erklärung" von einem Papierstück, dem Sie vertrauen müssen, in ein Beweisstück, das Sie verifizieren können.

Wichtigste Erkenntnis: In der Welt der öffentlichen Leistungen geht es bei einer Erklärung nicht nur darum, klar zu sein; es geht darum, rechtlich wahr zu sein. Dieses System ist das Werkzeug, das prüft, ob die Wahrheit tatsächlich gesagt wird.

Technische Zusammenfassung

Technische Zusammenfassung: Ein neuro-symbolischer Rahmen für rechtliche Verantwortlichkeit im öffentlichen Sektor bei KI

1. Problemstellung

Öffentliche Behörden stützen sich zunehmend auf Systeme zur automatisierten Entscheidungsfindung (ADM), um den Zugang zu Sozialleistungen zu regeln. Obwohl diese Systeme Effizienz versprechen, fehlt es ihnen häufig an Transparenz, was es für Antragsteller schwierig macht, Feststellungen zur Berechtigung zu verstehen oder anzufechten. Aktuelle Ansätze für Erklärbare KI (XAI) konzentrieren sich auf Modellinterpretierbarkeit, Fidelity oder Vertrauen der Nutzer. Im rechtlichen und administrativen Kontext besteht die Hauptfunktion einer Erklärung jedoch nicht darin, lediglich verstanden zu werden, sondern als rechtliche Begründung zu dienen, die in kontradiktorischen oder quasi-gerichtlichen Verfahren angefochten werden kann.

Das identifizierte Kernproblem besteht darin, dass bestehende Erklärungen (z. B. Mitteilungen über Maßnahmen) für menschliche Leser plausibel erscheinen können, aber dennoch die richtige Rechtsgrundlage nicht zitieren oder gesetzliche Bedingungen falsch darstellen. Es fehlt an technischer Infrastruktur, um zu verifizieren, ob diese begründenden Artefakte gegenüber den maßgeblichen Gesetzen rechtlich gültig sind. Aktuelle Prüfverfahren konzentrieren sich häufig auf die Konformität auf Entscheidungsebene oder das Modellverhalten und vernachlässigen die rechtliche Integrität der Erklärungen selbst. Diese Lücke verhindert, dass Antragsteller und Aufsichtsbehörden effektiv bewerten können, ob eine Entscheidung gesetzlichen Kriterien und verfahrensrechtlichen Normen entspricht.

2. Methodik

Die Autoren schlagen einen neuro-symbolischen Rahmen vor, der entwickelt wurde, um die rechtliche Angemessenheit von Erklärungen zur Berechtigung für Sozialleistungen automatisch zu verifizieren. Das System verlagert den Fokus von der Interpretation interner Modellstrukturen hin zur Prüfung der den Antragstellern bereitgestellten Begründungen. Die Architektur besteht aus vier Hauptphasen:

2.1 Datenquellen

• Gesetzestextkorpus: Der California Manual of Policies and Procedures (MPP), Abteilung 63, der das CalFresh-Programm (SNAP) regelt.
• Falldaten: 50 Verwaltungsberufungsentscheidungen der State Hearings Division des California Department of Social Services (CDSS). Diese Aufzeichnungen umfassen die ursprüngliche Erklärung der Behörde, das Ergebnis der Feststellung und die vom Antragsteller dargelegten tatsächlichen Umstände.

2.2 Systemarchitektur

Der Rahmen arbeitet über eine Pipeline, die Rechtsnormen von fallbezogenen Behauptungen trennt:

1. Ontologie-Erstellung:

   • Ein kontrolliertes rechtliches Vokabular wird unter Verwendung von Named Entity Recognition (NER) und einbettungsbasiertem Ähnlichkeitsmatching (unter Verwendung von Qwen3-Embedding-8B) aus den MPP-Verordnungen abgeleitet.
   • Die Ontologie zielt auf Kernbereiche der Berechtigung ab: Einkommen, Wohnsitz, Staatsbürgerschaft, Vermögen und Studentenstatus.
   • Diese Struktur gewährleistet die Rückverfolgbarkeit zu autoritativen Quellen und verhindert Redundanzen.

2. TBox (Terminologischer Kasten) Kodierung:

   • Repräsentiert die normative Struktur des Gesetzes (fallunabhängige Regeln).
   • Gesetzliche Bestimmungen werden segmentiert, und operative Begriffe werden extrahiert.
   • Ein Large Language Model (LLM), spezifisch OpenAI's o1, wird angewiesen, diese Bestimmungen in formale, für Solver bereitliegende logische Regeln zu übersetzen (z. B. Implikationen, notwendige Bedingungen).
   • Jede Regel ist mit ihrer Quellenangabe verknüpft (z. B. MPP §63-409.111).

3. ABox (Assertionskasten) Konstruktion:

   • Repräsentiert fallbezogenen Inhalt (Fakten und erklärende Behauptungen).
   • Die Erklärung der Behörde wird unter Verwendung des LLM in dasselbe logische Format wie die TBox übersetzt.
   • Faktische Prädikate (z. B. Haushaltsgröße, Einkommensbeträge) werden aus den Anhörungsakten extrahiert.
   • Der ABox kombiniert die durch die Erklärung herbeigerufenen abgerufenen TBox-Regeln, die übersetzte Erklärungslogik und die spezifischen Falldaten.

4. SMT-basierte Verifizierung:

   • Ein Satisfiability Modulo Theories (SMT)-Solver bewertet die gemeinsame Erfüllbarkeit der TBox (Rechtsregeln) und der ABox (Fallbehauptungen).
   • SAT-Ergebnis: Die Erklärung steht im Einklang mit dem geltenden Recht und kann als rechtlich zulässige Begründung fungieren.
   • UNSAT-Ergebnis: Die Erklärung steht im Widerspruch zum Recht. Der Solver extrahiert einen unbefriedigbaren Kern – eine minimale Teilmenge von Einschränkungen, die für den Konflikt verantwortlich sind – und bildet diese auf spezifische gesetzliche Bestimmungen ab.

3. Hauptbeiträge

• Wandel von der Interpretierbarkeit zur Überprüfbarkeit: Die Arbeit plädiert für einen Paradigmenwechsel, bei dem die algorithmische Verantwortlichkeit im öffentlichen Sektor durch die rechtliche Gültigkeit von Erklärungen gemessen wird und nicht nur durch die Interpretierbarkeit des Modells.
• Neuro-symbolische Verifizierungspipeline: Eine neuartige Integration, bei der neuronale Komponenten (LLMs) die Extraktion und Übersetzung unstrukturierter Rechtstexte und Erklärungen übernehmen, während symbolische Komponenten (SMT-Solver) deterministische Verifizierung und Rückverfolgbarkeit bieten.
• Verantwortlichkeit auf Erklärungsebene: Im Gegensatz zu früheren Arbeiten, die Screening-Tools formalisierten (z. B. Escher und Banovic, 2020), bewertet dieser Rahmen die begründenden Artefakte (Mitteilungen über Maßnahmen), die an Antragsteller ausgegeben werden, und unterstützt so das Recht auf Anfechtung und Berufung.
• Gesetzesverankerte Signale: Das System markiert nicht nur Fehler; es erzeugt handlungsrelevante Signale zur Verantwortlichkeit, indem es genau identifiziert, welche gesetzlichen Bestimmungen durch eine Erklärung verletzt werden.

4. Ergebnisse

Der Rahmen wurde an 50 CalFresh-Fällen über fünf Berechtigungskategorien hinweg evaluiert (Studentenstatus, Einkommen, Wohnsitz, Staatsbürgerschaft, Vermögen). Für die Evaluation erstellten die Autoren gepaarte Instanzen, indem sie die Berechtigungsentscheidung umkehrten, während die Erklärung konstant blieb, um rechtliche Widersprüche zu testen.

• Verifizierungsgenauigkeit: Das System erreichte eine Gesamtgenauigkeit von 97,7 % bei der Unterscheidung zwischen rechtlich kohärenten (SAT) und inkohärenten (UNSAT) Erklärungen.
• Lokalisierungspräzision: Wenn eine Inkonsistenz erkannt wurde (UNSAT), lokalisierte das System erfolgreich die spezifische gesetzliche Bestimmung, die betroffen war.
  • Lokalisierungs-F1-Score: Variierte je nach Kategorie und reichte von 0,51 (Einkommen) bis 0,83 (Staatsbürgerschaft), mit einem Gesamtdurchschnitt von 0,977 für die UNSAT-Fälle, bei denen eine Lokalisierung anwendbar war.
  • Kategorien mit determinierteren Regeln (Staatsbürgerschaft, Wohnsitz) zeigten eine höhere Abrufgenauigkeit als solche mit kontextueller Nuance (Einkommen, Studentenstatus).
• Fallstudie: In einem spezifischen Fall, in dem die Beendigung einer Leistung damit begründet wurde, dass das „Bruttoeinkommen die Grenze überschreitet", bestätigte das System, dass die Erklärung SAT war. Als die Feststellung in „berechtigt" umgekehrt wurde, während dieselbe Erklärung beibehalten wurde, lieferte das System korrekt UNSAT zurück und identifizierte MPP §63-409.111 als die verletzte Bestimmung.

5. Bedeutung und Behauptungen

Die Autoren behaupten, dass diese Arbeit einen Proof-of-Concept für die Einbettung rechtlicher Verantwortlichkeit in die technische Substanz von KI im öffentlichen Sektor bietet.

• Institutionelle Gerüstbildung: Das System ist nicht dazu gedacht, administratives Ermessen zu ersetzen oder rechtliche Urteile zu automatisieren, sondern als „institutionelles Gerüst" zu fungieren, das Aufsicht und Anfechtbarkeit stärkt. Es automatisiert die Verifizierung von Begründungen, nicht die Entscheidungen selbst.
• Governance vor Transparenz: Die Arbeit rahmt Erklärbarkeit als Governance-Herausforderung neu. Sie geht davon aus, dass Erklärungen für öffentliche Algorithmen mehr tun müssen als statistische Assoziationen aufzudecken; sie müssen die rechtliche Grundlage einer Entscheidung darlegen, um den Ansprüchen auf ordnungsgemäßen Rechtsprozess zu genügen.
• Anwendbarkeit: Der Rahmen ist anwendbar, unabhängig davon, ob die zugrunde liegende Entscheidungsmaschine prädiktiv, regelbasiert oder hybrid ist, da sie die erklärende Ebene bewertet, die an den Antragsteller ausgegeben wird.
• Einschränkungen: Die Autoren vermerken bescheiden, dass das System auf eine aufgaben spezifische Formalisierung von Gesetzen angewiesen ist und nicht vollständig offen strukturierte Standards oder Ermessensentscheidungen erfassen kann. Die Evaluation nutzte kontrollierte Ein-Gesetz-Fälle, um eine klare Zuordnung sicherzustellen, was bedeutet, dass reale Komplexität, die mehrere interagierende Gesetze umfasst, zusätzliche Herausforderungen darstellen kann. Das System ist ein technisches Instrument für Infrastruktur zur Verantwortlichkeit, kein Ersatz für ganzheitliche rechtliche Urteilsfähigkeit.

Zusammenfassend zeigt die Arbeit, dass rechtliche Verantwortlichkeit auf Erklärungsebene durch neuro-symbolische Methoden rechnerisch handhabbar gemacht werden kann und einen Mechanismus für Behörden, Aufsichtsbehörden und Einzelpersonen bietet, um zu bewerten, ob automatisierte Begründungen gesetzlichen Anforderungen genügen.