Technische Zusammenfassung: BEAVER – Ein effizienter deterministischer LLM-Verifizierer

1. Problemstellung

Während Large Language Models (LLMs) von Forschungsprototypen zu Produktionssystemen übergehen, sehen sich Praktiker mit der kritischen Herausforderung konfrontiert, „Tail-Risiken" zu charakterisieren – seltene, aber hochwirksame Fehler wie das Offenlegen privater Informationen, das Generieren unsicherer Codes oder das Erzeugen toxischer Inhalte. Die aktuellen Bereitstellungspraktiken verlassen sich fast ausschließlich auf ad-hoc empirische Methoden, einschließlich Benchmarking, Red-Teaming und schätzungen auf Basis von Stichproben. Obwohl diese Methoden ein intuitives Verständnis bieten, liefern sie keine fundierten Garantien bezüglich des Modellverhaltens.

Die Kernschwierigkeit bei der Verifizierung von LLMs liegt in ihrer Natur als auto-regressive Modelle, die eine Wahrscheinlichkeitsverteilung über Ausgabesequenzen induzieren, anstatt eine einzelne deterministische Ausgabe zu produzieren. Bestehende neuronale Netzwerk-Verifizierer zielen auf deterministische Eingabe-Ausgabe-Beziehungen ab und können die Kombination aus probabilistischer Wahl, sequenzieller Entfaltung und Dekodierungslogik, die spezifisch für die auto-regressive Generierung ist, nicht bewältigen. Folglich wurde die fundierte Verifizierung von LLMs aufgrund des Modellumfangs und des exponentiellen Wachstums des Ausgaberaums als nicht durchführbar angesehen.

2. Methodik

Die Arbeit stellt BEAVER vor, das erste praktische Framework zur Berechnung deterministischer, fundierter Wahrscheinlichkeitsgrenzen für die Erfüllung von Sicherheitsbedingungen durch LLMs. Der Ansatz basiert auf der Beobachtung, dass viele Sicherheitsbedingungen die Form der Linearen Temporallogik (LTL) $G\phi$ einhalten (und behaupten, dass „niemals etwas Schlechtes passiert"). Für solche Bedingungen können Verstöße frühzeitig erkannt werden, was eine aggressive Beschneidung des Generierungsraums ermöglicht.

Kern-Datenstrukturen

BEAVER nutzt zwei neuartige Datenstrukturen, um den Ausgaberaum systematisch zu erkunden:

1. Token-Trie ($T$): Ein Präfixbaum, der alle erkundeten Sequenzen verfolgt, die die Sicherheitsbedingung $\Phi$ erfüllen. Jeder Knoten repräsentiert eine Token-Sequenz $s$ mit ihrer zugehörigen Wahrscheinlichkeit $\mu(s)$. Der Trie speichert nur Sequenzen, die die präfixgeschlossene Eigenschaft von $\Phi$ erfüllen.
2. Frontier ($\Psi$): Eine Menge von Blattknoten im Token-Trie, unterteilt in:
   • $\Psi_c$: Vollständige Sequenzen (endend mit <eos>).
   • $\Psi_i$: Unvollständige Sequenzen, die für eine Erweiterung in Frage kommen.

Algorithmus: Branch-and-Bound

BEAVER verwendet einen Branch-and-Bound-Algorithmus, um die Wahrscheinlichkeitsgrenzen $[P_{LB}, P_{UB}]$ für die Wahrscheinlichkeit $P$, dass eine generierte Antwort $\Phi$ erfüllt, iterativ zu verengen:

• Initialisierung: Der Trie beginnt mit der Wurzel (leere Sequenz). $P_{LB} = 0$ und $P_{UB} = 1$.
• Auswahl: Ein unvollständiger Knoten $n[x]$ wird aus der Frontier ausgewählt (typischerweise unter Verwendung einer gierigen Max-$\mu$-Heuristik, um Sequenzen mit hoher Wahrscheinlichkeit zu priorisieren).
• Erweiterung: Das Modell wird nach Wahrscheinlichkeiten für den nächsten Token $P_M(\cdot | p \cdot x)$ abgefragt. Gültige Fortsetzungen $x \cdot t$, die $\Phi$ erfüllen, werden zum Trie hinzugefügt.
• Aktualisierung: Die Grenzen werden neu berechnet:
  • $P_{LB}$ ist die Summe der Wahrscheinlichkeiten aller vollständigen, erfüllenden Sequenzen in $\Psi_c$.
  • $P_{UB}$ ist die Summe der Wahrscheinlichkeiten aller Sequenzen in $\Psi_i \cup \Psi_c$ plus ein Beschneidungs-Massen-Akkumulator ($M_p$).
• Fundiertheit: Wenn Token oder Sequenzen mit niedriger Wahrscheinlichkeit zur Gewährleistung der Skalierbarkeit beschneidet werden (z. B. durch Top-$p$- oder Top-$k$-Filter), wird ihre kumulative Wahrscheinlichkeitsmasse zu $M_p$ addiert. Dies stellt sicher, dass $P_{UB}$ in jedem Iterationsschritt eine gültige Obergrenze bleibt ($P_{LB} \le P \le P_{UB}$), unabhängig von der Beschneidung.

Der Algorithmus terminiert, wenn ein maximales Budget an Vorwärtsdurchläufen erreicht ist oder wenn die Lücke $P_{UB} - P_{LB}$ unter eine Toleranz $\epsilon$ fällt.

3. Hauptbeiträge

1. Formalisierung: Die Autoren formalisieren die Bewertung von LLM-Tail-Risiken als Verifizierungsproblem und berechnen Wahrscheinlichkeitsgrenzen für Sicherheitsbedingungen der Form $G\phi$. Sie führen die Datenstrukturen Token-Trie und Frontier ein, um die Berechnung fundierter Grenzen zu ermöglichen.
2. BEAVER-Algorithmus: Ein neuartiger Branch-and-Bound-Verifizierungsalgorithmus mit formalen Fundierbarkeitsbeweisen. Er erzeugt in jeder Iteration gültige Wahrscheinlichkeitsintervalle, die gegen die wahre Wahrscheinlichkeit konvergieren.
3. Empirische Validierung: Das Framework wird an 12 open-weight, instruktionsfeinabgestimmten Modellen (aus den Familien Llama, Qwen, Gemma, Phi, OLMo und Mistral) und vier Sicherheitsbedingungen evaluiert:
   • Datenschutzverletzung (Enron-E-Mail-Datensatz).
   • Generierung unsicherer Codes (CyberSecEval).
   • Stereotypen-Bias (DecodingTrust).
   • Toxizität (RealToxicityPrompts).

4. Ergebnisse

Die Evaluation zeigt, dass BEAVER sampling-basierte Baselines sowohl in der Effizienz als auch in der Risikoerkennung deutlich übertrifft:

• Risikoerkennung: BEAVER identifiziert 2,5- bis 3,3-mal mehr riskante Instanzen als ein sampling-basierter Verifizierer (SV), selbst wenn er mit 1/10 des Rechenbudgets arbeitet (100 Vorwärtsdurchläufe gegenüber ~1000 für SV).
• Aufdeckung von Tail-Risiken: BEAVER bestätigt nicht-triviale Tail-Risiken (Verletzungswahrscheinlichkeit $\ge 10\%$) bei einem erheblichen Anteil von Prompts, die durch ad-hoc-Evaluation als sicher erklärt werden.
• Aufgabenabhängige Profile: Die Ergebnisse zeigen, dass Risikoprofile stark aufgabenabhängig sind und nicht sauber mit der Modellgröße korrelieren. Beispielsweise zeigt Qwen3-4B ein hohes Risiko bei Datenschutz und Codesicherheit, ist jedoch bei Toxizität sicher, während Gemma-3-4B das inverse Muster aufweist.
• Effizienz: BEAVER konvergiert in moderater Wandzeit zu engen Grenzen ($\epsilon=0,01$) (z. B. ~9,4 s für Enron, ~18,8 s für Secure Code) mit Speicherverbräuchen unter 5 MB pro Instanz.
• Distributionelle Zertifizierung: Die Arbeit zeigt, dass prompt-spezifische Garantien mit statistischen Techniken (Clopper-Pearson) kombiniert werden können, um distributionelle Sicherheitsgarantien über große Eingabemengen zu bieten – eine Fähigkeit, die von bestehenden Evaluierungsmethoden nicht geboten wird.

5. Bedeutung und Behauptungen

Die Arbeit behauptet, dass die deterministische Verifizierung des LLM-Verhaltens sowohl machbar als auch praktisch für den Einsatz in der realen Welt ist. Durch den Schritt über ad-hoc-Stichproben hinaus ermöglicht BEAVER eine prinzipielle Risikobewertung, die Tail-Risiken aufdecken kann, die für einzelne Sicherheitswerte unsichtbar sind.

Die Autoren betonen, dass ihr Ansatz fundierte Garantien statt statistischer Schätzungen liefert. Dies ist für sicherheitskritische Szenarien entscheidend, bei denen eine Verletzungsrate von 10 % in der Produktion Tausende unsicherer Ausgaben bedeuten könnte. Das Framework stellt fest, dass LLM-Tail-Risiken fundiert und handhabbar charakterisiert werden können, und bietet eine rigorose Alternative zu aktuellen empirischen Evaluierungsmethoden.

Einschränkungen: Das aktuelle Framework zielt auf präfixgeschlossene Sicherheitsbedingungen ($G\phi$) ab, erlaubt jedoch Erweiterungen auf nicht-präfixgeschlossene Bedingungen. Es setzt weißen-Box-Zugriff auf vollständige Token-Wahrscheinlichkeitsverteilungen voraus und verwendet Heuristiken (Max-$\mu$) für die Auswahl, die die Autoren als verbesserbar mit gelernten Wertfunktionen für schwierigere Spezifikationen ansehen.