Closed-Loop Sicherheits Verifikation gelernter Tree-Ensemble Policies im Planen

• Antragsteller: Professor Dr. Jörg Hoffmann
• Fachliche Zuordnung: Künstliche Intelligenz und Maschinelle Lernverfahren
• Förderung: Förderung seit 2026
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 568838440

Safe AI, insbesondere die Verifikation gelernter Entscheidungskomponenten, ist ein wichtiges Problem in der KI. In diesem Projekt betrachten wir sogenannte action policies in KI Handlungsplanung: gelernte Funktionen pi von Zuständen in Aktionen, welche einen Agenten kontrollieren der ein Ziel erreichen soll. Unser Projektvorschlag adressiert "closed-loop" Sicherheits Verifikation von pi, den Beweis dass pi niemals einen unsicheren Zustand erreicht; in enger Kombination mit Lernmethoden die Verifizierbarkeit fördern. Wir adressieren dies für tree ensembles. Dies ist motiviert durch unsere gemeiname Vorarbeit (ECAI'24), in der wir policy predicate abstraction (PPA) entwickelt haben als Methode für closed-loop Sicherheits Verifikation von tree-ensemble policies im KI Handlungsplanungs Kontext. Unser Schlüsselresultat ist dass tree ensembles in diesem Kontext oft ähnlich performant sind wie neuronale Netzwerke, aber um mehrere Größenordnungen leichter zu verifizieren. Möglicherweise bieten also tree ensembles einen besseren Kompromiss zwischen Performanz vs. Verifizierbarkeit, zumindest im Bereich der policies für die formale Verifikation praktikabel ist. Diese Hypothese kann wichtige Konsequenzen haben für die Wahl des ML Modells in Situationen wo Verifizierbarkeit wichtig ist. Das Ziel dieses Projektes ist, die Hypothese zu bestätigen. Dazu ist es nötig, mehrere signifikante und miteinander verwandte technische Probleme zu addressieren, die entstehen weil tree ensembles im allgemeinen komplexe input features benötigen um performant zu sein, d.h., features die über die Umgebungszustands Repräsentation durch Zustandsvariablen hinaus gehen. Erstens brauchen wir Methoden um sinnvolle komplexe features automatisch im Trainingsprozess zu konstruieren, unter Berücksichtigung von Verifizierbarkeit. Zweitens kann PPA in seiner aktuellen Form nicht mit komplexen features umgehen und muss entsprechend erweitert werden. Dies impliziert zum einen reasoning über constraints auf solche features, eine Fähigkeit die aktuelle tree-ensemble reasoners nicht haben. Zum anderen implizieren komplexe features eine neue Form von spuriousness (Impräzision) in PPA, welche neue abstraction refinement Methoden erfordert. Wir addressieren diese Probleme für zwei Arten formaler Umgebungsmodelle. Erstens Automatenmodelle, die wir auch in unseren Vorarbeiten verwendet haben. Zweitens PDDL, dem de-fakto Standard in KI Handlungsplanung, wo die wichtige neue Herausforderung darin besteht, über Umgebungs-Instanzen zu generalisieren, sowohl im Lernen als auch in der Verifikation. Das Projekt vereint die Expertise von PI Davis in tree-ensemble Lernen und reasoning mit der Expertise von PI Hoffmann in KI Handlungsplanung und closed-loop policy Sicherheits Verifikation. Diese Vereinigung ist nötig, es wäre für jeden einzelnen Partner unmöglich die vorgeschlagene Forschung erfolgreich auszuführen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Belgien
• Kooperationspartner: Professor Jesse Davis, Ph.D.