Standardizzazione dei benchmark VNN-COMP: analisi strutturale di reti neurali ONNX e automazione della transizione a VNN-LIB 2.0

Abstract

La competizione VNN-COMP consiste in una raccolta di suite di benchmark per la valutazione degli strumenti di verifica formale per le reti neurali. Questa tesi mira ad analizzare sistematicamente le architetture delle reti neurali contenute nei benchmark esistenti attraverso le loro rappresentazioni ONNX, estraendo informazioni strutturali e altre caratteristiche rilevanti per comprendere meglio quali architetture di rete debbano essere supportate dal verificatore NeVer2. Il lavoro include anche la migrazione delle proprietà di sicurezza dei benchmark dal formato VNN-LIB 1.0 al recente standard VNN-LIB 2.0. In particolare, la tesi si concentra sull'analisi dei modelli di reti neurali ONNX e sullo sviluppo e adattamento di script di conversione per tradurre automaticamente le proprietà dei benchmark da VNN-LIB 1.0 a VNN-LIB 2.0. Il framework proposto garantisce la correttezza e la conformità dei benchmark generati rispetto al nuovo standard, contribuendo alla standardizzazione delle specifiche dei benchmark all'interno della comunità VNN-COMP e facilitando le future campagne di verifica basate sull'emergente formato VNN-LIB 2.0.

The VNN-COMP competition consists of a collection of benchmark suites for evaluating formal verification tools for neural networks. This thesis aims to systematically analyze the neural network architectures contained in existing benchmarks through their ONNX representations, extracting structural information and other relevant characteristics to better understand which network architectures must be supported by the NeVer2 verifier. The work also includes the migration of the benchmark safety properties from the VNN-LIB 1.0 format to the recently introduced VNN-LIB 2.0 standard. In particular, the thesis focuses on the analysis of ONNX neural network models and on the development and adaptation of conversion scripts to automatically translate benchmark properties from VNN-LIB 1.0 to VNN-LIB 2.0. The proposed framework ensures the correctness and compliance of the generated benchmarks with the new standard, contributing to the standardization of benchmark specifications within the VNN-COMP community and facilitating future verification campaigns based on the emerging VNN-LIB 2.0 format.