title: Parallel techniques for neural network verification
title: Παράλληλες τεχνικές για την επαλήθευση νευρωνικών δικτύων
Creators: name: Μονογυιος Αντωνιος
Publisher: name: Technical University of Crete
Year: 2025

description: Parallel Neural Networks verifiers are software tools that leverage parallel architectures to prove fast and rigorously the correct functionality of neural networks in mission-critical environments such as aviation, autonomous driving, etc. In this thesis, we present a plug-in based on Bayesian Optimization that uses transfer learning between different safety specifications to accelerate their parallel verification, while also providing an alternative method based on the state of neurons inside the neural network under verification.
In the proposed method of transferring between safety specifications, the plug-in utilizing the available computational resources receives as input a trained neural network and a safety specification applied on its input dimensions. Accordingly, performing a few verification trials it creates a Bayesian Optimization model, which can accurately predict the verification time for any parallelization scheme (input split). Thus, it can provide a parallelization scheme minimizing the overall verification time. Then, it utilizes the trained model to predict parallelization schemes that minimize the overall execution time for new safety specifications that fully or partially overlap with the original specification.
The second operational mode is based on performing few prediction trials with the neural network under verification instead of verification. The process creates and trains a Bayesian Optimization model that can accurately predict the number of active and inactive ReLU neurons for a parallelization scheme. As a result, it can provide a parallelization scheme that minimizes the number of unstable neurons, since minimizing this number is accompanied by a minimization on the verification time.
Summarizing, we perform an experimental evaluation of the 2 methods of operation in our proposed plug-in, evaluating the quality of the proposed parallelization schemes based on their ranking relative to every other, and provide the results of our measurements. The results gathered during the experimental evaluation prove the efficiency of our methods in regard to accelerating the parallel verification of neural networks.

description: Οι παράλληλοι πιστοποιητές νευρωνικών δικτύων είναι εργαλεία λογισμικού, που αξιοποιούν παράλληλες αρχιτεκτονικές ώστε να επαληθεύσουν γρήγορα και με αυστηρό τρόπο τη ορθή λειτουργικότητα νευρωνικών δικτύων σε περιβάλλοντα καίριας σημασίας όπως αεροπλοΐα, αυτόνομη οδήγηση, κ.ο.κ. Στην παρούσα διπλωματική εργασία, προτείνουμε μια εξωτερική επεκτάση με βάση την Bayesian βελτιστοποίηση, η οποία χρησιμοποιεί μεταφορά μάθησης μεταξύ διαφορετικών προδιαγραφών ασφαλείας για να επιταχύνει την παράλληλη πιστοποίηση τους, καθώς και μια εναλλακτική μέθοδο βασισμένη στη συμπεριφορά των νευρώνων του δικτύου υπό επαλήθευση.
Στη μεταφορά μάθησης μεταξύ προδιαγραφών ασφαλείας, η επέκταση αξιοποιώντας τους διαθέσιμους πόρους λαμβάνει ένα εκπαιδευμένο νευρωνικό δίκτυο και μια προδιαγραφή πάνω στις διαστάσεις εισόδου του. Εκτελώντας ένα περιορισμένο αριθμό από δοκιμές πιστοποίησης δημιουργεί ένα μοντέλο} Bayesian βελτιστοποίησης, το οποίο μπορεί με ακρίβεια να προβλέψει τον χρόνο πιστοποίησης για κάθε σχέδιο παραλληλισμού (διαμέριση προδιαγραφής εισόδου). Επομένως, μπορεί να παρέχει ένα σχέδιο παραλληλισμού το οποίο ελαχιστοποιεί τον συνολικό χρόνο πιστοποίησης. Στη συνέχεια, αξιοποιεί το εκπαιδευμένο μοντέλο για να προβλέψει σχέδια παραλληλισμού που ελαχιστοποιούν τον συνολικό χρόνο πιστοποίησης νέων προδιαγραφών μερικώς ή πλήρως επικαλυπτόμενων από την αρχική προδιαγραφή.
Η δεύτερη λειτουργία βασίζεται στην πραγματοποίηση μερικών δοκιμών πάνω στις προβλέψεις του νευρωνικού δικτύου αντί για πιστοποιήσεις. Δημιουργεί και εκπαιδεύει ένα μοντέλο Bayesian βελτιστοποιητή το οποίο μπορεί να προβλέψει με ακρίβεια τον αριθμό από νευρώνες που ενεργοί ή ανενεργοί για κάποιο σχέδιο παραλληλισμού. Συνεπώς, μπορεί να παρέχει ένα σχέδιο παραλληλισμού που ελαχιστοποιεί τον αριθμό των ενεργοποιημένων νευρώνων, καθώς ελαχιστοποιώντας αυτόν τον αριθμό συνοδεύεται με ελαχιστοποίηση του χρόνου πιστοποίησης. 
Εν κατακλείδι, πραγματοποιούμε πειραματική αξιολόγηση και των 2 τρόπων λειτουργίας της εξωτερικής επέκτασης που προτείνουμε, αξιολογώντας την ποιότητα των προτεινόμενων σχεδίων παραλληλισμού με βάση την κατάταξη τους σε σχέση με όλες τις υπόλοιπες, καθώς και παρέχουμε τα αποτελέσματα των μετρήσεων μας. Τα αποτελέσματα που συλλέχθηκαν κατά την πειραματική διαδικασία επιβεβαιώνουν την αποτελεσματικότητα τους όσο αναφορά την επιτάχυνση της παράλληλη πιστοποίηση νευρωνικών δικτύων.