ETD

• certificazione
• certify
• network
• neural
• neurali
• properties
• proprietà
• reti
• simplesso
• simplex
• tropical
• tropicale

Deep Neural Networks (DNNs) are increasingly deployed in safety-critical systems, necessitating rigorous formal guarantees on their behavior. This thesis theoretically investigates and implements the Tropical Simplex algorithm as a novel approach to certify safety properties of ReLU-based neural networks. Leveraging the mathematical correspondence between ReLU activations and tropical rational maps, the verification problem is reframed within Tropical Linear Programming (TLP). Unlike classical relaxation methods, this study operates on the symmetrized tropical semiring, utilizing the Tropical Simplex to navigate the complex geometry of the network's decision boundaries. By encoding the network's constraints as tropical hypersurfaces, the implemented algorithm allows for the exact verification of safety properties, exploiting the intrinsic combinatorial structure of tropical polyhedra to address the challenge of non-convex optimization in neural certification.

Le reti neurali profonde (DNN) sono sempre più utilizzate nei sistemi critici per la sicurezza, i quali richiedono garanzie formali e rigorose per il loro comportamento. Questo lavoro studia ed implementa l'algoritmo del simplesso tropicale come approccio innovativo per certificare le proprietà di sicurezza delle reti neurali basate su ReLU. Sfruttando la corrispondenza matematica tra la funzione di attivazione ReLU e le mappe razionali tropicali, il problema della verifica formale delle proprietà della rete viene riformulato nell'ambito della programmazione lineare tropicale (TLP). A differenza dei metodi di rilassamento classici, questo studio lavora con il semianello tropicale simmetrizzato e utilizza il simplesso tropicale per navigare nella complessa geometria dei confini decisionali della rete. Codificando i vincoli della rete come ipersuperfici tropicali, l'algoritmo implementato consente la verifica esatta delle proprietà di sicurezza, sfruttando la struttura combinatoria intrinseca dei poliedri tropicali per superare la sfida dell'ottimizzazione non convessa nella certificazione neurale.