Auf dem Weg zur überprüfbaren KI: Fünf Herausforderungen formaler Methoden-KI-php.cn

Künstliche Intelligenz ist ein Computersystem, das versucht, die menschliche Intelligenz zu imitieren, einschließlich einiger menschlicher Funktionen, die intuitiv mit Intelligenz verbunden sind, wie Lernen, Problemlösung sowie rationales Denken und Handeln. Im weitesten Sinne deckt der Begriff KI viele eng verwandte Bereiche wie maschinelles Lernen ab. Systeme, die KI stark nutzen, haben erhebliche soziale Auswirkungen in Bereichen wie Gesundheitswesen, Transport, Finanzen, soziale Netzwerke, E-Commerce und Bildung.

Diese wachsenden gesellschaftlichen Auswirkungen haben auch eine Reihe von Risiken und Bedenken mit sich gebracht, darunter Fehler in der Software für künstliche Intelligenz, Cyberangriffe und die Sicherheit von Systemen mit künstlicher Intelligenz. Daher hat die Frage der Verifizierung von KI-Systemen und das umfassendere Thema vertrauenswürdiger KI begonnen, die Aufmerksamkeit der Forschungsgemeinschaft auf sich zu ziehen. Als Ziel für den Entwurf von KI-Systemen wurde „überprüfbare KI“ festgelegt, ein überprüfbares KI-System mit starken und idealerweise nachweisbaren Korrektheitsgarantien für bestimmte mathematische Anforderungen. Wie können wir dieses Ziel erreichen?

Kürzlich wurde in einem Übersichtsartikel in „The Communications of ACM“ versucht, über die Herausforderungen nachzudenken, denen sich verifizierbare KI aus der Perspektive der formalen Verifizierung gegenübersieht, und einige Lösungsprinzipien vorgestellt. Die Autoren sind Professor S. Shankar Sastry und Sanjit A. Seshia, Vorsitzender der Fakultät für Elektrotechnik und Informatik an der UC Berkeley, und Dorsa Sadigh, Assistenzprofessorin für Informatik an der Stanford University.

In der Informatik und im Ingenieurwesen umfassen formale Methoden die strenge mathematische Spezifikation, den Entwurf und die Verifizierung von Systemen. Im Kern geht es bei formalen Methoden um Beweise: Formulierung von Spezifikationen, die die Beweispflichten bilden, Entwurf von Systemen zur Erfüllung dieser Pflichten und Überprüfung durch algorithmische Beweissuche, ob das System tatsächlich seinen Spezifikationen entspricht. Von spezifikationsgesteuerten Tests und Simulationen bis hin zu Modellprüfungen und Theorembeweisen werden eine Reihe formaler Methoden häufig beim computergestützten Entwurf integrierter Schaltkreise verwendet und häufig verwendet, um Fehler in Software zu finden, cyber-physikalische Systeme zu analysieren und Sicherheit zu entdecken Schwachstellen.

Dieser Artikel gibt einen Überblick über die traditionelle Anwendung formaler und identifiziert fünf einzigartige Herausforderungen formaler Methoden in KI-Systemen, darunter: #🎜 🎜#

Entwicklung von Sprachen und Algorithmen für die Umgebung
# 🎜🎜#Abstrakt und stellen komplexe ML-Komponenten und -Systeme dar 🎜# Entwicklung einer skalierbaren Computer-Engine für automatisierte Inferenz
Entwickeln Sie Algorithmen und Techniken, die für eine vertrauenswürdige Konstruktion ausgelegt sind zur Lösung der oben genannten Herausforderungen. Dieser Artikel konzentriert sich nicht nur auf eine bestimmte Art von KI-Komponente wie tiefe neuronale Netze oder eine bestimmte Methode wie Reinforcement Learning, sondern versucht, ein breiteres Spektrum von KI-Systemen und ihren Entwurfsprozessen abzudecken. Darüber hinaus sind formale Methoden nur ein Weg zu vertrauenswürdiger KI, sodass die Ideen in diesem Artikel Methoden aus anderen Bereichen ergänzen sollen. Diese Perspektiven basieren weitgehend auf Überlegungen zu den Problemen, die sich aus dem Einsatz von KI in autonomen und halbautonomen Systemen ergeben, bei denen Sicherheits- und Verifizierungsfragen eine größere Rolle spielen. Abbildung 1 zeigt die Laufzeitelastizität der formalen Verifizierung, formalen Synthese und formalen Anleitung. Der formale Verifizierungsprozess beginnt mit drei Eingaben:
Abbildung 1: für formal Methoden zur Verifizierung, Synthese und LaufzeitresilienzZu verifizierendes Systemmodell S Antwort als Ausgabe, um anzugeben, ob S erfüllt die Eigenschaft Φ in der Umgebung E. Typischerweise wird die „Nein“-Ausgabe von einem Gegenbeispiel, auch Fehlerverfolgung genannt, begleitet, bei dem es sich um eine Ausführung des Systems handelt, die zeigt, wie Φ gefälscht wurde. Einige Validierungstools enthalten auch einen Richtigkeitsnachweis oder ein Zertifikat mit einer „Ja“-Antwort. Wir betrachten formale Methoden aus einer breiten Perspektive, einschließlich aller Techniken, die einen Aspekt der formalen Spezifikation, Verifizierung oder Synthese nutzen. Wir schließen beispielsweise simulationsbasierte Hardware-Verifikationsmethoden oder modellbasierte Software-Testmethoden ein, da sie auch formale Spezifikationen oder Modelle verwenden, um den Simulations- oder Testprozess zu leiten.
1. Um eine formale Verifizierung auf ein KI-System anzuwenden, muss man in der Lage sein, mindestens die drei Eingaben S, E und Φ formal darzustellen. Idealerweise gibt es ein effizientes Entscheidungsverfahren, um die Frage mit „Ja“ zu beantworten Frage „zuvor beschrieben /Nein“. Es ist jedoch nicht trivial, selbst für drei Eingaben eine gute Darstellung zu erstellen, geschweige denn, sich mit der Komplexität der zugrunde liegenden Design- und Verifizierungsprobleme auseinanderzusetzen.
2. Hier veranschaulichen wir den Sinn dieses Artikels anhand eines Beispiels aus dem Bereich des teilautonomen Fahrens. Abbildung 2 zeigt ein anschauliches Beispiel eines KI-Systems: ein CPS mit geschlossenem Regelkreis, das ein halbautonomes Fahrzeug mit einer maschinellen Lernkomponente und seiner Umgebung umfasst. Nehmen wir insbesondere an, dass ein halbautonomes „Ego“-Fahrzeug über ein automatisches Notbremssystem (AEBS) verfügt, das versucht, vorausfahrende Objekte zu erkennen und zu klassifizieren und bei Bedarf die Bremsen zu betätigen, um eine Kollision zu vermeiden. In Abbildung 2 besteht ein AEBS aus einem Controller (autonomes Bremsen), einem gesteuerten Objekt (subsystem des gesteuerten Fahrzeugs, einschließlich anderer Teile des Autonomiestapels) und einem Sensor (Kamera) sowie einer Wahrnehmungskomponente, die DNN verwendet. AEBS wird mit der Fahrzeugumgebung kombiniert, um ein geschlossenes CPS zu bilden. Die Umgebung eines „eigenen“ Fahrzeugs umfasst Agenten und Objekte außerhalb des Fahrzeugs (andere Fahrzeuge, Fußgänger usw.) sowie innerhalb des Fahrzeugs (z. B. den Fahrer). Die Sicherheitsanforderungen eines solchen geschlossenen Kreislaufsystems können informell anhand der Eigenschaft charakterisiert werden, einen sicheren Abstand zwischen dem sich bewegenden „Ego“-Fahrzeug und jedem anderen Agenten oder Objekt auf der Straße einzuhalten. Allerdings gibt es viele Nuancen bei der Spezifikation, Modellierung und Verifizierung solcher Systeme.
Abbildung 2: Beispiel für Closed-Loop-CPS mit maschineller Lernkomponente

Erwägen Sie zunächst die Modellierung der Umgebung eines halbautonomen Fahrzeugs. Sogar Fragen wie die Anzahl und welche Agenten (sowohl menschliche als auch nichtmenschliche) in der Umwelt, ganz zu schweigen von ihren Eigenschaften und Verhaltensweisen, können mit erheblicher Unsicherheit behaftet sein. Zweitens sind Wahrnehmungsaufgaben mithilfe von KI oder ML schwer, wenn nicht gar unmöglich, zu formalisieren. Drittens können Komponenten wie DNNs komplexe, hochdimensionale Objekte sein, die auf komplexen, hochdimensionalen Eingaberäumen arbeiten. Daher ist es eine große Herausforderung, die drei Eingaben S, E, Φ des formalen Verifizierungsprozesses selbst in einer Form zu generieren, die die Verifizierung handhabbar macht.

Wenn jemand dieses Problem löst, wird es eine schwierige Aufgabe sein, ein so komplexes KI-basiertes CPS wie Abbildung 2 zu verifizieren. Bei einem solchen CPS ist ein kompositorischer (modularer) Ansatz von entscheidender Bedeutung für die Skalierbarkeit, die Implementierung kann jedoch aufgrund von Faktoren wie der Schwierigkeit der Zusammensetzungsspezifikation schwierig sein. Schließlich verspricht der Correct-by-Construction (CBC)-Ansatz eine verifizierbare KI, steckt aber noch in den Kinderschuhen und ist stark auf Fortschritte bei der Spezifikation und Verifizierung angewiesen. Abbildung 3 fasst die fünf herausfordernden Bereiche der überprüfbaren KI zusammen. Für jeden Bereich destillieren wir aktuelle erfolgsversprechende Ansätze in drei Prinzipien zur Bewältigung von Herausforderungen, dargestellt als Knotenpunkte. Kanten zwischen Knoten zeigen, welche Prinzipien überprüfbarer KI voneinander abhängen, wobei gemeinsame Abhängigkeitsstränge durch eine einzelne Farbe dargestellt werden. Diese Herausforderungen und die entsprechenden Prinzipien werden im Folgenden erläutert.

Abbildung 3: Zusammenfassung von 5 Herausforderungsbereichen für überprüfbare KI #Die Umgebung, in der KI/ML-basierte Systeme laufen, ist in der Regel komplex, wie beispielsweise die Modellierung verschiedener städtischer Verkehrsumgebungen, in denen autonome Fahrzeuge agieren. Tatsächlich wird KI/ML häufig in diese Systeme eingeführt, um mit der Komplexität und Unsicherheit der Umgebung umzugehen. Aktuelle ML-Designprozesse verwenden häufig Daten, um die Umgebung implizit zu spezifizieren. Das Ziel vieler KI-Systeme besteht im Gegensatz zu herkömmlichen Systemen, die für eine a priori festgelegte Umgebung konzipiert sind, darin, ihre Umgebung während ihres Betriebs zu entdecken und zu verstehen. Allerdings beziehen sich alle formalen Verifizierungen und Synthesen auf ein Modell der Umgebung. Daher müssen Annahmen und Eigenschaften der Eingabedaten in das Umgebungsmodell interpretiert werden. Wir destillieren diese Dichotomie in drei Herausforderungen für die Modellierung der Umgebung von KI-Systemen und entwickeln entsprechende Prinzipien, um diese Herausforderungen anzugehen.

2.1 Modellierungsunsicherheit

#🎜🎜 ## 🎜 🎜#Bei der traditionellen Verwendung der formalen Verifizierung besteht ein gängiger Ansatz darin, die Umgebung als eingeschränkten nichtdeterministischen Prozess oder „Störung“ zu modellieren. Diese „übermäßige Annäherung“ der Umweltmodellierung ermöglicht es, Umweltunsicherheiten konservativer zu erfassen, ohne übermäßig detaillierte Modelle zu benötigen, die für Schlussfolgerungen sehr ineffizient wären. Für eine KI-basierte Autonomie kann eine rein nichtdeterministische Modellierung jedoch zu viele falsche Fehlerberichte erzeugen, wodurch der Verifizierungsprozess in der Praxis unbrauchbar wird. Beispielsweise ist bei der Modellierung des Verhaltens umgebender Fahrzeuge eines autonomen Autos das Verhalten der umgebenden Fahrzeuge unterschiedlich. Wenn eine rein nichtdeterministische Modellierung angewendet wird, können Unfälle, die immer unerwartet auftreten, nicht berücksichtigt werden. Darüber hinaus machen viele KI/ML-Systeme implizit oder explizit Verteilungsannahmen über Daten oder Verhalten aus der Umgebung, was eine probabilistische Modellierung erfordert. Da es schwierig ist, die zugrunde liegende Verteilung genau zu bestimmen, kann nicht davon ausgegangen werden, dass das resultierende Wahrscheinlichkeitsmodell perfekt ist, und Unsicherheiten im Modellierungsprozess müssen im Modell selbst charakterisiert werden.

Probabilistische Modellierung. Um dieser Herausforderung zu begegnen, schlagen wir eine Form vor, die probabilistische und nichtdeterministische Modellierung kombiniert. Probabilistische Modellierung kann verwendet werden, wenn eine Wahrscheinlichkeitsverteilung zuverlässig angegeben oder geschätzt werden kann. In anderen Fällen kann nichtdeterministische Modellierung verwendet werden, um das Umweltverhalten übermäßig anzunähern. Während Formalismen wie Markov-Entscheidungsprozesse bereits eine Möglichkeit bieten, probabilistische und nichtdeterministische Ansätze zu kombinieren, glauben wir, dass umfangreichere Formalismen wie das probabilistische Programmierparadigma eine ausdrucksstärkere und prozeduralere Modellierung der Umgebung ermöglichen können. Wir gehen davon aus, dass solche probabilistischen Verfahren in vielen Fällen (teilweise) aus Daten gelernt oder synthetisiert werden müssen. An diesem Punkt muss jede Unsicherheit in den gelernten Parametern auf den Rest des Systems übertragen und im Wahrscheinlichkeitsmodell dargestellt werden. Konvexe Markov-Entscheidungsprozesse bieten beispielsweise eine Möglichkeit, Unsicherheit in erlernten Übergangswahrscheinlichkeitswerten darzustellen und Algorithmen zur Validierung und Steuerung zu erweitern, um dieser Unsicherheit Rechnung zu tragen. #🎜🎜 ## 🎜🎜 ## 🎜🎜 ## 🎜🎜 ## 🎜🎜#2.2 Unbekannte Variablen#🎜🎜 ## 🎜🎜#### 🎜🎜 ## 🎜🎜 ## 🎜🎜 ## 🎜 🎜#In traditionellen formalen Verifizierungsfeldern wie der Verifizierung von Gerätetreibern ist die Schnittstelle zwischen System S und seiner Umgebung E genau definiert, und E kann nur über diese Schnittstelle mit S interagieren. Diese Schnittstelle ist für die KI-basierte Autonomie unvollständig, da sie durch Sensor- und Wahrnehmungskomponenten bestimmt wird, die die Umgebung nur teilweise und verrauscht erfassen und nicht alle Interaktionen zwischen S und E erfassen können. Alle Variablen (Merkmale) der Umgebung sind bekannt, geschweige denn wahrgenommen. Selbst in eingeschränkten Szenarien, in denen Umgebungsvariablen bekannt sind, mangelt es deutlich an Informationen über deren Entwicklung, insbesondere zum Zeitpunkt des Entwurfs. Darüber hinaus stellt die Modellierung von Sensoren wie Lidar, die Umgebungsschnittstellen darstellen, eine erhebliche technische Herausforderung dar.
Introspektive Umgebungsmodellierung. Wir schlagen vor, dieses Problem durch die Entwicklung introspektiver Entwurfs- und Verifizierungsmethoden anzugehen, d. h. durch die Durchführung einer Introspektion im System S, um algorithmisch eine Annahme A über die Umgebung E zu identifizieren, die ausreicht, um zu garantieren, dass die Spezifikation Φ erfüllt ist. Im Idealfall muss A die schwächste dieser Annahmen sein und außerdem effizient genug sein, um zur Entwurfszeit zu generieren, zur Laufzeit auf verfügbare Sensoren und andere Informationsquellen über die Umgebung zu überwachen und die Erkennung zu erleichtern, wenn die Annahmen verletzt werden. Abhilfemaßnahmen können durchgeführt werden genommen. Wenn darüber hinaus ein menschlicher Bediener beteiligt ist, könnte man hoffen, dass A in eine verständliche Erklärung übersetzt werden kann, das heißt, S kann einem Menschen „erklären“, warum es die Spezifikation Φ möglicherweise nicht erfüllt. Die Bewältigung dieser vielfältigen Anforderungen sowie der Bedarf an guten Sensormodellen machen die Modellierung introspektiver Umgebungen zu einem sehr wichtigen Problem. Vorläufige Arbeiten zeigen, dass diese Extraktion überwachbarer Hypothesen in einfachen Fällen machbar ist, obwohl noch mehr Arbeit erforderlich ist, um sie in die Praxis umzusetzen.

2.3 Simulation menschlichen Verhaltens

Für viele KI-Systeme, wie zum Beispiel halbautonome Autos, sind menschliche Agenten ein entscheidender Teil der Umgebung und des Systems. Künstliche Modelle des Menschen sind nicht in der Lage, die Variabilität und Unsicherheit menschlichen Verhaltens angemessen zu erfassen. Andererseits können datengesteuerte Ansätze zur Modellierung menschlichen Verhaltens empfindlich auf die Aussagekraft und Datenqualität der vom ML-Modell verwendeten Merkmale reagieren. Um ein hohes Maß an Sicherheit für menschliche KI-Systeme zu erreichen, müssen wir die Einschränkungen aktueller menschlicher Modellierungstechniken angehen und Sicherheit für deren Vorhersagegenauigkeit und Konvergenz bieten.

Proaktive datengesteuerte Modellierung. Wir glauben, dass die menschliche Modellierung einen aktiven datengesteuerten Ansatz erfordert und dass die mathematisch dargestellten Modellstrukturen und -merkmale für formale Methoden geeignet sind. Ein wichtiger Teil der menschlichen Modellierung ist die Erfassung menschlicher Absichten. Wir schlagen einen dreigleisigen Ansatz vor: Definieren Sie Vorlagen oder Funktionen des Modells basierend auf Expertenwissen, verwenden Sie Offline-Lernen, um das Modell für die Verwendung zur Entwurfszeit zu vervollständigen, und lernen und aktualisieren Sie das Umgebungsmodell zur Laufzeit durch Überwachung und Interaktion mit der Umgebung. Beispielsweise wurde gezeigt, dass Daten, die in Fahrsimulatoren durch Experimente mit menschlichen Probanden gesammelt wurden, zur Erstellung von Verhaltensmodellen menschlicher Fahrer verwendet werden können, die zur Validierung und Steuerung autonomer Fahrzeuge verwendet werden können. Darüber hinaus können gegnerische Trainings- und Angriffstechniken in der Computersicherheit zum aktiven Lernen menschlicher Modelle und zur weiteren Entwicklung von Modellen für spezifische menschliche Handlungen verwendet werden, die zu unsicherem Verhalten führen. Diese Techniken können bei der Entwicklung von Verifizierungsalgorithmen für Mensch-KI-Systeme helfen.

Formale Spezifikationen

Die formale Verifizierung basiert stark auf formalen Spezifikationen – präzisen mathematischen Aussagen darüber, was ein System tun soll. Selbst in Bereichen, in denen formale Methoden beachtliche Erfolge erzielt haben, ist die Erstellung qualitativ hochwertiger formaler Spezifikationen eine Herausforderung, und insbesondere KI-Systeme stehen vor besonderen Herausforderungen.

3.1 Schwierig zu formalisierende Aufgabe

Das Wahrnehmungsmodul im AEBS-Controller in Abbildung 2 muss Objekte erkennen und klassifizieren und dadurch Fahrzeuge und Fußgänger von anderen Einheiten unterscheiden. Die Genauigkeit dieses Moduls erfordert eine formale Definition jedes Verkehrsteilnehmer- und Objekttyps, was im Sinne der klassischen formalen Methode äußerst schwierig ist. Dieses Problem besteht bei allen Implementierungen dieses Wahrnehmungsmoduls, nicht nur bei Deep-Learning-basierten Methoden. Ähnliche Probleme treten bei anderen Wahrnehmungs- und Kommunikationsaufgaben auf, beispielsweise bei der Verarbeitung natürlicher Sprache. Wie legen wir also das Präzisionsattribut für ein solches Modul fest? Was soll die Spezifikationssprache sein? Mit welchen Werkzeugen können wir Spezifikationen erstellen?

End-to-End-/Systemebene-Spezifikationen. Um die oben genannten Herausforderungen zu bewältigen, können wir dieses Problem leicht ändern. Anstatt Aufgaben, die schwer zu formalisieren sind, direkt zu spezifizieren, sollten wir uns zunächst darauf konzentrieren, das End-to-End-Verhalten eines KI-Systems genau zu spezifizieren. Aus dieser Spezifikation auf Systemebene können Einschränkungen für die Eingabe-Ausgabe-Schnittstellen von Komponenten abgeleitet werden, die schwer zu formalisieren sind. Diese Einschränkungen dienen als Spezifikation auf Komponentenebene, die für das gesamte KI-System kontextuell relevant ist. Für das AEBS-Beispiel in Abbildung 2 beinhaltet dies die Spezifikation der Eigenschaft Φ, die darin besteht, während der Bewegung einen Mindestabstand zu jedem Objekt einzuhalten, aus dem wir Einschränkungen für den DNN-Eingaberaum ableiten können, um die Semantik in der kontradiktorischen Analyse sinnvoll zu erfassen Eingaberaum.

3.2 Quantitative Spezifikationen vs. Boolesche Spezifikationen

Traditionell sind formale Spezifikationen in der Regel boolesche Spezifikationen, die ein bestimmtes Systemverhalten auf „wahr“ oder „falsch“ abbilden. In KI und ML werden Spezifikationen jedoch häufig als objektive Funktionen angegeben, die Kosten oder Belohnungen regulieren. Darüber hinaus kann es mehrere Ziele geben, von denen einige gemeinsam erreicht werden müssen, während andere unter bestimmten Umständen Kompromisse gegeneinander erfordern. Wie lassen sich die beiden normativen Ansätze, der boolesche und der quantitative, am besten vereinen? Gibt es einen Formalismus, der gemeinsame Eigenschaften von KI-Komponenten wie Robustheit und Fairness einheitlich erfasst?

Mischen Sie quantitative und boolesche Spezifikationen. Sowohl boolesche als auch quantitative Spezifikationen haben ihre Vorteile: Boolesche Spezifikationen sind einfacher zu erstellen, aber objektive Funktionen erleichtern die Validierung und Synthese mit optimierungsbasierten Techniken und definieren eine feinere Granularität der Eigenschaftszufriedenheit. Eine Möglichkeit, diese Lücke zu schließen, besteht darin, auf quantitative Spezifikationssprachen umzusteigen, beispielsweise die Verwendung von Logik mit boolescher und quantitativer Semantik (wie metrische zeitliche Logik) oder die Kombination von Automaten mit Belohnungsfunktionen für RL. Ein anderer Ansatz besteht darin, boolesche und quantitative Spezifikationen in einer gemeinsamen Spezifikationsstruktur zu kombinieren, beispielsweise einem Regelwerk, in dem Spezifikationen in einer hierarchischen Struktur organisiert, verglichen und zusammengefasst werden können. Die Forschung hat mehrere Kategorien von Eigenschaften von KI-Systemen identifiziert, darunter Robustheit, Fairness, Datenschutz, Verantwortlichkeit und Transparenz. Forscher schlagen neue Formalismen vor, die Ideen aus formalen Methoden und ML verknüpfen, um Variationen dieser Eigenschaften wie semantische Robustheit zu modellieren.

3.3 Daten vs. formale Anforderungen

Die Sichtweise „Daten sind Spezifikation“ ist beim maschinellen Lernen sehr verbreitet. Gekennzeichnete „echte“ Daten zu einem begrenzten Satz von Eingaben sind oft die einzige Spezifikation für korrektes Verhalten. Dies unterscheidet sich stark von formalen Methoden, die normalerweise in Form von Logik oder Automaten vorliegen und den Satz korrekter Verhaltensweisen definieren, die alle möglichen Eingaben durchlaufen. Die Kluft zwischen Daten und Normen ist bemerkenswert, insbesondere wenn die Daten begrenzt oder voreingenommen sind oder von Nicht-Experten stammen. Wir benötigen Techniken zur Formalisierung der Eigenschaften von Daten, sowohl von Daten, die zur Entwurfszeit verfügbar sind, als auch von Daten, die noch nicht vorhanden sind.

Spezifikations-Mining. Um die Lücke zwischen Daten und formalen Spezifikationen zu schließen, schlagen wir den Einsatz von Algorithmen vor, um Spezifikationen aus Daten und anderen Beobachtungen abzuleiten – sogenannte Specification-Mining-Techniken. Ein solcher Ansatz kann häufig für ML-Komponenten, einschließlich Wahrnehmungskomponenten, verwendet werden, da in vielen Fällen keine genaue Spezifikation oder eine für den Menschen lesbare Spezifikation erforderlich ist. Wir können auch Norm-Mining-Methoden verwenden, um aus Demonstrationen oder komplexeren Formen der Interaktion zwischen mehreren Agenten (Mensch und KI) auf menschliche Absichten und andere Eigenschaften zu schließen.

Modellierung lernender Systeme

In den meisten traditionellen Anwendungen der formalen Verifizierung ist das System S zum Zeitpunkt des Entwurfs festgelegt und bekannt, beispielsweise kann es sich um ein Programm oder ein Programm handeln, das eine Programmiersprache oder Hardware verwendet Beschreibungssprache zur Beschreibung von Schaltkreisen. Das Problem der Systemmodellierung besteht hauptsächlich darin, S auf eine besser handhabbare Größe zu reduzieren, indem irrelevante Details abstrahiert werden. KI-Systeme bringen sehr unterschiedliche Herausforderungen für die Systemmodellierung mit sich, die hauptsächlich auf den Einsatz von maschinellem Lernen zurückzuführen sind:

Hochdimensionaler Eingaberaum

ML-Komponenten für die Wahrnehmung arbeiten typischerweise mit sehr hohen Operationen auf einer Dimension Eingaberaum. Ein Eingabe-RGB-Bild kann beispielsweise 1000 x 600 Pixel groß sein und 256 ((1000 x 600 x 3)) Elemente enthalten. Die Eingabe ist normalerweise ein hochdimensionaler Vektorstream wie dieser. Obwohl Forscher formale Methoden für hochdimensionale Eingaberäume (wie in digitalen Schaltkreisen) verwendet haben, ist die Art des Eingaberaums für die ML-basierte Wahrnehmung anders. Er ist nicht vollständig boolesch, sondern gemischt und umfasst diskrete Variablen und kontinuierliche Variablen .

Hochdimensionaler Parameter-/Zustandsraum

ML-Komponenten wie tiefe neuronale Netze verfügen über Tausende bis Millionen von Modellparametern und Rohkomponenten. Beispielsweise verfügt das in Abbildung 2 verwendete hochmoderne DNN über bis zu 60 Millionen Parameter und Dutzende Komponentenschichten. Dadurch entsteht ein riesiger Suchraum für die Verifizierung, und der Abstraktionsprozess muss sehr sorgfältig durchgeführt werden.

Online-Anpassung und -Evolution

Einige Lernsysteme, wie z. B. Roboter, die RL nutzen, entwickeln sich weiter, wenn sie auf neue Daten und Situationen stoßen. Bei solchen Systemen muss die Überprüfung zur Entwurfszeit die zukünftige Entwicklung des Systemverhaltens berücksichtigen oder inkrementell online durchgeführt werden, während sich das Lernsystem weiterentwickelt.

Modellierung von Systemen im Kontext

Bei vielen KI/ML-Komponenten wird ihre Spezifikation ausschließlich durch den Kontext definiert. Um beispielsweise die Sicherheit des DNN-basierten Systems in Abbildung 2 zu überprüfen, ist eine Modellierung der Umgebung erforderlich. Wir brauchen Techniken, die ML-Komponenten und ihren Kontext modellieren, damit semantisch bedeutsame Eigenschaften überprüft werden können.

In den letzten Jahren haben sich viele Arbeiten auf die Verbesserung der Effizienz konzentriert, um die Robustheit und die Eingabe-Ausgabe-Eigenschaften von DNN zu überprüfen. Dies reicht jedoch nicht aus, wir müssen auch in den folgenden drei Aspekten Fortschritte machen:

Automatische Abstraktion und effiziente Darstellung

Die Abstraktion automatisch generierter Systeme war schon immer der Schlüssel zu formalen Methoden , das der Schlüssel zu formalen Methoden ist, spielen eine entscheidende Rolle bei der Ausweitung des Anwendungsbereichs auf große Hardware- und Softwaresysteme. Um die Herausforderungen ultrahochdimensionaler gemischter Zustandsräume und Eingaberäume für ML-basierte Systeme zu bewältigen, müssen wir effiziente Techniken zur Abstraktion von ML-Modellen in einfachere Modelle entwickeln, die einer formalen Analyse besser zugänglich sind. Einige vielversprechende Richtungen umfassen: Analyse von DNNs mithilfe abstrakter Interpretationen, Entwicklung von Abstraktionen zur Herstellung cyber-physischer Systeme mit ML-Komponenten und Entwurf neuer Darstellungen zur Verifizierung (z. B. Sternenmengen).

Erklärung und Ursache und Wirkung

Wir können die Aufgabe der Modellierung lernender Systeme vereinfachen, wenn Lernende ihre Vorhersagen mit Erklärungen darüber begleiten, wie die Vorhersagen aus den Daten und Hintergrundwissen entstanden sind. Die Idee ist nicht neu, da Begriffe wie „erklärungsbasierte Generalisierung“ bereits von der ML-Community erforscht werden, aber in jüngerer Zeit gibt es ein erneutes Interesse daran, Logik zur Erklärung der Ergebnisse lernender Systeme zu verwenden. Die Generierung von Erklärungen hilft beim Debuggen von Designs und Spezifikationen zur Entwurfszeit und hilft bei der Synthese robuster KI-Systeme, die zur Laufzeit Sicherheit bieten. ML, einschließlich kausaler und kontrafaktischer Argumentation, kann auch dabei helfen, Erklärungen für formale Methoden zu generieren.

Semantischer Merkmalsraum

Kontradiktorische Analyse und formale Verifizierung von ML-Modellen sind effizienter, wenn die generierten kontradiktorischen Eingaben und Gegenbeispiele im Kontext des verwendeten ML-Modells eine semantische Bedeutung haben. Beispielsweise sind Techniken, die einen DNN-Objektdetektor auf kleine Änderungen in der Farbe eines Autos oder der Tageszeit analysieren, nützlicher als Techniken, die einer kleinen Anzahl willkürlich ausgewählter Pixel Rauschen hinzufügen. Derzeit sind die meisten Methoden an diesem Punkt unzureichend. Wir brauchen eine semantische kontradiktorische Analyse, das heißt die Analyse von ML-Modellen im Kontext des Systems, zu dem sie gehören. Ein wichtiger Schritt besteht darin, den semantischen Merkmalsraum darzustellen, der die Umgebung modelliert, in der das ML-System arbeitet, und nicht den spezifischen Merkmalsraum, der den Eingaberaum für das ML-Modell definiert. Dies steht im Einklang mit der Intuition, dass der latente Raum, der durch semantisch bedeutsame Teile des konkreten Merkmalsraums (z. B. Bilder von Verkehrsszenen) gebildet wird, viel kleiner ist als der des gesamten konkreten Merkmalsraums. Der semantische Merkmalsraum in Abbildung 2 ist ein niedrigdimensionaler Raum, der die 3D-Welt um ein autonomes Fahrzeug herum darstellt, während der spezifische Merkmalsraum ein hochdimensionaler Pixelraum ist. Da die Dimensionalität des semantischen Merkmalsraums geringer ist, kann er einfacher durchsucht werden. Allerdings benötigen wir auch einen „Renderer“, der einen Punkt im semantischen Merkmalsraum auf einen Punkt im konkreten Merkmalsraum abbildet. Eigenschaften des Renderers, wie beispielsweise die Differenzierbarkeit, erleichtern die Anwendung formaler Methoden zur zielgerichteten Suche im semantischen Merkmalsraum.

Computer-Engines für Design und Verifizierung

Die Wirksamkeit formaler Methoden für Hardware- und Softwaresysteme wird durch Fortschritte bei den zugrunde liegenden „Computer-Engines“ vorangetrieben – zum Beispiel Boolean Satisfiability Solving (SAT) und Satisfiability Modular Theory ( SMT) und Modellprüfung. Angesichts der Größe von KI-/ML-Systemen, der Komplexität der Umgebung und der damit verbundenen neuartigen Spezifikationen wird eine neue Klasse von Rechenmaschinen für effizientes und skalierbares Training, Tests, Design und Validierung benötigt – wichtige Herausforderungen, die bewältigt werden müssen, um diese Fortschritte zu erzielen.

5.1 Datensatzdesign

Daten sind der grundlegende Ausgangspunkt für maschinelles Lernen Die Qualität eines ML-Systems muss die Qualität der Daten verbessern, aus denen es lernt. Wie können formale Methoden bei der systematischen Auswahl, Gestaltung und Anreicherung von ML-Daten helfen?

Die Datengenerierung für ML weist Ähnlichkeiten mit dem Problem der Testgenerierung für Hardware und Software auf. Formale Methoden haben sich für die systematische, auf Einschränkungen basierende Testgenerierung als effektiv erwiesen. Dies unterscheidet sich jedoch von den Anforderungen für Systeme der künstlichen Intelligenz, bei denen die Einschränkungstypen viel komplexer sein können – beispielsweise für den Einsatz von Sensoren zum Extrahieren von Daten aus komplexen Umgebungen wie z B. Verkehrsbedingungen), um Anforderungen an die „Authentizität“ der erfassten Daten zu kodieren. Wir müssen nicht nur Datenelemente mit bestimmten Merkmalen generieren (z. B. Tests, die Fehler finden), sondern wir müssen auch Sammlungen erstellen, die Verteilungsbeschränkungen erfüllen. Die Datengenerierung muss den Zielen in Bezug auf Datensatzgröße und Diversität für effektives Training und Verallgemeinerung entsprechen. Diese Anforderungen erfordern die Entwicklung neuer formaler Techniken.

Kontrollierte Randomisierung in formalen Methoden. Dieses Problem des Datensatzdesigns hat viele Aspekte. Erstens muss der Raum der „legitimen“ Eingaben definiert werden, damit die Beispiele entsprechend der Anwendungssemantik korrekt gebildet werden. Zweitens müssen Einschränkungen hinsichtlich des Ähnlichkeitsmaßes mit realen Daten vorgenommen werden erfasst werden; drittens muss häufig die Verteilung von Beispielen eingeschränkt werden, um eine Garantie dafür zu erhalten, dass der Lernalgorithmus mit dem wahren Konzept konvergiert.

Wir glauben, dass diese Aspekte durch stochastische formale Methoden angegangen werden können – Zufälligkeit, die zur Generierung von Daten verwendet wird, die formalen Einschränkungen und Verteilungsanforderungen unterliegen. Eine vielversprechende neue Klasse von Techniken heißt kontrollierte Improvisation, die zufällige Zeichenfolgen (Beispiel) x generiert, die drei Einschränkungen erfüllen:
- #🎜 🎜#Eine harte Einschränkung, die den zulässigen x-Raum definiert.
- Eine weiche Einschränkung, die definiert, wie x einer realen Welt ähneln muss Beispiel 🎜🎜#
Wir müssen verstehen, was zur Designzeit garantiert werden kann, wie der Designprozess zum sicheren Betrieb zur Laufzeit beiträgt, und das Design und wie Laufzeittechnologien effektiv zusammenarbeiten können.

5.3 Kombinatorisches Denken von KI/ML

Für die Skalierung auf große Systeme Formal Methoden, kombinatorisches (modulares) Denken sind unerlässlich. Bei der kompositorischen Verifizierung wird ein großes System (z. B. ein Programm) in seine Komponenten (z. B. ein Programm) zerlegt, jede Komponente wird anhand einer Spezifikation überprüft und dann werden die Komponentenspezifikationen zusammengenommen, um eine Spezifikation auf Systemebene zu erstellen. Ein üblicher Ansatz zur kombinatorischen Verifizierung ist die Verwendung von Annahme-Garantie-Verträgen. Beispielsweise geht ein Verfahren von seinem Anfangszustand (Vorbedingungen) aus, der wiederum seinen Endzustand (Nachbedingungen) garantiert und gleichzeitige Software- und Hardwaresysteme anwenden.

Diese Paradigmen decken jedoch keine künstlichen Intelligenzsysteme ab, was hauptsächlich auf den Abschnitt „Formale Spezifikationen“ zurückzuführen ist. Die Formalisierungsherausforderungen künstlicher Intelligenz Systeme besprochen in . Die zusammensetzbare Verifizierung erfordert eine kompositorische Spezifikation – das heißt, die Komponenten müssen formalisierbar sein. Allerdings ist es, wie unter „Formale Spezifikationen“ beschrieben, möglicherweise nicht möglich, das korrekte Verhalten einer Wahrnehmungskomponente formal zu spezifizieren. Daher besteht eine der Herausforderungen darin, Techniken des kombinatorischen Denkens zu entwickeln, die nicht auf einer vollständigen kombinatorischen Spezifikation beruhen. Darüber hinaus erfordert die quantitative und probabilistische Natur von KI-Systemen eine Ausweitung der Theorie des kombinatorischen Denkens auf quantitative Systeme und Spezifikationen.

Komponentenverträge ableiten. Der kombinatorische Entwurf und die Analyse von KI-Systemen erfordern Fortschritte an mehreren Fronten. Erstens besteht die Notwendigkeit, auf einigen vielversprechenden Vorarbeiten aufzubauen, um eine Theorie für den Entwurf und die Überprüfung probabilistischer Garantien für den semantischen Raum dieser Systeme zu entwickeln. Zweitens müssen neue induktive Synthesetechniken entwickelt werden, um hypothesengewährleistende Verträge algorithmisch zu generieren, die den normativen Aufwand verringern und kombinatorisches Denken erleichtern. Drittens schlagen wir Techniken vor, um Einschränkungen auf Komponentenebene aus der Analyse auf Systemebene abzuleiten und mithilfe dieser Einschränkungen die Analyse auf Komponentenebene, einschließlich der kontradiktorischen Analyse, auf die Suche zu konzentrieren, um Fälle wie die Wahrnehmung zu behandeln, bei denen Komponenten keine präzisen formalen Spezifikationen haben „relevanter“ Teil des Raumes. In einer idealen Welt wäre die Verifizierung in den Entwurfsprozess integriert, sodass das System „während der Konstruktion geändert“ wird. Beispielsweise könnte die Verifizierung mit dem Kompilierungs-/Syntheseschritt verschachtelt werden, wobei ein RTL-Entwurfsablauf (Register Transfer Level) angenommen wird, der in integrierten Schaltkreisen üblich ist, und möglicherweise könnte sie in den Synthesealgorithmus integriert werden, um sicherzustellen, dass die Implementierung der Spezifikation entspricht. Können wir einen geeigneten Entwurfsprozess für Systeme der künstlichen Intelligenz entwerfen, der während des Baus schrittweise überarbeitet wird?

6.1 Spezifikationsgesteuertes Design von ML-Komponenten
Gegeben a Formale Spezifikation: Können wir eine Komponente (Modell) für maschinelles Lernen entwerfen, die nachweislich diese Spezifikation erfüllt? Der Entwurf dieser neuen ML-Komponente umfasst viele Aspekte: (1) Entwurf des Datensatzes, (2) Synthese der Struktur des Modells, (3) Generierung eines repräsentativen Satzes von Merkmalen, (4) Synthese der Hyperparameter und anderer Auswahlmöglichkeiten der Aspekte des ML-Algorithmus und (5) Techniken zur Automatisierung des Debuggens von ML-Modellen oder -Spezifikationen, wenn die Synthese fehlschlägt.

Formale Synthese von ML-Komponenten. Lösungen für einige der zuvor aufgeführten Probleme können mithilfe semantischer Verlustfunktionen oder zertifizierter Robustheit erzwungen werden. Diese Techniken können mit Methoden wie der neuronalen Architektursuche kombiniert werden, um korrekt konstruierte Modelle zu generieren. Ein anderer Ansatz basiert auf der aufkommenden Theorie der formalen induktiven Synthese, also der Synthese aus Programminstanzen, die formale Spezifikationen erfüllen. Der gebräuchlichste Weg zur Lösung formaler induktiver Syntheseprobleme ist die Verwendung eines orakelgesteuerten Ansatzes, bei dem ein Lernender mit einem Orakel gepaart wird, das die Anfrage beantwortet, wie in Abbildung 2 im Beispiel. Das Orakel kann ein Fälscher sein, der Gegenbeispiele generiert Zeigen Sie, wie die Lernkomponente versagt. Verletzung von Spezifikationen auf Systemebene. Schließlich ist die Verwendung von Theorembeweisen zur Sicherstellung der Korrektheit der zum Trainieren von ML-Modellen verwendeten Algorithmen auch ein wichtiger Schritt zur Konstruktion modifizierter ML-Komponenten.
6.2 Systemdesign basierend auf maschinellem Lernen
#🎜 🎜#
Die zweite Herausforderung besteht darin, ein Gesamtsystem zu entwerfen, das lernende und nicht-lernende Komponenten umfasst. Es sind mehrere Forschungsfragen aufgetaucht: Können wir die sicheren Grenzen berechnen, innerhalb derer der Betrieb von ML-Komponenten eingeschränkt werden kann? Können wir einen Steuerungs- oder Planungsalgorithmus entwerfen, der die Einschränkungen der ML-fähigen Komponente, die er als Eingabe erhält, überwindet? Können wir eine kombinatorische Designtheorie für Systeme der künstlichen Intelligenz entwickeln? Wenn zwei ML-Modelle verwendet werden, um zwei verschiedene Arten von Sensordaten (z. B. LiDAR und visuelle Bilder) zu erfassen, und jedes Modell unter bestimmten Annahmen seine Spezifikationen erfüllt, unter welchen Bedingungen können die beiden dann zusammen verwendet werden, um die Zuverlässigkeit des Gesamtsystems zu verbessern?

Ein prominentes Beispiel für Fortschritte bei dieser Herausforderung ist die Arbeit an einer sicheren lernbasierten Steuerung. Dieser Ansatz berechnet vorab einen Sicherheitsbereich und verwendet Lernalgorithmen, um den Controller innerhalb dieses Bereichs abzustimmen. Dazu sind Techniken erforderlich, um solche Sicherheitsbereiche beispielsweise auf der Grundlage einer Erreichbarkeitsanalyse effizient zu berechnen. Auch auf dem Gebiet der sicheren RL wurden erhebliche Fortschritte erzielt .

Allerdings werden diese den Herausforderungen, die maschinelles Lernen für die Wahrnehmung und Vorhersage mit sich bringt, nicht vollständig gerecht – beispielsweise muss ein nachweislich sicheres End-to-End-Deep-Reinforcement-Learning noch erreicht werden. 6.3 Überbrückung von Entwurfszeit und Laufzeit für belastbare KI Für die Richtigkeit kann keine Gewähr übernommen werden. Technologien, die Fehlertoleranz und Fehlerbehebung zur Laufzeit implementieren, spielen in Systemen der künstlichen Intelligenz eine wichtige Rolle. Wir benötigen ein systematisches Verständnis dafür, was zur Entwurfszeit garantiert werden kann, wie der Entwurfsprozess zum sicheren und korrekten Betrieb von KI-Systemen zur Laufzeit beiträgt und wie Entwurfszeit- und Laufzeittechnologien effektiv zusammenarbeiten können.

In dieser Hinsicht liefert uns die Literatur zu fehlertoleranten und zuverlässigen Systemen die Grundlage für die Entwicklung von Laufzeitsicherungstechniken – also Laufzeitverifizierungs- und Mitigationstechniken, die beispielsweise mit der Simplex-Methode kombiniert werden können komplex, aber einfach Ein Ansatz, der fehlerhafte Module mit sicheren, formal verifizierten Backup-Modulen kombiniert. In jüngerer Zeit haben Techniken, die Entwurfszeit- und Laufzeitsicherungsansätze kombinieren, gezeigt, dass nicht verifizierte Komponenten, einschließlich solcher, die auf KI und ML basieren, in Laufzeitsicherungs-Frameworks verpackt werden können, um Garantien für einen sicheren Betrieb zu bieten. Derzeit sind diese jedoch auf bestimmte Systemklassen beschränkt oder erfordern den manuellen Entwurf von Laufzeitmonitoren und Schadensbegrenzungsstrategien. Es werden noch weitere Ansätze wie introspektive Umgebungsmodellierung, auf künstlicher Intelligenz basierende Monitore und die Synthese sicherer Fallback-Strategien folgen. Es muss noch viel Arbeit geleistet werden.

Der hier diskutierte Entwurfsansatz zur Änderung intelligenter Systeme im Bauwesen kann zu einem Mehraufwand führen, der es schwieriger macht, Leistungs- und Echtzeitanforderungen zu erfüllen. Aber wir glauben (vielleicht nicht intuitiv), dass formale Methoden sogar dazu beitragen können, die Leistung oder Energieeffizienz eines Systems im folgenden Sinne zu verbessern.

Traditionelle Leistungsoptimierung ist in der Regel kontextunabhängig – Aufgaben müssen beispielsweise Fristen einhalten, unabhängig von der Umgebung, in der sie ausgeführt werden. Wenn diese Umgebungen jedoch zur Entwurfszeit formal charakterisiert, zur Laufzeit überwacht und ihr Systembetrieb formal als sicher verifiziert wird, können ML-Modelle in solchen Umgebungen Genauigkeit gegen höhere Effizienz eintauschen. Dieser Kompromiss könnte ein fruchtbarer Bereich für zukünftige Forschung sein.

FazitAus formaler Methodenperspektive haben wir das Problem des Entwurfs hochsicherer Systeme für künstliche Intelligenz analysiert. Wie in Abbildung 3 dargestellt, haben wir fünf große Herausforderungen bei der Anwendung formaler Methoden auf KI-Systeme identifiziert und drei Entwurfs- und Verifizierungsprinzipien für jede der fünf Herausforderungen entwickelt, die das Potenzial haben, diese Herausforderung zu bewältigen.

Die Kanten in Abbildung 3 zeigen die Abhängigkeiten zwischen diesen Prinzipien, wie z. B. Laufzeitgarantien, die auf Selbstbeobachtung und datengesteuerter Umgebungsmodellierung basieren, um überwachbare Annahmen und Umgebungsmodelle zu extrahieren. Um eine Analyse auf Systemebene durchzuführen, müssen wir uns ebenfalls mit kombinatorischem Denken und Abstraktion befassen, wobei einige KI-Komponenten möglicherweise Mining-Spezifikationen erfordern, während andere die richtige Struktur durch formale induktive Synthese generieren.

Mehrere Forscher, darunter auch die Autoren, arbeiten seit 2016 an diesen Herausforderungen, als die ursprünglich veröffentlichte Version dieses Artikels einige beispielhafte Fortschritte präsentierte. Wir haben die Open-Source-Tools VerifAI und Scenic entwickelt, die Techniken basierend auf den in diesem Artikel beschriebenen Prinzipien implementieren und auf Systeme im industriellen Maßstab im autonomen Fahren und in der Luft- und Raumfahrt angewendet wurden. Diese Ergebnisse sind erst der Anfang, und es gibt noch viel zu tun. Es wird erwartet, dass überprüfbare KI auch in den kommenden Jahren ein fruchtbares Forschungsgebiet sein wird.

Das obige ist der detaillierte Inhalt vonAuf dem Weg zur überprüfbaren KI: Fünf Herausforderungen formaler Methoden. Für weitere Informationen folgen Sie bitte anderen verwandten Artikeln auf der PHP chinesischen Website!