Studio e classificazione di istanze per la verifica di reti neurali

Abstract

La verifica delle reti neurali rappresenta un campo in rapida evoluzione e di fondamentale importanza per il loro impiego in applicazioni critiche, ovvero in contesti in cui è indispensabile garantire un comportamento affidabile del modello. Dal 2020, esiste una competizione internazionale su questo tema, la VNNCOMP, che vede la partecipazione di diversi strumenti di verifica. La valutazione delle performance si basa su benchmark proposti annualmente dai team partecipanti. Tuttavia, un problema rilevante risiede nella mancanza di organizzazione di questi benchmark, i quali non risultano classificati secondo la tipologia di modello o altre caratteristiche affini.

La presente tesi si propone di offrire una struttura più ordinata e coerente per i benchmark, migliorandone l’organizzazione. Inoltre, si sviluppa un software in grado di generare benchmark personalizzati, basati su criteri specifici, come il tipo di layer utilizzato o l'architettura del modello. L’obiettivo finale è facilitare la fase di testing degli strumenti di verifica, con particolare attenzione agli strumenti nelle prime fasi del loro sviluppo, rendendo il processo più accessibile e strutturato.

Il linguaggio di programmazione utilizzato per il raggiungimento dell'obiettivo è Python, con l'ausilio delle librerie ONNX, Pandas, e CustomTkinter. Queste librerie sono rispettivamente utilizzate per la classificazione automatizzata, la gestione della logica per il software di generazione dei benchmark personalizzati, e la creazione di un'interfaccia grafica.

The verification of neural networks is a rapidly evolving field and is of fundamental importance for their use in critical applications, i.e., in contexts where it is essential to ensure a reliable behavior of the model. Since 2020, there has been an international competition on this topic, VNNCOMP, which sees the participation of various verification tools. Performance evaluation is based on benchmarks proposed annually by participating teams. However, a significant issue lies in the lack of organization of these benchmarks, as they are not classified according to model type or other relevant characteristics.

This thesis aims to provide a more structured and coherent framework for the benchmarks, improving their organization. Furthermore, software is being developed to generate customized benchmarks based on specific criteria, such as the type of layer used or the model architecture. The ultimate goal is to facilitate the testing phase of verification tools, with particular attention to tools in the early stages of development, making the process more accessible and structured.

The programming language used to achieve this goal is Python, with the aid of the ONNX, Pandas, and CustomTkinter libraries. These libraries are respectively used for automated classification, logic management for the customized benchmark generation software, and the creation of a graphical interface.