💻 computer science

VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents

VASO ist ein neuartiges Framework, das die Selbstevolution von durch LLMs generierten Roboterfertigkeitskontrakten durch formale Verifikation ermöglicht, indem es Gegenbeispiele nutzt, um wiederverwendbare Fertigkeiten iterativ gegen temporale Sicherheitsspezifikationen zu verfeinern, ohne die Gewichte des Basismodells zu modifizieren, wodurch eine hohe Konformität bei physischen Agenten mit minimalen Optimierungsstichproben erreicht wird.

Ursprüngliche Autoren: Yunhao Yang, Neel P. Bhatt, Kevin Wang, Samuel Tetteh, Zhangyang Wang, Ufuk Topcu

Veröffentlicht 2026-06-05

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Yunhao Yang, Neel P. Bhatt, Kevin Wang, Samuel Tetteh, Zhangyang Wang, Ufuk Topcu

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Das große Problem: „Intelligente“ Roboter, denen man nicht vertrauen kann

Stellen Sie sich vor, Sie stellen einen sehr talentierten, kreativen Koch (die KI) ein, der Rezepte (Fähigkeiten) für eine Roboter-Küche schreibt. Der Koch kann in Sekundenschnelle ein Rezept für „Mache ein Sandwich“ oder „Vermeide die Katze“ schreiben.

Es gibt jedoch einen Haken: Nur weil das Rezept auf Englisch gut klingt, heißt das noch lange nicht, dass der Roboter nicht das Haus abfackelt.

Aktuelle Methoden versuchen dies zu beheben, indem sie den Roboter das Rezept ausprobieren lassen, prüfen, ob es fehlschlägt, und den Koch bitten, es neu zu schreiben. Das ist so, als würde man an einer Suppe probieren und sagen: „Sie ist zu salzig, versuch es nochmal.“ Aber das sagt einem nur, dass die Suppe dieses eine Mal zu salzig war. Es beweist nicht, dass das Rezept für jede erdenkliche Situation sicher ist (z. B. wenn der Herd zu heiß wird oder eine Katze auf die Arbeitsplatte springt).

Die Lösung: VASO (Der „mathematische Lektor“)

Die Autoren führen VASO ein, ein System, das wie ein strenger, mathematischer Lektor für diese Roboter-Rezepte fungiert. Anstatt nur die Suppe zu probieren, gleicht VASO das Rezept mit einem Satz unumstößlicher Sicherheitsregeln ab (wie „Berühre niemals Feuer“ oder „Halte immer an, wenn eine Person in der Nähe ist“).

So funktioniert VASO, Schritt für Schritt:

1. Der „Übersetzer“ (Die Brücke)

Roboter sprechen „Code“ (bewege links, halte an, beschleunige), aber Sicherheitsregeln sind in „Logik“ geschrieben (Wenn Person gesehen, dann Stopp).

Die Analogie: Stellen Sie sich vor, der Roboter ist ein Ausländer, der nur „Roboter“ spricht, und der Sicherheitsinspektor spricht nur „Logik“.
Was VASO macht: Es erstellt einen Übersetzer (eine sogenannte Labeling Function), der die Bewegungen des Roboters sofort in logische Aussagen umwandelt. Dies ermöglicht es dem Sicherheitsinspektor, genau zu verstehen, was der Roboter tut.

2. Der „Mathe-Check“ (Formale Verifikation)

Bevor der Roboter das Rezept überhaupt ausprobiert, führt VASO eine mathematische Simulation durch.

Die Analogie: Denken Sie an einen Flugsimulator für Piloten. Bevor das Flugzeug abhebt, lässt der Simulator Millionen von Szenarien durchlaufen, um zu sehen, ob der Flugplan mit einem Berg kollidiert.
Was VASO macht: Es prüft, ob das Rezept jemals gegen die Sicherheitsregeln verstoßen könnte. Wenn die Mathematik sagt: „Ja, dieses Rezept könnte einen Absturz verursachen“, sagt das System nicht einfach nur „Fehlgeschlagen“. Es findet den exakten Moment, in dem der Absturz passiert (das „Gegenbeispiel“ bzw. „Counterexample“).

3. Der „Text-Gradient“ (Die Feedback-Schleife)

Dies ist der magische Teil. Normalerweise muss man bei einem fehlgeschlagenen Mathe-Check den gesamten Code neu schreiben. VASO ist klüger.

Die Analogie: Stellen Sie sich vor, der Mathe-Check schickt dem Koch eine Notiz: „Dein Rezept sagt ‚Gehe vorwärts‘, obwohl eine Person da ist. Ändere diese Zeile in ‚Stopp‘.“
Was VASO macht: Es verwandelt den mathematischen Fehler in eine Text-Anweisung (einen „textuellen Gradienten“). Es sagt dem KI-Koch genau, wie er das Rezept selbst umschreiben muss, um den Fehler zu beheben.
Wichtiges Detail: Das Gehirn des KI-Kochs (das zugrunde liegende Modell) bleibt unverändert. Wir trainieren nicht den Koch neu; wir bearbeiten lediglich die spezifische Rezeptkarte, die er geschrieben hat.

Warum das eine große Sache ist

Die Autoren haben dies an zwei echten Robotern getestet: einem Bodenroboter (wie ein Roomba auf Steroiden) und einer Drohne.

Das Ergebnis: VASO brachte die Roboter dazu, die Sicherheitsregeln 97,2 % der Zeit einzuhalten – und das mit weniger als 100 Versuchen.
Der Vergleich: Andere Methoden (wie die KI einfach nur nochmal probieren zu lassen oder das Gehirn der KI neu zu trainieren) waren entweder weniger sicher oder nahmen viel mehr Zeit in Anspruch und verbrauchten mehr Rechenleistung.

Der „selbstentwickelnde“ Teil

Die Arbeit bezeichnet dies als „Self-Evolving Skills“ (Selbstentwickelnde Fähigkeiten).

Der alte Weg: Man trainiert einen Roboter mit einer Million Beispielen, und er lernt ein allgemeines „Gefühl“ dafür, was zu tun ist.
Der VASO-Weg: Man gibt dem Roboter eine spezifische Fähigkeit (wie „Fahren“), prüft sie mit Mathematik, findet den Fehler und aktualisiert die Definition der Fähigkeit. Nun ist dieselbe Fähigkeit auch für jede zukünftige Aufgabe besser geeignet. Es ist, als würde man den Bauplan eines Automotor-Designs verbessern, sodass jeder aus diesem Bauplan gefertigte Wagen sicherer ist, anstatt nur ein einzelnes Auto zu reparieren.

Zusammenfassung in einem Satz

VASO ist ein System, das mathematische Beweise nutzt, um Fehler in Roboter-Anweisungen zu finden, diese Fehler in einfache Text-Rückmeldungen übersetzt und die „Rezepturen“ der Roboter automatisch umschreibt, damit sie perfekt sicher sind, ohne das Gehirn der KI neu trainieren zu müssen.

Was die Arbeit nicht behauptet

Sie behauptet nicht, dass dies bereits für die chirurgische Medizin oder lebenskritische Entscheidungen funktioniert (sie wurde für Navigation und Drohnen getestet).
Sie behauptet nicht, dass der Roboter „bewusst“ ist oder Sicherheit „versteht“; er folgt lediglich den mathematisch verifizierten Regeln.
Sie behauptet nicht, dass dies sofort für jedes mögliche Roboterszenario funktioniert; es hängt davon ab, dass der „Übersetzer“ (die Labeling Function) korrekt geschrieben wurde. Wenn der Übersetzer einen Fehler macht, könnte die mathematische Prüfung ein falsches Gefühl von Sicherheit vermitteln.

Technisches Resümee: VASO – Formal verifizierbare, selbstentwickelnde Fähigkeiten für physische KI-Agenten

Problemstellung

Wiederverwendbare Roboterfertigkeiten dienen als Schnittstelle zwischen Fundamentmodellen und physischer Steuerung, wodurch eingebettete Agenten in der Lage sind, langfristige Aufgaben unter Sicherheitsbeschränkungen auszuführen. Während Fundamentmodelle die Kosten für die Generierung dieser Fähigkeiten mittels natürlicher Sprache gesenkt haben, konnten sie das Problem der Fähigkeitsabsicherung (Skill Assurance) noch nicht lösen. Bestehende Methoden zur Selbstentwicklung verlassen sich auf „weiche“ Feedbacksignale – wie etwa Ausführungsergebnisse, Unit-Tests, Umgebungsbelohnungen oder LLM-Selbstkritik. Diese Signale liefern lediglich belegbasierte Evidenz auf Trace-Ebene, die zwar zeigt, dass eine Fähigkeit bei Stichproben-Ausführungen funktionierte, aber keine Garantie dafür bietet, dass die durch die Fähigkeit induzierten Pläne unter ungetesteten Bedingungen zeitliche Sicherheitsverträge erfüllen. In der Robotik ist ein einzäufiger, seltener, aber schwerwiegender Sicherheitsverstoß (z. B. ein Bodenroboter, der sich bewegt, nachdem eine Person erkannt wurde) inakzeptabel, doch weiches Feedback versagt oft dabei, solche Grenzfälle zu erkennen.

Die zentrale Herausforderung besteht darin, den Kreislauf zwischen formaler Verifizierung und der Entwicklung von Fähigkeiten zu schließen, ohne lediglich unsichere Pläne zu filtern oder die Gewichte des Modells feinabzustimmen. Es bedarf einer Repräsentation, in der formale Gegenbeispiele direkt die Verträge wiederverwendbarer Fähigkeiten aktualisieren können, um sicherzustellen, dass Verbesserungen inspizierbar, wiederverwendbar und verifizierbar sind.

Methodik: VASO-Framework

Die Autoren schlagen VASO (Verification-Guided Automated Skill Optimization) vor, ein geschlossenes Framework für die Selbstentwicklung von LLM-generierten Roboter-Fähigkeitsverträgen. VASO operiert, indem es Fähigkeiten als semantische Verträge behandelt, die eine formale Schnittstelle mit einer planorientierten Schnittstelle koppeln.

1. Verifizierbare Fähigkeitsrepräsentation

Eine Fähigkeit $sk$ wird als Tupel $(G, \psi_{sk}, C_{sk})$ definiert:

$G$ (Globale Spezifikationen): Eine Menge von LTL-Formeln, die Sicherheitsbeschränkungen repräsentieren, die stets gelten müssen.
$\psi_{sk}$ (Lokale Regel): Eine LTL-Formel, die die spezifische Intention oder das Ziel der Fähigkeit definiert.
$C_{sk}$ (Semantischer Vertrag):: Die Kernkomponente, bestehend aus:
- $L_{sk}$ (Proposition-Aligned Labeling Function): Eine Funktion, die niedrige Roboterzustände, Beobachtungen und Steuerbefehle auf atomare logische Propositionen abbildet. Dies überbrückt die Lücke zwischen physischer Ausführung und symbolischer Modellprüfung.
- $C^p_{sk}$ (Text-basiertes Plan-Template): Eine Verhaltensprior, die den Planer bei der Generierung ausführbarer Befehle (z. B. API-Aufrufe oder Trajektorien) leitet.

2. Zweistufiger Verifizierungskreislauf

VASO nutzt einen hierarchischen Verifizierungsprozess, um Fähigkeiten zu verfeinern:

Fähigkeitsebene-Verifizierung (Machbarkeitsprüfung): Bevor Pläne gesampelt werden, prüft das Framework, ob die lokale Regel $\psi_{sk}$ logisch konsistent mit den globalen Spezifikationen $G$ ist. Ein universelles Übergangssystem wird konstruiert, um die Erfüllbarkeit zu verifizieren. Wenn die lokale Regel im Widerspruch zur globalen Sicherheit steht (z. B. eine Regel, die Bewegung befiehlt, während eine Person beobachtet wird), wird die Fähigkeit abgelehnt und das Fundamentmodell wird zur Verfeinerung der lokalen Regel abgefragt.
Planebene-Verifizierung (Verhaltensprüfung): Sobald eine machbare Fähigkeit vorliegt, generiert ein Planer einen ausführbaren Plan $\pi$ . Dieser Plan wird unter Verwendung der Labeling-Funktion $L_{sk}$ in ein symbolisches Übergangssystem (Automaten) kompiliert. Ein Model Checker (NuSMV) verifiziert den Plan gegen $G \land \psi_{sk}$ .

3. Optimierung via Textueller Gradienten

Wenn die Verifizierung fehlschlägt, gibt der Model Checker einen Gegenbeispiel-Trace zurück. VASO konvertiert diesen Trace in einen textuellen Gradienten (z. B. „verstößt gegen Spezifikation: $G(\text{person\_observed} \to X \text{ stop})$ “). Dieses textuelle Feedback wird in das Fundamentmodell zurückgespeist, um den semantischen Vertrag $C_{sk}$ und die lokale Regel $\psi_{sk}$ zu aktualisieren.

Zentrale Einschränkung: Die Gewichte des Fundamentmodells bleiben eingefroren. Die Optimierung erfolgt vollständig auf Ebene des Prompt/Vertrags, indem das wiederverwendbare Fähigkeitsartefakt verfeinert wird, statt die Modellparameter oder einen einzelnen Task-Prompt zu tunen.
Prozess: Der Kreislauf wechselt zwischen Vorwärtsgenerierung (Vertrag $\to$ Plan $\to$ Automat) und Rückwärtsverfeinerung (Automat $\to$ Textueller Gradient $\to$ Aktualisierter Vertrag).

Zentrale Beiträge

Verifizierbare, selbstentwickelnde Fähigkeitsrepräsentation: Das Paper führt eine Fähigkeitsstruktur ein, die zeitlogische Spezifikationen, proposition-ausgerichtete Robotersemantik und planorientierte Templates explizit miteinander verbindet. Dies ermöglicht es, LLM-generierte Fähigkeiten für die Planung zu nutzen und gleichzeitig der formalen Verifizierung zugänglich zu machen.
Formale Gegenbeispiele als Optimierungsfeedback: Die Autoren entwickeln einen zweistufigen Verifizierungskreislauf, in dem Gegenbeispiel-Traces in textuelle Gradienten umgewandelt werden. Dies ermöglicht die Verfeinerung des wiederverwendbaren Fähigkeitsvertrags selbst, anstatt nur einen spezifischen Plan abzulehnen oder einen Prompt zu optimieren.
Validierung am physischen Agenten: Das Framework wird auf realen Roboterplattformen (Clearpath Jackal und PX4 Quadrocopter) validiert und zeigt, dass optimierte Fähigkeiten eine hohe Übereinstimmung mit formalen Spezifikationen erreichen können, ohne das zugrunde liegende Fundamentmodell feinabzustimmen.

Empirische Ergebnisse

Das Framework wurde auf 11 temporal-logischen Spezifikationen über 400 generierte Pläne auf zwei Roboterplattformen evaluiert.

Compliance: VASO erreichte eine formale Spezifikations-Compliance von 97,2 % mit weniger als 100 Optimierungsstichproben (unter 20 Minuten pro Fähigkeit).
Vergleich: Es übertraf Zero-Shot-Baselines, Prompt-Optimierungsmethoden (wie LAD-VF) und auf Fine-Tuning basierende Ansätze (wie RLVF). Bemerkenswerterweise erreichte VASO höhere Sicherheitswerte als Fine-Tuning-Methoden bei nur einem Bruchteil der Trainingskosten und -zeit.
Generalisierung: Optimierte Fähigkeiten zeigten eine starke Generalisierung auf ungesehene Task-Prompts innerhalb derselben Task-Familie und behielten hohe Sicherheits- und Aufgabenerfüllungsraten ohne zusätzliche Verfeinerung bei.
Automatische Ausrichtung: Die Studie zeigte, dass automatisch generierte, proposition-ausgerichtete Labeling-Funktionen auf Augenhöhe mit handgefertigten Abbildungen performten, was die Notwendigkeit manueller Domänenexpertise zur Definition symbolischer Abstraktionen eliminierte.

Bedeutung und Ansprüche

Das Paper beansprucht, das erste Framework zu sein, das den Kreislauf zwischen formaler Verifizierung und selbstentwickelten LLM-generierten Fähigkeiten für physische KI-Agenten schließt.

Paradigmenwechsel: Im Gegensatz zu Standard-Verifizierungs-Pipelines für die Planung, die Verifizierung lediglich als Pass/Fail-Filter für einmalige Pläne nutzen, verwendet VASO den Grund für die Ablehnung (das Gegenbeispiel), um die Quelle des Plans (die wiederverwendbare Fähigkeit) zu verbessern.
Effizienz und Sicherheit: Durch die Optimierung des Fähigkeitsvertrags anstatt der Modellgewichte bietet VASO einen Mechanismus zur Generierung sichererer, zuverlässigerer Verhaltensweisen, die über verschiedene Aufgaben hinweg inspizierbar und wiederverwendbar sind, und adresst damit den kritischen Engpass der Fähigkeitsabsicherung in der physischen KI.
Limitierungen: Die Autoren räumen ein, dass die formalen Garantien von der Korrektheit der KI-generierten, proposition-ausgerichteten Labeling-Funktion abhängen. Fehler bei der Abbildung niedriger Dynamiken auf symbolische Propositionen könnten zu fehlerhaften Verifizierungsergebnissen führen, obwohl empirische Daten darauf hindeuten, dass dies selten vorkommt (< 1 % Degradation der Sicherheitswerte). Das aktuelle Framework setzt zudem eine sequentielle, nicht-konkurrente Ausführung voraus.