KI-Sicherheit: Amazon investiert in Lean

Förderung der Lean-Entwicklung

Amazon hat eine langfristige, umfangreiche finanzielle Förderung der Lean Focused Research Organization (FRO) angekündigt. Die Non-Profit-Organisation wurde 2023 unter dem Dach von Convergent Research gegründet. Convergent Research ist eine noch relativ junge US-amerikanische Non-Profit-Organisation, die ein neues Modell für wissenschaftliche Forschung etablieren möchte. Sogenannte Focused Research Organizations (FROs) sollen eine Lücke zwischen klassischen Forschungseinrichtungen, Unternehmen und Start-ups schließen. Das Ziel ist, klar definierte technische Themen über einen begrenzten Zeitraum zu fördern und die Ergebnisse der Allgemeinheit zur Verfügung zu stellen.

Im Falle von Lean lautet der Plan, dessen Entwicklung über einen Zeitraum von fünf Jahren gezielt weiterzuentwickeln und anschließend in eine langfristig selbsttragende Stiftung oder Organisation zu überführen. Gründer und Chief Architect der Lean FRO sowie gleichzeitig Senior Principal Applied Scientist bei Amazon Web Services (AWS) ist Leonardo de Moura. Co-Gründer und Head of Engineering von Lean FRO ist der am Karlsruhe Institute of Technology (KIT) promovierte Sebastian Ullrich, der seit drei Jahren hauptamtlich von München aus für die Organisation arbeitet.

Einsatzgebiete von Lean

Lean ist keine Mainstream-Programmiersprache. Jedoch gewinnt die Sprache für Forschende und Unternehmen, die etwa in der Kryptographie oder bei sicherheitskritischer Software höchste Anforderungen an Korrektheit stellen, an Bedeutung. Daher hat Lean bereits eine lebendige Community in Mathematik, Informatik, Physik und weiteren Fachbereichen hervorgebracht.

Eine wahrscheinlich noch bedeutendere Rolle kann Lean im Zusammenhang mit künstlicher Intelligenz und hier bei agentischer KI spielen. Lean lässt sich beispielsweise nutzen, um KI-generierte Workflows, Vertragslogiken oder sicherheitskritische Entscheidungen formal zu überprüfen, bevor sie produktiv eingesetzt werden. Das Ziel von Lean FRO ist es, mathematische Beweisführung für Entwickler weltweit zugänglich zu machen und damit KI-Agenten, die zunehmend folgenreiche Entscheidungen treffen, überprüfbar sicher zu gestalten.

Da KI-Agenten immer häufiger Zahlungen auslösen, Anträge bearbeiten oder Infrastruktur steuern, reichen klassische Softwaretests allein nicht mehr aus: Sie prüfen nur die Fälle, die man zuvor bedacht hat. Mathematische Beweisführung wie mit Lean zeigt dagegen mit absoluter Sicherheit, dass sich ein System, unabhängig von der Eingabe, nicht falsch verhalten kann.

Verwendung von Lean bei AWS

AWS hat Lean bereits produktiv im Einsatz: So wird Lean genutzt, um Policies für KI-Agenten in Amazon Bedrock AgentCore formal zu verifizieren. Dabei handelt es sich nicht um einfache Richtlinien, sondern um technisch definierte Regeln, die festlegen, welche Aktionen ein KI-Agent ausführen darf. So lässt sich mathematisch nachweisen, dass ein Agent bestimmte Grenzen nicht überschreitet.

Außerdem habe ein Wissenschaftler kürzlich mithilfe eines LLM in Kombination mit Lean die Korrektheit des Segment-Reparaturprotokolls von Amazon Aurora bewiesen. Der Beweis gelang laut Unternehmensangaben in einem Bruchteil der Zeit, die eine manuelle Prüfung benötigt hätte.

Die Rolle von AWS

Mit der langfristigen Finanzierung und der Doppelrolle von Lean-Erfinder Leonardo de Moura als AWS-Forscher und Chief Architect der Lean FRO vertieft Amazon seine Verbindung zum Lean-Ökosystem erheblich. Gleichzeitig betont das Unternehmen ausdrücklich, dass die Weiterentwicklung von Lean weiterhin in einer unabhängigen, community-geführten Organisation erfolgen soll, um Transparenz und Vertrauen in die Verifikationstechnologie zu gewährleisten.