Nachweis, 1. Teil: Warum „wahrscheinlich richtig“ für KI-Startups nicht gut genug ist

Maßgeblich für Startups, die im Zeitalter der KI erfolgreich sein wollen, sind nicht die modernsten Modelle oder die größten Trainingsdatensätze, sondern das Vertrauen. Der entscheidende Unterschied liegt darin, ob die Benutzer ihnen vertrauen und ob sie die Frage, was bei Fehlern der KI geschieht, nicht nur mit einer probabilistischen Zusicherung, sondern mit mathematischer Gewissheit beantworten können. In regulierten Märkten gewinnt die Verifizierbarkeit zunehmend an Bedeutung. Sie ist mittlerweile wichtiger als die reine Leistungsfähigkeit der Modelle.

Sie haben gerade Ihre Seed-Finanzierungsrunde abgeschlossen. Ihr KI-gestützter Kreditassistent ist letzte Woche mit 200 Beta-Benutzern online gegangen. Am dritten Tag macht eine Kundin einen Screenshot Ihres Chatbots, wonach sie die Voraussetzungen für eine herkömmliche Hypothek mit 8 Prozent Anzahlung erfüllt. Sie veröffentlicht diesen Screenshot in den sozialen Medien. Ihre Richtlinien sehen jedoch eine Anzahlung in Höhe von 20 Prozent vor.

Ihr Mitbegründer sieht es zuerst, Ihr Investor als Zweiter und Ihr Rechtsberater als Dritter.

Das ist kein hypothetischer Fall, sondern die Realität bei der Entwicklung von KI-Produkten im Jahr 2026. Dreiköpfige Teams bringen Produkte auf den Markt, für die vor zwei Jahren noch 50 Ingenieure nötig gewesen wären. Dabei vergehen von der Idee bis zum Minimum Viable Product (MVP) nur wenige Tage statt mehrere Monate.

Doch Tempo allein ohne entsprechende Verifizierung birgt Risiken. Die generative KI hat es trivial und gefährlich einfach gemacht, etwas herauszubringen, das Halluzinationen erzeugt, den eigenen Richtlinien widerspricht oder den Kunden nachweislich falsche Antworten gibt. Die Veröffentlichung von Lösungen, die nicht vertrauenswürdig sind, lässt Startups scheitern.

Die Ursache dafür ist struktureller Natur. Große Sprachmodelle (LLMs) sind stochastische Systeme. Sie generieren Text, indem sie das nächste wahrscheinliche Token vorhersagen. Dieser Prozess ist von Natur aus mit Zufälligkeit verbunden: Temperatur, Stichprobenstrategien und Top-k/Top-p-Parameter führen allesamt zu Variabilität. Der gleiche Prompt kann bei unterschiedlichen Durchläufen verschiedene Antworten hervorbringen. Das macht LLMs kreativ und nützlich, aber auch grundsätzlich unzuverlässig für Aufgaben, die Korrektheit erfordern. Ihr Modell hat nicht versucht, schlechte Hypothekenratschläge zu geben, sondern einfach nur den wahrscheinlichsten nächsten Token vorhergesagt.

Jedes KI-Startup muss diesen Spagat schaffen: Wie entwickelt man Lösungen auf Grundlage von probabilistischen Systemen und liefert zugleich Korrektheitsgarantien für Kunden, Aufsichtsbehörden und Investoren?

Was geschieht, wenn KI die falsche Antwort gibt?

Wenn Ihre KI falsche Anweisungen gibt und ein Kunde danach handelt, tragen Sie die Verantwortung für das Ergebnis. Trifft Ihre für das Gesundheitswesen entwickelte KI bei einigen hundert Interaktionen mit Patienten eine falsche Entscheidung zur Kostenübernahme, liegen die zivilrechtlichen Strafen gemäß HIPAA je nach Schweregrad zwischen 137 und 68 928 USD pro Verstoß. Die jährlichen Obergrenzen liegen nach den neuesten inflationsbereinigten Zahlen bei 2 067 813 USD pro Verstoßkategorie. Die Bußgelder können Ihr Gesamtbudget übersteigen, bevor Sie überhaupt bemerken, dass ein Problem vorliegt. Nach der DSGVO können Bußgelder für schwerwiegende Verstöße bis zu 20 Millionen EUR oder 4 Prozent des weltweiten Jahresumsatzes betragen (je nachdem, welcher Betrag höher ist). Für ein junges Startup, das Daten von Kunden aus der EU verarbeitet, ist das nicht nur eine Geldstrafe, sondern das Aus. Ein Fintech-Chatbot, der einem nicht berechtigten Antragsteller einen Kredit bewilligt, verursacht eine regulatorische Haftung. Ein Versicherungsbot, der Versicherungsbedingungen falsch wiedergibt, führt zu einem Vertragsstreit, den Sie nur verlieren können.

Und neben den direkten Strafen entstehen Folgekosten: der Unternehmensdeal, der scheitert, weil Sie die Sicherheitsüberprüfung nicht bestehen, das SOC-2-Audit, das ins Stocken gerät, weil Sie nicht erklären können, wie Ihre KI Entscheidungen trifft, und der Series-A-Investor, der abspringt, weil er auf die Frage, was geschieht, wenn die KI falsch liegt, keine zufriedenstellende Antwort erhält.

Warum Prompt-Engineering und RAG nicht ausreichen

Jedes Startup, das mithilfe von LLMs Lösungen entwickelt, hat eine Variante des gleichen Sicherheits-Stacks: sorgfältiges Prompt-Engineering, Retrieval-Augmented Generation (RAG) und ein gewisses Maß an manueller Überprüfung. Das sind bewährte Vorgehensweisen, die aber bei Weitem nicht ausreichen.

Das Prompt-Engineering ist heuristisch und nicht beweisbar. Sie erstellen Anweisungen, die das Modell zum korrekten Verhalten bewegen sollen, doch es gibt keine Garantie dafür, dass das Modell ihnen auch folgt. Wenn Sie ein Upgrade auf eine neuere Modellversion durchführen oder den System-Prompt zur Verarbeitung eines neuen Grenzfalls anpassen, kann ein zuvor sicheres Verhalten unbemerkt versagen. Die Sicherheit wird auf informellen Vereinbarungen ohne Durchsetzungsmechanismus aufgebaut.

RAG verringert die Wahrscheinlichkeit von Halluzinationen, da dem Modell abgerufene Dokumente zugrunde gelegt werden. Das stellt eine echte Verbesserung dar. Doch das Modell kann den abgerufenen Kontext immer noch ignorieren, falsch interpretieren oder selektiv nutzen. RAG verschiebt die Wahrscheinlichkeitsverteilung in Richtung besserer Antworten, schließt die Möglichkeit falscher Antworten aber nicht aus. „Meistens richtig“ ist keine geeignete Compliance-Strategie.

Die manuelle Qualitätssicherung kann nicht parallel zum Firmenwachstum mitwachsen. Selbst bei einer aggressiven Stichprobenprüfung (von 10 Prozent der Interaktionen) bleiben 90 Prozent ungeprüft. Für ein Startup, das monatlich 100 000 Kundeninteraktionen verarbeitet, kostet die Einstellung von Prüfern zur stichprobenartigen Überprüfung der Ergebnisse jährlich Hunderttausende Euro. Das ist ein Personalbestand, über den Sie in der Seed-Phase einfach nicht verfügen. Und dabei verlassen Sie sich bei 90 Prozent der nicht geprüften Interaktionen auch noch auf das Prinzip Hoffnung. Zudem fallen diese Kosten nicht nur einmalig an. Die Art und Weise, wie die Kunden Fragen formulieren, ändert sich im Laufe der Zeit. Auch die Modelle selbst ändern sich. Zuvor zuverlässige Verhaltensweisen können nach einer routinemäßigen Modellaktualisierung an Qualität einbüßen. Sorgfältig formulierte Prompts, die im vergangenen Monat noch funktioniert haben, können im nächsten Monat unbemerkt versagen. Deshalb müssen Sie den Qualitätssicherungsprozess kontinuierlich bewerten, erneut testen und anpassen. Er ist also kein Problem, das Sie einmalig lösen können, sondern ein dauerhafter Kostenfaktor.

All diese Ansätze verringern das Risiko, ohne jedoch absolute Gewissheit zu bieten. Wenn Ihr Investor danach fragt, ob die KI falsche Ergebnisse liefern kann, dann lautet die ehrliche Antwort bei alleiniger Nutzung dieser Instrumente: „Wahrscheinlich nicht, zumindest meistens nicht.“ Mit dieser Antwort können Sie aber weder eine Series-A-Finanzierungsrunde abschließen noch eine Aufsichtsbehörde zufriedenstellen.

Was genau ist Automated Reasoning?

Das Automated Reasoning ist ein Gebiet der Informatik, das sich der mathematischen Logik bedient, um Gewissheit darüber zu erlangen, was ein System tun wird und was nicht. Im Gegensatz zum Machine Learning, bei dem aus Daten Muster erlernt werden, nutzt das Automated Reasoning mathematische Logik, Theorembeweise und Constraint-Solving, um nachzuweisen, dass bestimmte Eigenschaften im unendlichen Raum aller möglichen Eingaben stets gültig sind.

Die Differenzierung ist wichtig. Wenn ein Machine-Learning-Modell sagt, dass „diese Ausgabe mit 95-prozentiger Wahrscheinlichkeit korrekt ist“, macht es eine statistische Behauptung. Sagt ein Automated-Reasoning-System, dass „diese Ausgabe gültig ist“, hat es einen mathematischen Beweis dafür konstruiert, dass die Ausgabe alle von Ihnen definierten Einschränkungen erfüllt. Es gibt kein Konfidenzintervall. Der Beweis ist entweder vorhanden oder nicht.

Automated Reasoning ist kein Ersatz für große Sprachmodelle (LLMs). Ihr Chatbot benötigt nach wie vor ein Sprachmodell, um Kundenfragen verstehen und natürliche Antworten generieren zu können. Was das Automated Reasoning bietet, ist die darüberliegende Verifizierungsebene: LLMs generieren die Antworten, die durch das Automated Reasoning überprüft werden.

Zusammen bilden sie den kompletten Stack, in dem Kreativität und Korrektheit nebeneinander existieren. Ihre KI kann weiterhin dialogorientiert, hilfreich und schnell sein. Das Automated Reasoning stellt jedoch sicher, dass sie die von Ihnen definierten geschäftlichen und Compliance-Einschränkungen einhält.

Wie AWS Automated Reasoning einsetzt

AWS nutzt Automated Reasoning seit Jahren in der Produktion, um die Infrastruktur zu schützen, auf der Startups (und alle anderen Unternehmen) ihre Anwendungen ausführen.

• Zelkova, die Automated-Reasoning-Engine, die AWS IAM Access Analyzer zugrunde liegt, überprüft mithilfe des SMT-Lösungsverfahrens (Satisfiability Modulo Theories) mathematisch, ob Ihre Richtlinien für IAM und Amazon Simple Storage Service (Amazon S3) genau wie beabsichtigt funktionieren. Dabei erkennt die Engine unbeabsichtigte Zugriffspfade, die bei einer manuellen Überprüfung nicht erkennbar sind.
• Cedar, inzwischen ein CNCF-Sandbox-Projekt, ist die erste Sprache für Autorisierungsrichtlinien, die von Anfang an für die Verifizierung mit Automated Reasoning entwickelt wurde. Sie unterstützt Amazon Verified Permissions.
• Die Nitro Isolation Engine, der erste formal verifizierte Cloud-Hypervisor, gewährleistet die Isolierung von Mandanten für Amazon Elastic Compute Cloud (Amazon EC2) mit rund 260 000 Zeilen maschinell geprüfter Beweise.
• s2n-tls, die Open-Source-TLS-Bibliothek von AWS, verifiziert anhand von formalen Beweisen, dass ihre kryptografischen Operationen zeitgesteuerten Seitenkanalangriffen widerstehen.

Für Startup-Entwickler ist folgender Punkt entscheidend: Die mathematischen Verifizierungstechniken, die Ihnen über Amazon Bedrock und Amazon Bedrock AgentCore zur Verfügung stehen, sind keine Forschungsprototypen. Sie stammen aus derselben technischen Disziplin, mit der AWS die Beständigkeit von S3, die Isolierung von EC2 und die Sicherheit aller TLS-Verbindungen zu AWS-Services gewährleistet. Bis vor Kurzem erforderte der Zugang zu dieser Disziplin den Aufbau eines internen Teams aus promovierten Fachleuten für formale Methoden – ein Luxus, der Unternehmen mit den entsprechenden Budgets für Forschungslabore vorbehalten war. Mit Bedrock und AgentCore kann dies per API-Aufruf mit nutzungsabhängiger Bezahlung erfolgen.

Wie können Startups Automated Reasoning nutzen?

Für Startup-Teams ist diese Disziplin der mathematischen Verifizierung nun direkt über zwei Produkte verfügbar, die jeweils eine andere Ebene des KI-Vertrauensproblems behandeln.

Automated-Reasoning-Prüfungen im Amazon-Bedrock-Integritätsschutz überprüfen mithilfe einer SMT-basierten formalen Logik (der gleiche Ansatz wie bei Zelkova), ob die Ausgabe Ihres LLM Ihren Geschäftsregeln entspricht. Zunächst definieren Sie die eigenen Richtlinien: Kriterien für die Kreditvergabe, Gesundheitsprotokolle, Compliance-Regeln – was auch immer Ihr Unternehmen benötigt. Anschließend übersetzt das System diese in formale Logik und überprüft alle LLM-Antworten anhand dieser Regeln. Wenn das Modell etwas sagt, das Ihren Richtlinien widerspricht, erkennt das System dies und teilt Ihnen genau mit, welche Regel verletzt wurde und warum.

In dem am Anfang dieses Beitrags erwähnten Hypotheken-Szenario hätte das System den Fehler mit der Anzahlung von nur 8 Prozent erkannt und den richtigen Wert vorgeschlagen, damit das LLM die Antwort umformulieren kann, ehe sie die Benutzerin überhaupt erreicht.

Policy in Amazon Bedrock AgentCore nutzt Cedar (eine Open-Source-Richtliniensprache für die Autorisierung), um deterministische Grenzen für die Aktionen von KI-Agenten durchzusetzen. Wenn Sie agentenbasierte Anwendungen entwickeln, bei denen Ihre KI durch den Aufruf von Tools kritische Entscheidungen trifft – sei es der Zugriff auf sensible Daten, das Schreiben in externe Systeme oder das Ausführen von Aktionen im Namen von Benutzern –, fängt Policy alle Anfragen von Agenten an Tools an der Gateway-Grenze ab und bewertet sie vor der Ausführung anhand von Cedar-Richtlinien. Die Durchsetzung erfolgt deterministisch. Sie funktioniert unabhängig vom Reasoning des Agenten und kann nicht durch Promptinjektionen, Halluzination oder Bugs im Agentencode umgangen werden. Für Startups im Gesundheitswesen, im Fintech-Bereich oder im Rechtswesen bedeutet das, dass sie der Aufsichtsbehörde genau mitteilen können, was der eigene Agent tun kann und was nicht – gestützt auf mathematisch validierte Richtlinien.

Von den anderen Systemen im Portfolio formaler Methoden von AWS (die Nitro Isolation Engine, s2n-tls, s2n-quic, Dafny) profitieren Sie indirekt: Jede ausgeführte EC2-Instance basiert auf einer formal verifizierten Isolierung und jede TLS-Verbindung nutzt formal verifizierte Kryptografie. Über den Bedrock-Integritätsschutz und Policy in AgentCore werden formale Methoden direkt in Ihren Anwendungscode integriert.

Zwei Ebenen, ein Prinzip: formale mathematische Verifizierung anstelle von stochastischem Vertrauen.

Nächstes Thema in dieser Reihe

Dies ist der 1. Teil einer dreiteiligen Reihe. Im 2. Teil: „Formale Logik, Cedar-Richtlinien und die Wirtschaftlichkeit der Verifizierung“ gehen wir näher auf die folgenden Fragen ein: Wie funktionieren Automated-Reasoning-Richtlinien, wie werden Ihre Geschäftsregeln in formale Logik umgesetzt, wie sieht die Verifizierungspipeline aus und wie ist es um die Wirtschaftlichkeit der mathematischen Verifizierung im Vergleich zu manuellen QS-Teams bestellt? Beim 3. Teil: „Ein Schritt-für-Schritt-Playbook für die Implementierung“ handelt es sich um eine praktische Anleitung mit produktionsreifen Codemustern. Damit können Sie Automated-Reasoning-Prüfungen im Bedrock-Integritätsschutz sowie Policy in AgentCore in Ihren Stack integrieren.