Korrekte Orchestrierung generischer Algorithmen des föderierten Lernens: Python-Übersetzung in CSP und Verifizierung durch PAT

Zusammenfassung Föderiertes Lernen (FL) ist ein maschinelles Lernsetting, in dem die Clients die Trainingsdaten dezentral halten und ein Modell entweder unter der Koordination eines zentralen Servers (zentrales FL) oder in einem Peer-to-Peer-Netzwerk (dezentralisiertes FL) gemeinsam trainieren. Die korrekte Orchestrierung ist eine der Haupt Herausforderungen. In diesem Papier überprüfen wir formal die Korrektheit von zwei generischen FL-Algorithmen, einem zentralisierten und einem dezentralisierten, unter Verwendung der Communicating Sequential Processes (CSP) Berechnung und des Process Analysis Toolkit (PAT) Model Checkers. Die CSP-Modelle bestehen aus CSP-Prozessen, die den Instanzen generischer FL-Algorithmen entsprechen. PAT beweist automatisch die Korrektheit der beiden generischen FL-Algorithmen, indem es ihre Deadlock-Freiheit (Sicherheitsproperty) und erfolgreiche Beendigung (Erreichbarkeits- und Lebendigkeitsproperty) nachweist. Die CSP-Modelle werden als treue Darstellung des tatsächlichen Python-Codes konstruiert und direkt in der CSP#-Sprache ausgedrückt, die PAT verwendet. Anschließend werden sie automatisch von oben nach unten von PAT überprüft. Der Python-Code folgt einem eingeschränkten aktorbasierten Programmiermodell, und die Konstruktion von CSP#-Code aus solchem Python-Code erfolgt systematisch. Der Prozess wird im Detail beschrieben, um sicherzustellen, dass die Modelle dem tatsächlichen Code entsprechen. Dies stellt eine Grundlage für die Entwicklung von Werkzeugen zur automatischen Übersetzung bestimmter Klassen von Python-Code in CSP-Modelle dar, die in CSP# ausgedrückt sind.