BarrierBench: LLMs prüfen Barrierezertifikate für sichere dynamische Systeme

Die Sicherheit autonomer Systeme hängt entscheidend davon ab, ob ihre dynamischen Modelle zuverlässig verifiziert werden können. Traditionell erfolgt die Synthese von Barrierezertifikaten – mathematischen Funktionen, die das Durchdringen unsicherer Zustände verhindern – über aufwändige, manuell gesteuerte Verfahren. Diese Methoden leiden unter schlechter Skalierbarkeit, starkem Template‑Abhängigkeitsgrad und umfangreichem Fachwissen, das bislang nur durch sprachliche Argumentation vermittelt wurde.

Um diese Hürden zu überwinden, hat ein neues Forschungsprojekt ein agentisches Framework entwickelt, das große Sprachmodelle (LLMs) nutzt, um Barrierezertifikate zu generieren, zu verfeinern und zu validieren. Das System kombiniert natürliche Sprachlogik mit SMT‑basierten Verifikationsschritten und ermöglicht gleichzeitig die gleichzeitige Synthese von Barrieren und zugehörigen Controllern, sodass Sicherheit und Steuerung im Einklang stehen.

Zur Bewertung dieser innovativen Herangehensweise wurde BarrierBench – ein Benchmark mit 100 dynamischen Systemen, die lineare, nichtlineare, diskrete und kontinuierliche Modelle abdecken – eingeführt. Die Experimente zeigen, dass die LLM‑gestützte Synthese nicht nur die Effektivität steigert, sondern auch durch retrieval‑augmentierte Generierung und koordinierte Agentenstrategien die Zuverlässigkeit und Leistung deutlich verbessert.

Diese Fortschritte markieren einen bedeutenden Schritt in Richtung automatisierter, skalierbarer Sicherheitssicherung für autonome Anwendungen und eröffnen neue Möglichkeiten, Expertenwissen in maschinell lernbaren Systemen zu verankern.