Institutional Repository [SANDBOX]
Technical University of Crete
EN  |  EL

Search

Browse

My Space

Parallel techniques for neural network verification

Monogyios Antonios

Simple record


URIhttp://purl.tuc.gr/dl/dias/63577073-807A-4ECA-9EC7-FFD821D402A1-
Identifierhttps://doi.org/10.26233/heallink.tuc.102611-
Languageen-
Extent75 pagesen
TitleParallel techniques for neural network verificationen
TitleΠαράλληλες τεχνικές για την επαλήθευση νευρωνικών δικτύωνel
CreatorMonogyios Antoniosen
CreatorΜονογυιος Αντωνιοςel
Contributor [Thesis Supervisor]Giatrakos Nikolaosen
Contributor [Thesis Supervisor]Γιατρακος Νικολαοςel
Contributor [Committee Member]Chalkiadakis Georgiosen
Contributor [Committee Member]Χαλκιαδακης Γεωργιοςel
Contributor [Committee Member]Spyropoulos Thrasyvoulosen
Contributor [Committee Member]Σπυροπουλος Θρασυβουλοςel
PublisherΠολυτεχνείο Κρήτηςel
PublisherTechnical University of Creteen
Academic UnitTechnical University of Crete::School of Electrical and Computer Engineeringen
Academic UnitΠολυτεχνείο Κρήτης::Σχολή Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστώνel
Content SummaryParallel 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. en
Content SummaryΟι παράλληλοι πιστοποιητές νευρωνικών δικτύων είναι εργαλεία λογισμικού, που αξιοποιούν παράλληλες αρχιτεκτονικές ώστε να επαληθεύσουν γρήγορα και με αυστηρό τρόπο τη ορθή λειτουργικότητα νευρωνικών δικτύων σε περιβάλλοντα καίριας σημασίας όπως αεροπλοΐα, αυτόνομη οδήγηση, κ.ο.κ. Στην παρούσα διπλωματική εργασία, προτείνουμε μια εξωτερική επεκτάση με βάση την Bayesian βελτιστοποίηση, η οποία χρησιμοποιεί μεταφορά μάθησης μεταξύ διαφορετικών προδιαγραφών ασφαλείας για να επιταχύνει την παράλληλη πιστοποίηση τους, καθώς και μια εναλλακτική μέθοδο βασισμένη στη συμπεριφορά των νευρώνων του δικτύου υπό επαλήθευση. Στη μεταφορά μάθησης μεταξύ προδιαγραφών ασφαλείας, η επέκταση αξιοποιώντας τους διαθέσιμους πόρους λαμβάνει ένα εκπαιδευμένο νευρωνικό δίκτυο και μια προδιαγραφή πάνω στις διαστάσεις εισόδου του. Εκτελώντας ένα περιορισμένο αριθμό από δοκιμές πιστοποίησης δημιουργεί ένα μοντέλο} Bayesian βελτιστοποίησης, το οποίο μπορεί με ακρίβεια να προβλέψει τον χρόνο πιστοποίησης για κάθε σχέδιο παραλληλισμού (διαμέριση προδιαγραφής εισόδου). Επομένως, μπορεί να παρέχει ένα σχέδιο παραλληλισμού το οποίο ελαχιστοποιεί τον συνολικό χρόνο πιστοποίησης. Στη συνέχεια, αξιοποιεί το εκπαιδευμένο μοντέλο για να προβλέψει σχέδια παραλληλισμού που ελαχιστοποιούν τον συνολικό χρόνο πιστοποίησης νέων προδιαγραφών μερικώς ή πλήρως επικαλυπτόμενων από την αρχική προδιαγραφή. Η δεύτερη λειτουργία βασίζεται στην πραγματοποίηση μερικών δοκιμών πάνω στις προβλέψεις του νευρωνικού δικτύου αντί για πιστοποιήσεις. Δημιουργεί και εκπαιδεύει ένα μοντέλο Bayesian βελτιστοποιητή το οποίο μπορεί να προβλέψει με ακρίβεια τον αριθμό από νευρώνες που ενεργοί ή ανενεργοί για κάποιο σχέδιο παραλληλισμού. Συνεπώς, μπορεί να παρέχει ένα σχέδιο παραλληλισμού που ελαχιστοποιεί τον αριθμό των ενεργοποιημένων νευρώνων, καθώς ελαχιστοποιώντας αυτόν τον αριθμό συνοδεύεται με ελαχιστοποίηση του χρόνου πιστοποίησης. Εν κατακλείδι, πραγματοποιούμε πειραματική αξιολόγηση και των 2 τρόπων λειτουργίας της εξωτερικής επέκτασης που προτείνουμε, αξιολογώντας την ποιότητα των προτεινόμενων σχεδίων παραλληλισμού με βάση την κατάταξη τους σε σχέση με όλες τις υπόλοιπες, καθώς και παρέχουμε τα αποτελέσματα των μετρήσεων μας. Τα αποτελέσματα που συλλέχθηκαν κατά την πειραματική διαδικασία επιβεβαιώνουν την αποτελεσματικότητα τους όσο αναφορά την επιτάχυνση της παράλληλη πιστοποίηση νευρωνικών δικτύων. el
Type of ItemΔιπλωματική Εργασίαel
Type of ItemDiploma Worken
Licensehttp://creativecommons.org/licenses/by/4.0/en
Date of Item2025-03-12-
Date of Publication2025-
SubjectΠαράλληλες τεχνικέςel
SubjectParallel techniquesen
SubjectBayesian optimizationen
SubjectΕπαλήθευση νευρωνικών δικτύωνel
SubjectNeural Network Verificationen
Bibliographic CitationAntonios Monogyios, "Parallel techniques for neural network verification", Diploma Work, School of Electrical and Computer Engineering, Technical University of Crete, Chania, Greece, 2025en
Bibliographic CitationΑντώνιος Μονογυιός, "Παράλληλες τεχνικές για την επαλήθευση νευρωνικών δικτύων", Διπλωματική Εργασία, Σχολή Ηλεκτρολόγων Μηχανικών και Μηχανικών Υπολογιστών, Πολυτεχνείο Κρήτης, Χανιά, Ελλάς, 2025el

Available Files

Services

Statistics