Prophecy: Automatisches Ableiten formaler Eigenschaften aus Neuronaktivierungen
Ein neues Werkzeug namens Prophecy ermöglicht es, formale Eigenschaften von Feed‑Forward‑Neuronalen Netzwerken automatisch abzuleiten. Die Idee beruht auf der Erkenntnis, dass ein großer Teil der Logik solcher Netzwerke in den Aktivierungszuständen der Neuronen in den inneren Schichten verankert ist.
Prophecy extrahiert Regeln, die auf Neuronaktivierungen (Werte oder Ein/Aus‑Status) basieren und bestimmte gewünschte Ausgabeeigenschaften implizieren – etwa die Vorhersage einer bestimmten Klasse. Diese Regeln stellen die in den versteckten Schichten gefangenen Netzwerkeigenschaften dar, die das gewünschte Verhalten der Ausgabe bestimmen.
Die Architektur des Tools, seine Funktionen und Anwendungsbeispiele werden detailliert vorgestellt. Prophecy findet Einsatz bei der Ableitung und dem Beweis formaler Erklärungen, der kompositionsbasierten Verifikation, der Laufzeitüberwachung, der Reparatur und weiteren Bereichen. Besonders hervorzuheben sind die neu gewonnenen Erkenntnisse, die das Potenzial von Prophecy im Zeitalter großer Vision‑Language‑Modelle unterstreichen.