LeanGuard prüft Tool-Aufrufe von KI-Agenten vor der Ausführung gegen Lean-4-Regeln

LeanGuard prüft Tool-Aufrufe vor der Ausführung gegen Lean-4-Regeln

LeanGuard ist eine Laufzeitschicht für Sprachmodell-Agenten. Jeder vorgeschlagene Tool-Aufruf wird geprüft, bevor er die Umgebung erreicht. Maßstab ist eine Richtlinie in Lean 4. Sie besteht aus Zustandsprädikaten, die mit zeitlich begrenzten Vergangenheits-Temporaloperatoren über die Ausführungshistorie verknüpft sind. Eine Regel wie „erst lesen, dann schreiben“ bezieht sich damit auf den bisherigen Verlauf der Sitzung.

Die Auswertung ist fail-closed, das heißt, im Zweifel wird nicht ausgeführt (Angabe der Autoren). Die Autoren schreiben außerdem, die Entscheidungsprozedur sei als äquivalent zu einer LeanLTL-Semantik bewiesen. Das ist ihre Angabe zum eigenen System. Eine unabhängige Prüfung liegt nicht vor.

Abgelehnte Aufrufe lassen sich auf zwei Wegen korrigieren. Beim Feedback erhält der Agent die verletzte Regel samt Hinweis und kann neu ansetzen. Bei der beweisgeleiteten Reparatur sucht Lean-Metaprogrammierung ohne Sprachmodell nach einem nahen Aufruf, der die Absicht des Nutzers wahrt, und beweist, dass die Richtlinie ihn zulässt.

Laut Autoren blockiert die Schicht auf Tau-Bench und DTap verbotene Aufrufe und senkt den Injection-Erfolg von 57,9 auf 5,9 Prozent

Die Zahlen stammen von den Autoren. Reproduktionen oder unabhängige Bewertungen gibt es bislang nicht. Auf Tau-Bench führten ungeschützte Agenten mit fünf Qwen-Modellen (0,8B bis 27B) mindestens 33 Aufrufe aus, die die Lean-Richtlinie verbietet. Mit LeanGuard waren es null. Der Aufgabenerfolg änderte sich bei Feedback nicht signifikant. Gegenüber einer bloßen Ablehnung steigerte Feedback den Erfolg bei vier von fünf Modellen und verringerte wiederholt blockierte Aufrufe. Auf DTap sank der Erfolg direkter Prompt-Injection von 57,9 auf 5,9 Prozent.

Bei wiederabgespielten Ablehnungen fand die Reparatur für 88 von 252 durch Argumentwerte verursachte Fälle eine zulässige Änderung, im Median nach 2 ms. Für knapp zwei Drittel der Fälle blieb sie also ohne Ergebnis.

Die Zusammenfassung auf der Hugging-Face-Seite wirbt damit, die Leistung bei gutartigen Aufgaben werde nicht beeinträchtigt. Das Paper trägt diese Aussage nur eingeschränkt. Im Telecom-Bereich blieb der Erfolg gleich. Dort brauchen gutartige Aufgaben jedoch keine Schreibzugriffe. Das Ergebnis sagt deshalb wenig über Aufgaben mit Schreibzugriffen aus. Die Verallgemeinerung ist werblich zugespitzt.

Das Repository liegt als Release-Kandidat v0.2.0-rc2 offen vor, der Name LeanGuard ist aber mehrfach vergeben

Die Referenzimplementierung DebarghaG/LeanGuard steht offen auf GitHub, Stand ist der Release-Kandidat v0.2.0-rc2. Ein kleiner Python-Host fängt den Aufruf ab, liest Fakten aus dem Backend und fragt die kompilierte Lean-Engine. Die Entscheidung landet in einem Journal auf der Platte, bevor das Tool läuft. Ein abgelehnter Aufruf erreicht das Backend nie.

Voraussetzungen sind Linux, Python ab 3.12, Git und curl sowie LeanLTL und mathlib. Richtlinien sind gewöhnliche Lean-4-Definitionen, die Nutzer selbst formulieren müssen. Die Demo verlangt, dass ein Dokument vor dem Schreiben gelesen wird und jeder Schreibzugriff eine Freigabe braucht.

Bei der Suche ist Vorsicht geboten: Der Name ist mehrfach vergeben. Sachlich unabhängig davon existieren ein neuro-symbolisches Framework zur Schwachstellenerkennung in Quellcode und ein 395M-Encoder zur Inhaltsmoderation von Dongbin Na (POSTECH). Weitere Arbeiten zu formalen Richtlinien für Agenten sind das Lean-Agent Protocol (Finanzbereich), eine Cedar-Autoformalisierung und CaMeL (jeweils Eigenangaben der Autoren).