Amazon investiert langfristig in die Lean Focused Research Organization (FRO), die hinter der Programmiersprache Lean steht. Ziel ist es, mathematische Beweisführung für Entwickler leichter zugänglich zu machen. Damit sollen KI-Agenten, die zunehmend eigenständig Entscheidungen treffen, nachweisbar innerhalb definierter Regeln arbeiten.

Grafik: Lean Focused Research Organization (FRO)

Künstliche Intelligenz entwickelt sich zunehmend von einem Assistenzwerkzeug zu autonomen Systemen, die Zahlungen auslösen, Anträge bearbeiten oder kritische Infrastrukturen steuern. Damit steigen auch die Anforderungen an ihre Sicherheit. Nach Einschätzung von Amazon reichen klassische Softwaretests in solchen Szenarien allein nicht mehr aus. Sie überprüfen lediglich jene Fälle, die Entwickler zuvor definiert haben. Mathematische Beweise verfolgen einen anderen Ansatz: Sie sollen nachweisen, dass sich ein System unabhängig von den Eingaben nicht außerhalb seiner vorgegebenen Regeln verhält. Vor diesem Hintergrund kündigt Amazon eine langfristige und umfangreiche finanzielle Förderung der Lean Focused Research Organization (FRO) an. Die gemeinnützige Organisation entwickelt die Programmiersprache Lean weiter und erhält damit nach Angaben des Unternehmens die bislang größte Einzelspende ihrer Geschichte.

Lean soll formale Verifizierung für Entwickler zugänglich machen

Lean wird bereits heute in Mathematik, Informatik, Physik und weiteren wissenschaftlichen Disziplinen eingesetzt. Zudem bildet die Sprache die Grundlage von Mathlib, einer umfassenden Bibliothek formalisierter Mathematik, die die Entwicklung mathematischer Beweise erleichtert. Nach Angaben von Amazon spielt Lean inzwischen auch in der KI-Forschung eine wichtige Rolle. KI-generierte Beweise in Lean werden genutzt, um Modelle mit geringeren Fehlerraten zu trainieren und ermöglichen inzwischen korrekte Lösungen für Probleme auf Forschungsniveau.

Auch innerhalb von AWS kommt Lean bereits produktiv zum Einsatz. Policy in Amazon Bedrock AgentCore nutzt Lean-basierte Verifizierung, um mathematisch nachzuweisen, dass KI-Agenten innerhalb definierter Richtlinien und Berechtigungen bleiben. Darüber hinaus bildet Lean die Grundlage für Genauigkeitsnachweise von SampCert sowie des KI-Chip-Compilers AWS Neuron. Amazon verweist zudem auf ein Forschungsprojekt, bei dem ein Wissenschaftler mithilfe eines Large Language Models in Kombination mit Lean die Korrektheit des Segment-Reparaturprotokolls von Amazon Aurora in einem Bruchteil der Zeit nachweisen konnte, die für eine manuelle formale Prüfung erforderlich gewesen wäre.

Transparenz als Voraussetzung für vertrauenswürdige KI

Bemerkenswert ist nach Angaben des Unternehmens auch die Organisationsform der Initiative. Amazon entwickelt Lean nicht selbst weiter, sondern unterstützt bewusst die unabhängige, community-geführte Lean Focused Research Organization. Dadurch sollen Kunden, Auditoren und Regulierungsbehörden die zugrunde liegenden Werkzeuge unabhängig überprüfen können. Nach Auffassung des Unternehmens schafft gerade diese Offenheit die Grundlage für Vertrauen in sicherheitskritische KI-Anwendungen.

Amazon sieht in der Verbindung generativer KI mit der mathematischen Strenge von Lean einen wichtigen Baustein für sogenannte agentische Sicherheit und neurosymbolische KI. Ziel ist es, autonome KI-Agenten nicht nur leistungsfähiger, sondern auch nachvollziehbar und überprüfbar zu machen. Mit der langfristigen Förderung der Lean FRO will das Unternehmen dazu beitragen, formale Verifizierung künftig einem deutlich größeren Kreis von Entwicklern zugänglich zu machen und den Einsatz mathematischer Beweise in modernen Software- und KI-Systemen zu beschleunigen.

Den vollständigen englischsprachigen Blogbeitrag stellt Amazon Science auf seiner Website bereit.