Prove It, Teil 2: Formale Logik, Cedar-Richtlinien und die Ökonomie der Überprüfung

Automated Reasoning ergänzt die LLM-Ergebnisse um eine Überprüfung, indem Geschäftsrichtlinien in formale Logik übersetzt und anhand dieser Regeln überprüft werden. Es erkennt Halluzinationen, setzt Compliance-Einschränkungen durch und kontrolliert die Aktionen der Agenten – und das zu einem Bruchteil der Kosten einer manuellen Qualitätssicherung.

In Teil 1 („'Probably Correct' Is Not Good Enough“) haben wir behandelt, warum Startups, die auf KI aufbauen, eine deterministische Überprüfung benötigen und nicht nur probabilistische Schutzmaßnahmen. In diesem Beitrag werfen wir einen Blick hinter die Kulissen. Wenn Sie technischer Mitbegründer, technischer Leiter oder leitender Entwickler bei einem KI-Startup sind, erfahren Sie hier, wie Automated Reasoning tatsächlich funktioniert, was passiert, wenn Ihr LLM eine Antwort generiert und diese durch formale Logik überprüft wird, und warum dies aus wirtschaftlicher Sicht im Vergleich zur Einstellung von QA-Teams ein Kinderspiel ist.

Kein API-Code in diesem Beitrag. Das kommt in Teil 3. Hier konzentrieren wir uns auf Konzepte, formale Logik und die Überprüfungs-Pipeline, damit Sie verstehen, was Sie erstellen.

Stochastisch vs. deterministisch: Der grundlegende Unterschied

Bevor wir uns mit den technischen Details befassen, lohnt es sich, den zentralen Unterschied klar zu definieren, da er sich auf jede architektonische Entscheidung auswirkt, die Sie treffen.

LLMs sind stochastisch.

Sie sagen das nächste Token auf der Grundlage von Wahrscheinlichkeitsverteilungen voraus, die aus Trainingsdaten gelernt wurden. Die Stichprobenparameter „Temperatur“, „Top-K“ und „Top-P“ führen zu bewusster Zufälligkeit. Wenn Sie denselben Prompt zweimal ausführen, erhalten Sie möglicherweise unterschiedliche Antworten. Dies ist eine Funktion, kein Fehler: Genau das macht LLMs flexibel, kreativ und fähig, verschiedene Eingaben in natürlicher Sprache zu verarbeiten. Es bedeutet aber auch, dass jede einzelne Ausgabe eine Stichprobe aus einer Wahrscheinlichkeitsverteilung ist und keine nachgewiesene Tatsache.

Automated Reasoning (AR) ist richtig.

Ausgehend von einer Reihe von Regeln und einer Eingabe ist das Ergebnis keine beste Schätzung. Es ist ein Beweis. Eine Aussage ist entweder in Bezug auf Ihre Regeln nachweislich gültig, nachweislich ungültig, oder das System teilt Ihnen genau mit, welche Informationen fehlen oder nicht eindeutig sind. Wenn die Antwort falsch ist, weist AR nicht nur darauf hin, sondern liefert Ihnen ein Gegenbeispiel, das genau zeigt, warum sie falsch ist. Die Ausgabe ist mathematisch überprüfbar, nicht probabilistisch. Es gibt keinen Temperaturregler. Es gibt keine Stichproben. Es gibt einen Beweis, den Sie überprüfen können.

Es geht nicht darum, dass ein Ansatz „besser“ ist. LLMs sind besser darin, natürliche Sprache zu verstehen und menschenähnliche Reaktionen zu erzeugen. AR ist besser darin, zu überprüfen, ob diese Antworten logisch korrekt sind. Zusammen bilden sie das komplette System: Das LLM kümmert sich um die Konversation, AR kümmert sich um die Richtigkeit. Diese Kombination aus neuronalen Netzwerken und formaler Logik nennen Forscher neurosymbolische KI.

Für ein fünfköpfiges Startup, das seine ersten 100 Kunden beliefert, hat diese Unterscheidung eine sehr praktische Konsequenz. Sie verfügen weder über die personellen Ressourcen für ein QA-Team noch über den finanziellen Spielraum, um einen Compliance-Vorfall abzufedern. Die formelle Überprüfung wird zu einem Multiplikator, der es einem kleinen Team ermöglicht, mit der Zuversicht eines viel größeren Teams zu liefern.

Was sind die beiden Schutzebenen in Amazon Bedrock?

AWS bietet AR auf zwei Ebenen und entspricht exakt der Reifegradkurve der meisten KI-Startups. Wenn Sie sich in einem frühen Stadium befinden, ist Ihr Produkt wahrscheinlich ein Chatbot oder Assistent: ein LLM, der Kundenfragen beantwortet, Empfehlungen ausgibt oder Anleitungen gibt. In dieser Phase überprüft Automated Reasoning in Amazon-Bedrock-Integritätsschutz den Inhalt der Modellergebnisse anhand definierter Geschäftsregeln.

Wenn Sie wachsen, beginnen Sie, agentenbasierte Workflows zu entwickeln: Ihre KI bucht Termine, verarbeitet Rückerstattungen, fragt Datenbanken ab und ruft externe APIs auf. Auf dieser Ebene regelt die Policy in Amazon Bedrock AgentCore, welche Aktionen ein Agent ergreifen darf. Dabei werden die Cedar-Richtlinien verwendet, die am Gateway vor jeder Ausführung des Tools durchgesetzt werden.

Cedar-Richtlinien regeln, was ein Agent tun kann. Sie können die AR-Checks-API aber auch als Tool im Toolkit des Agenten bereitstellen, sodass der Agent seine eigenen Zwischenergebnisse überprüfen kann, bevor er darauf reagiert. Der Agent ruft ApplyGuardrail anhand Ihrer Richtlinien auf, überprüft die Ergebnisse und korrigiert sich selbst, ohne den Benutzer einzubeziehen. Ein Agent, der einen mehrstufigen Workflow plant, kann prüfen, ob die vorgeschlagene Reihenfolge gegen eine Einschränkung verstößt, Widersprüche in seinen Annahmen erkennen oder bestätigen, dass aus den Eingaben tatsächlich ein abgeleiteter Wert folgt. Dadurch wird AR von einer Grenzprüfung zu einem Reasoning-Partner: Der Agent wird nicht einfach am Tor gestoppt, sondern vermeidet es von vornherein, sich überhaupt in Richtung des Tors zu bewegen.

Hier ist ein Vergleich:

AR-Prüfungen und Policy in Amazon Bedrock AgentCore schützen verschiedene Ebenen Ihrer Anwendung.

• AR-Prüfungen überprüfen, was Ihre KI sagt, d. h.: Ist diese Antwort zur Hypothekenberechtigung gemäß Ihren Kreditvergabekriterien korrekt?
• Policy in Amazon Bedrock AgentCore steuert, was Ihre KI tut, d. h.: Ist dieser Agent berechtigt, eine Rückerstattung einzuleiten oder das Konto eines Kunden abzufragen?

 Je nachdem, was Sie derzeit entwickeln, können Sie mit einem oder beiden beginnen.

• Wenn Ihr MVP ein Chatbot ist, der Fragen zu Richtlinien beantwortet, sollten Sie zunächst AR-Prüfungen integrieren.
• Wenn Sie einen Agenten bereitstellen, der Termine bucht und Geld überweist, ist Policy vom ersten Tag an unverzichtbar.

Die meisten Startups werden letztendlich beide gemeinsam einsetzen.

So funktionieren AR-Prüfungen: Kodierung Ihrer Unternehmensregeln als formale Logik

Die Eingabe für AR ist eine Richtlinie, und eine Richtlinie beginnt mit Dokumenten, die Sie bereits haben.

Wenn Sie ein Fintech-Startup sind, könnte es sich um ein Dokument mit Kreditvergabekriterien handeln. Im Gesundheitswesen können es klinische Protokolle oder Verfahren zur Einhaltung der HIPAA-Vorschriften sein. In der Versicherungsbranche sind es versicherungstechnische Richtlinien. Diese Dokumente legen fest, was Ihre KI sagen sollte und was nicht. Sie wurden von Ihrem Rechtsbeistand geprüft. Ihre Investoren haben im Rahmen der Due Diligence danach gefragt. AR wandelt diese vorhandenen Artefakte in durchsetzbare Regeln um. Sie entwickeln nichts Neues von Grund auf. Sie aktivieren etwas, das Sie bereits haben.

Wenn Sie ein Richtliniendokument (PDF, Markdown oder Klartext) auf Amazon Bedrock hochladen, extrahiert das System 2 Dinge: Variablen und Regeln.

Variablen stellen die Konzepte in Ihrer Domain dar. Jede Variable hat einen Namen, einen Typ und eine Beschreibung. Beispielsweise in einer Richtlinie zur Hypothekenberechtigung:

Die Variablenbeschreibungen sind der wichtigste Faktor für die Genauigkeit. Vage Beschreibungen führen dazu, dass das LLM nur raten kann, was eine Variable darstellt. Detaillierte Beschreibungen, die erklären, was das Konzept bedeutet, wie Ihre Benutzer es bezeichnen und wie es in Ihren Richtliniendokumenten erscheint, liefern dem LLM den Kontext, den es benötigt, um natürliche Sprache den richtigen formalen Variablen zuzuordnen. Hier kommt Ihr Fachwissen als Startup-Gründer am meisten zum Tragen.

Regeln sind formale Logikausdrücke, die Beziehungen zwischen Variablen erfassen. Sie verwenden eine Teilmenge der SMT-LIB-Syntax und die meisten folgen einem „Wenn-Dann“-Format (implikativ):

Das ist es, was Bedrock im Hintergrund generiert, wenn Sie Ihr Hypothekenrichtliniendokument hochladen. Sie können diese Regeln in der Konsole überprüfen, um sicherzustellen, dass das System Ihre Absicht korrekt erfasst hat, aber Sie schreiben SMT-LIB nicht von Hand. Sie schreiben die Richtlinie in natürlicher Sprache, und das System übersetzt sie in formale Logik.

Der zweistufige Überprüfungsprozess

Sobald Sie eine AR-Richtlinie eingerichtet und an einen Integritätsschutz angehängt haben (siehe Teil 3), durchläuft jede LLM-Antwort, die Ihre Anwendung an ApplyGuardrail sendet, einen zweistufigen Überprüfungsprozess. Es ist wichtig, diese Aufteilung zu verstehen, da sie Ihnen zeigt, worauf Sie Ihren Einsatz konzentrieren sollten.

Schritt 1: Übersetzung

Das System wandelt die natürliche Sprache sowohl in der Benutzerfrage als auch in der Antwort des LLM unter Verwendung der in Ihrer Richtlinie deklarierten Variablen in formale Logikprädikate um – also Aussagen wie earning “>= 180 & earning <= 220” anstelle einfacher Zuweisungen. Hier kommen die Variablenbeschreibungen ins Spiel.

Wenn die Antwort beispielsweise lautet: „Ein Kunde, der eine Anzahlung von 30 000 USD auf ein Haus im Wert von 350 000 USD geleistet hat, hat Anspruch auf eine konventionelle Hypothek“, ergibt sich aus dem Übersetzungsschritt: downPaymentAmount = 30000, purchasePrice = 350000, mortgageType = CONVENTIONAL.

Die Tatsache, dass wir LLMs einsetzen, um Ihre Eingabe in natürlicher Sprache in Logik zu übersetzen, ist der Grund dafür, dass das System eine Überprüfungsgenauigkeit von bis zu 99 Prozent angibt. Um sicherzustellen, dass unsere Übersetzung korrekt ist, verlassen wir uns nicht nur auf ein einziges LLM. Stattdessen setzen wir mehrere LLMs mit unterschiedlichen „Temperaturen“ parallel ein, um dieselbe Übersetzung durchzuführen. Erst wenn die redundanten Übersetzungen semantisch äquivalent sind, können wir ein Validierungsergebnis ausgeben. Stimmen die Übersetzungen nicht überein, geben wir stattdessen ein MEHRDEUTIGES Ergebnis zurück, das 2 mögliche Interpretationen der Eingabe enthält. Ihr LLM kann dieses Feedback nutzen, um seine Antwort zu präzisieren oder dem Benutzer klärende Fragen zu stellen. Als wir unser System mit dem bedingten QA-Datensatz der Carnegie Mellon verglichen haben, war in über 99 Prozent der Fälle, in denen eine Antwort von unserem System als GÜLTIG gekennzeichnet wurde, diese Kennzeichnung korrekt. Weitere Informationen zur Methodik finden Sie in diesem Artikel.

Schritt 2: Überprüfung

Ein Satisfiability Modulo Theories (SMT)-Solver bewertet, ob die übersetzten Aufgaben alle Ihre Richtlinienregeln erfüllen. Dieser Schritt ist per Definition mathematisch fundiert. Sobald die Übersetzung korrekt ist, ist die Überprüfung nachweislich korrekt.

Für das Hypothekenbeispiel: Der Solver berechnet downPaymentPercentage = (30 000 / 350 000) * 100 = 8,57 Prozent, vergleicht dies mit der Regel (=> (< downPaymentPercentage 20,0) (not (= mortgageType CONVENTIONAL)))), stellt fest, dass 8,57 < 20 ist, und kommt zu dem Schluss, dass mortgageType = CONVENTIONAL logisch ungültig ist. Das System gibt eine ungültige Erkenntnis mit einer vollständigen Rückverfolgung zurück, die genau zeigt, gegen welche Regel verstoßen wurde und warum.

Was bedeutet das konkret für Gründer von Startups? Die Übersetzungsqualität können Sie durch bessere Variablenbeschreibungen selbst steuern. Um die mathematische Überprüfung müssen Sie sich keine Gedanken machen. Sie investieren in eine gute Beschreibung Ihrer Domain, und der Solver kümmert sich um den Rest.

Was bedeuten die Erkenntnisse?

AR-Prüfungen geben nicht einfach „bestanden“ oder „nicht bestanden“ zurück. Sie liefern strukturierte Erkenntnisse, die Ihnen genau sagen, was passiert ist und was als Nächstes zu tun ist. Bei jeder Erkenntnis handelt es sich um einen dieser Typen:

Das ist wichtig: AR-Prüfungen werden im Erkennungsmodus ausgeführt. Sie geben Erkenntnisse und Feedback zurück, blockieren jedoch nicht die Antwort. Ihre Anwendung prüft die Erkenntnisse und entscheidet, was zu tun ist: bereitstellen, umschreiben, um Klarstellung bitten oder auf eine sichere Standardeinstellung zurückgreifen. Dadurch haben Sie die volle Kontrolle über das Benutzererlebnis und erhalten gleichzeitig eine mathematische Überprüfung jeder Antwort. Ein funktionierendes Beispiel für dieses Muster finden Sie in der Open-Source-Implementierung eines umschreibenden Chatbots, die zeigt, wie AR-Erkenntnisse zur automatischen Korrektur an das LLM zurückgesendet werden.

AgentCore-Policy: Deterministische Grenzen für KI-Agenten

Wenn Ihr Startup agentenbasierte Anwendungen entwickelt, bei denen Ihre KI mehrstufige Workflows orchestriert, Tools aufruft und Aktionen im Namen von Benutzern ergreift, haben Sie ein anderes Vertrauensproblem. Es geht nicht nur darum, was die KI sagt. Es geht darum, was die KI tut.

Für Startups aus den Bereichen Gesundheitswesen, Fintech oder Recht ist „der Agent hat etwas Unerwartetes getan“ aus Compliance- oder regulatorischer Sicht nicht akzeptabel. Sie benötigen nachweisbare Grenzen für das Verhalten der Agenten, und diese Grenzen müssen auch dann gelten, wenn der Agent durch eine Promptinjektion manipuliert wird oder einen Reasoning-Fehler macht.

Policy in Amazon Bedrock AgentCore löst dieses Problem mit einer Autorisierungsebene, die bei jeder Interaktion zwischen Agent und Tool an der Gateway-Grenze durchgesetzt wird. Die Richtlinien sind in Cedar geschrieben, der Autorisierungssprache, die von AWS für die Überprüfung mit AR entwickelt wurde. Cedar-Richtlinien definieren, wer (Prinzipal) was (Aktion) auf welcher Ressource unter welchen Bedingungen ausführen kann. Kein Tool-Aufruf durchläuft das Gateway ohne eine entsprechende Genehmigung. Sie können Richtlinien direkt in Cedar schreiben oder Ihre Regeln in natürlicher Sprache beschreiben und das System Cedar für Sie generieren lassen.

Bevor Ihre Richtlinien implementiert werden, führt Automated Reasoning eine semantische Validierung durch, um Probleme zu erkennen, darunter:

• Übermäßig permissive Richtlinien, die alle Anfragen für eine bestimmte Kombination aus Prinzipal, Aktion und Ressource zulassen würden
• Übermäßig restriktive Richtlinien, die alles verweigern würden
• Unwirksame Richtlinien, bei denen eine Genehmigung nichts erlaubt oder ein Verbot nichts verbietet

Die Durchsetzung folgt 2 Prinzipien, die für Startups in regulierten Branchen besonders wichtig sind:

1. Standard-Verweigerung: Wenn eine Richtlinie eine Aktion nicht ausdrücklich erlaubt, wird sie blockiert. Ihr Agent kann nichts tun, was Sie nicht autorisiert haben.
2. Verbot hat immer Vorrang vor Erlaubnis: Sie können feste Regeln festlegen, die nicht außer Kraft gesetzt werden können, unabhängig davon, welche anderen Richtlinien bestehen.

Nehmen wir als Beispiel ein Startup im Gesundheitswesen, das einen Terminplanungs-Agenten entwickelt. Mit AgentCore Policy können Sie durchsetzen, dass Patienten nur auf ihre eigenen Daten zugreifen, dass Terminbuchungen auf die Geschäftszeiten beschränkt sind und dass Rückerstattungsbeträge durch Richtlinien begrenzt werden. Diese Regeln gelten unabhängig davon, wie der Agent dazu aufgefordert wird, ob in Ihrem Code Fehler vorhanden sind oder wie kreativ der Benutzer bei seinen Anfragen wird. Die Durchsetzung erfolgt an der Gateway-Grenze, vollständig außerhalb des Agenten.

Wie viel kostet Automated Reasoning im Vergleich zu manueller Qualitätssicherung?

Um die Wirtschaftlichkeit von Automated Reasoning zu verstehen, ist es hilfreich, es mit dem Referenzszenario zu vergleichen, das die meisten Teams derzeit anwenden: die manuelle Qualitätssicherung der Modellausgaben.

Der alte Weg: Manuelle Qualitätssicherung

Ein Prüfer, der die KI-Ergebnisse überprüft, kann ungefähr 50 Interaktionen pro Stunde verarbeiten, was einem Gesamtpreis von etwa 40 USD pro Stunde entspricht. Für ein Startup, das monatlich 100 000 Kundeninteraktionen abwickelt, kostet die Überprüfung jeder Interaktion 80 000 USD pro Monat. Selbst eine Stichprobe von 10 Prozent kostet 8 000 USD pro Monat, und bei den anderen 90 Prozent sind Sie noch nicht verifiziert. Bei einem jährlichen Preis von 80 000 bis 150 000 USD pro Prüfer kostet ein Team von 5 bis 10 Prüfern 400 000 bis 1,5 Mio. USD pro Jahr. Für die meisten Startups ist das ein erheblicher Teil der Mittel, die dafür ausgegeben werden, zu überprüfen, ob Ihre KI korrekt ist.

Der neue Weg: Automated Reasoning

AR-Überprüfungen werden pro Validierungsanfrage berechnet. (Die genauen Preise sollten auf der Bedrock-Preisseite bestätigt werden, da die Preise variieren können.) Im Gegensatz zur manuellen Überprüfung kann jede Interaktion überprüft werden, anstatt nur Stichproben zu ziehen. Amazon-Bedrock-Integritätsschutz verwendet Texteinheiten als Validierungseinheit, wobei jede Texteinheit 1 000 Zeichen umfasst. So sieht das für ein typisches Startup aus:

Annahmen

Preisberechnung

Anhand des obigen Beispiels eines Startups, das 100 000 Interaktionen pro Monat verarbeitet, und unter der Annahme, dass die Ausgabe jeder Interaktion ~200 Token beträgt, können wir die Kosten für die Verwendung von AR-Überprüfungen zur Validierung leicht abschätzen. Amazon-Bedrock-Integritätsschutz misst die Nutzung in Texteinheiten, wobei eine Texteinheit 1 000 Zeichen umfasst. Bei einem Durchschnitt von 4 Zeichen pro Token schätzen wir jede Interaktion auf ~800 Zeichen und somit auf 0,8 Texteinheiten.

Die Validierung von 100 000 Interaktionen mit jeweils 0,8 Texteinheiten ergibt insgesamt 80 000 Texteinheiten pro Monat. Bei einem Preis von 0,17 USD pro 1 000 Texteinheiten durch AR würden sich unsere monatlichen Gesamtkosten für eine einzelne Richtlinie auf 13,60 USD belaufen. Wenn mehrere Richtlinien angewendet werden, skalieren die Kosten linear. Selbst bei mehreren Richtlinien bleiben die Gesamtkosten deutlich niedriger als bei einer manuellen Überprüfung.

Die Compliance-Mathematik ist noch überzeugender. Eine einzelne Kategorie von HIPAA-Verstößen kann nach aktuellen inflationsbereinigten Zahlen bis zu 2 067 813 USD pro Jahr kosten. Für ein Startup im Gesundheitswesen, dessen KI täglich Tausende von Patienteninteraktionen verarbeitet, ist das regulatorische Risiko durch nicht verifizierte Ergebnisse existenziell. In diesem Zusammenhang fungiert AR weniger als Software-Kostenfaktor, sondern vielmehr als Kontrollinstrument im Risikomanagement.

Für Entwickler ist der Borrow Checker von Rust die beste Analogie. Rust erkennt Speicherfehler bei der Kompilierung, bevor der Code die Produktion erreicht. AR erkennt Richtlinienverstöße zum Zeitpunkt der Überprüfung, bevor sie Ihren Kunden erreichen. Fehler zu erkennen, bevor sie Schaden anrichten, ist immer kostengünstiger, als sie im Nachhinein zu beheben.

Dabei gibt es einen Kompromiss: Die AR-Validierung erhöht die Latenz für jede Antwort, und das Umschreiben bedeutet, dass Ihr LLM bei markierten Ausgaben zweimal ausgeführt wird. Für die meisten Anwendungen sind diese Kosten jedoch neben den betrieblichen, rechtlichen oder rufschädigenden Auswirkungen einer falschen Ausgabe gering.

Das gleiche Argument findet bei Anlegern Anklang. Die Möglichkeit, sagen zu können, dass KI-Ausgaben systematisch anhand formeller Unternehmensrichtlinien überprüft werden, ist nicht einfach ein Produktmerkmal. Es ist ein Beweis dafür, dass Risiken proaktiv gemanagt werden. Das ist die Art von konkreter, überprüfbarer Behauptung, die das Risikoprofil eines Startups stärkt.

Was kommt als Nächstes?

Im 3. Teil: „Ein Schritt-für-Schritt-Playbook für die Implementierung“ befassen wir uns nach Vorstellung der Konzepte näher mit dem Code. Sie erfahren, wie Sie aus den vorhandenen Dokumenten eine Automated-Reasoning-Richtlinie erstellen, die Richtlinie im Integritätsschutz bereitstellen, sie in die ApplyGuardRail-API integrieren, Ergebnisse programmgesteuert verarbeiten, AgentCore Policy über AgentCore Gateway einrichten und einen Audit Trail erstellen. Es werden alle Punkte behandelt, die Sie benötigen, um von der Lektüre über die mathematische Verifizierung zur Auslieferung an die Produktion zu gelangen.