Können mathematische Beweise und formale Verifizierung helfen, die Sicherheit und Kontrollierbarkeit fortgeschrittener KI-Systeme zu gewährleisten?
Max Tegmark und Steve Omohundro skizzieren in ihrem neuen Papier einen möglichen Weg, um die sichere Entwicklung fortgeschrittener künstlicher Intelligenz, einschließlich allgemeiner künstlicher Intelligenz (AGI), zu gewährleisten.
Tegmark ist Physiker, Kosmologe und KI-Forscher und als Präsident des Future of Life Institute einer der Initiatoren des offenen Briefes, der im März eine mindestens sechsmonatige Pause in der KI-Entwicklung forderte. Omohundro ist ebenfalls Physiker und KI-Forscher sowie Gründer und CEO von Beneficial AI Research, einem Start-up, das nützliche und sichere KI entwickeln möchte.
Die zentrale Idee des Papiers ist es, KI-Systeme so zu gestalten, dass kritische Verhaltensweisen nachweisbar konform mit formalen mathematischen Spezifikationen sind, die menschliche Werte und Präferenzen kodieren. Dies würde KI-Systeme dazu zwingen, nur solche Handlungen auszuführen, die mathematisch nachweisbar sicher und für den Menschen vorteilhaft sind - denn bei jedem Schritt müssten sie einen mathematischen Sicherheitsnachweis erbringen, der überprüft werden könnte, bevor eine Handlung zugelassen wird.
Die Autoren argumentieren, dass aktuelle Ansätze, die sich auf die Ausrichtung von KI-Zielen an menschlichen Werten konzentrieren, allein keinen Schutz vor missbräuchlicher KI bieten. Stattdessen sei ein Sicherheitsdenken erforderlich, das die Sicherheit "sowohl in die AGI als auch in die physische, digitale und soziale Infrastruktur, mit der sie interagiert, einbaut".
Software- und Hardware-Überprüfung als Sicherheitsnetz
Der Vorschlag besteht aus mehreren Komponenten:
- Provably compliant system (PCS): System, das nachweislich bestimmte formale Spezifikationen erfüllt.
- Provably compliant hardware (PCH): Spezialisierte Hardware, die nachweislich bestimmte formale Spezifikationen erfüllt.
- Proof-carrying code (PCC): Software, die bei Bedarf den Nachweis erbringt, dass sie bestimmte formale Spezifikationen erfüllt.
- Provable contract (PC): Sichere Hardware, die Aktionen kontrolliert, indem sie die Einhaltung der formalen Spezifikation überprüft.
- Provable meta-contract (PMC): Sichere Hardware, die die Erstellung und Aktualisierung anderer PCs kontrolliert.
Gemeinsam würden diese Bausteine, es unmöglich machen, dass KI-Systeme wichtige Sicherheitseigenschaften verletzen. Die Beweise würden die Konformität sogar für superintelligente KI garantieren, so die Forscher. Statt einzigen KI-Modells, das hoffentlich unsere Anforderungen erfüllt, setzt die Methode ihre Hoffnung auf ein aufeinander aufbauendes Sicherheitsnetz an, bei dem in jedem Schritt Nachweise erbracht werden müssen.
Existenzielle Risiken sollen in jedem Schritt aufgehalten werden
Die Autoren greifen ein konkretes Bioterrorismus-Szenario aus einer Forschungsarbeit zu den vier Kategorien katastrophaler KI-Risiken auf, um zu veranschaulichen, wie ihr Ansatz angewendet werden könnte:
Eine Terrorgruppe will KI einsetzen, um ein tödliches Virus über einem dicht besiedelten Gebiet freizusetzen. Sie verwendet KI, um die DNA und die Hülle eines Erregers sowie die Schritte zur Herstellung zu entwerfen. Sie beauftragt ein Chemielabor, die DNA zu synthetisieren und in die Proteinhülle einzubauen. KI-gesteuerte Drohnen werden eingesetzt, um das Virus zu verbreiten, und KI in sozialen Medien, um ihre Botschaft nach dem Angriff zu verbreiten.
Mit dem vorgeschlagenen Ansatz für beweisbar sichere Systeme könnte ein solcher Angriff in jeder Phase verhindert werden: Biochemische Design-KIs würden keine gefährlichen Designs synthetisieren, GPUs würden keine unsicheren KI-Programme ausführen, Chipfabriken würden keine GPUs ohne Sicherheitschecks verkaufen, DNA-Synthesemaschinen würden nicht ohne Sicherheitsnachweis arbeiten, Drohnenkontrollsysteme würden keine Drohnenflüge ohne Sicherheitsnachweis erlauben und Social Bots keine Medien manipulieren.
Forscher sehen technische Hürden, erwarten jedoch Fortschritte
Die Autoren räumen ein, dass die vollständige Realisierung dieser Vision die Überwindung erheblicher technischer Hürden erfordert. Maschinelles Lernen wäre wahrscheinlich erforderlich, um die Entdeckung konformer Algorithmen und die entsprechenden Beweise zu automatisieren. Die jüngsten Fortschritte der maschinellen Lernverfahren beim automatisierten Beweisen von Theoremen geben Anlass zu Optimismus hinsichtlich rascher Fortschritte, so die Forscher.
Aber auch abseits von Überlegungen, wie man beispielsweise "die Menschheit nicht aussterben lassen" formal spezifizieren kann, gäbe es noch eine ganze Reihe ungelöster, aber einfacher und sehr gut spezifizierter Herausforderungen, deren Lösung bereits mittelfristig große Vorteile für Cybersicherheit, Blockchain, Datenschutz und kritische Infrastrukturen bringen würde.
