Perché è necessaria l’AI Verification?
Bene. Dobbiamo metterci comodi e rilassarci.
Stiamo per iniziare un affascinante, seppur complesso, viaggio.
Si parte.
AI Verification
Creare software complessi è difficile.
Così abbiamo iniziato a usare sistemi di machine learning, deep neural network, per risolvere questo problema.
Questi sistemi sono però opachi, delle black box: non sappiamo cosa avvenga al loro interno.
Fintantoché rimangano attive all’interno di laboratori di ricerca, questa particolarità è una questione secondaria. Quando però i contesti di applicazioni riguardano più direttamente noi essere umani entrano in gioco diversi fattori: etica, sicurezza, privacy, affidabilità.
L’AI Verification nasce allora come sistema di certificazione circa il corretto comportamento di reti neurali profonde, e più in generale per i sistemi d’intelligenza artificiale.
Questo è il secondo modulo di una serie di articoli introduttivi a una vasta area di studi che ho deciso di organizzare attorno a 5 aree tematiche:
- Trust AI (il concetto di fairness in primo luogo)
- Verification
- Security
- Privacy
- Adversarial
Ti esorto a leggere il primo modulo, qualora non lo avessi ancora fatto. Ti accorgerai che molti concetti si incastrano tra loro in una big picture generale ben più ampia.
Qualcosa di pazzesco!
Per il momento, concentriamoci sul tema del post.
Dove eravamo? Ah si… AI Verification
Neural Networks Attacks
Un modello di Linear Regression è semplice: ha poco senso attaccare un sistema simile per modificarne l’output.
Per una rete neurale profonda la situazione cambia. Ecco gli adversarial example
Adversarial Example
Un adversarial example è un’istanza con una piccola e intenzionale perturbazione, tale da renderla indistinguibile dall’originale all’occhio umano, che causa una falsa previsione da parte di un modello di machine learning, come un deep neural network.
Adversarial example sono quindi counterfactual example (esempi controfattuale) con l’obiettivo d’ingannare il modello.
Adversarial example rendono un modello di machine learning vulnerabile ad attacchi, come nei seguenti scenari:
- Scontro tra auto a guida autonoma causato da una mancata considerazione del segnale di STOP. Qualcuno ha piazzato delle immagini sopra il cartello stradale, che appare leggermente sporco a un essere umano, progettate per far riconoscere il segnale come un DIVIETO DI SOSTA.
- Uno spam detector fallisce a classificare un’email come spam. L’email è stata progettata per bypassare i sistemi di controllo del modello raggiungendo il destinatario.
- Uno scanner aeroportuale a raggi x, controllato da un modello di machine learning, lascia passare un coltello con piccole modifiche tali da evitarne il riconoscimento: appare come un ombrello.
Qualora volessi approfondire l’argomento ti rimando a un interessante libro di Christoph Molnar: Interpretable Machine Learning
Tornando a noi…
Perturbando alcune immagini di input in un classificatore è possibile influenzarne drasticamente il funzionamento.
In una pubblicazione datata 2015, EXPLAINING AND HARNESSING ADVERSARIAL EXAMPLES tre dipendenti di Google Ian J. Goodfellow, Jonathon Shlens e Christian Szegedy hanno approfondito questo concetto.
Nel loro caso è stato necessario modificare una moltitudine di pixel nelle immagini fornite al sistema.
Qual è dunque il minor numero di pixel che è necessario perturbare affinché venga compiuto un simile attacco?
Jiawei Su, Danilo Vargas e Kouichi Sakurai (so che non hai letto il nome: per loro rispetto torna indietro e leggi 🙂 hanno dimostrato come sia possibile modificare un singolo pixel per produrre risultati sconvolgenti!
Il problema dunque può quindi essere più grave di quanto si possa credere.
Qualora volessi approfondire il tema degli adversarial example ti rimando ad un post su IAML.
Zero Day Attacks
Un sistema grezzo per allenare le reti a resistere agli attacchi generici è quello di usare gli stessi Adversarial Example nella fase di training.
Esistono comunque attacchi denominati Zero-day, un simpatico nome per indicare i nuovi attacchi per la quale una rete neurale non era stata preparata.
Sono particolarmente pericolosi e danneggianti: ecco perché è fondamentale sviluppare delle metodologie per valutare la resistenza delle reti nonché aiutare gli sviluppatori a comprendere la confidenza nelle previsioni del modello e la loro affidabilità nel mondo reale.
Qui entrano in gioco le tecniche di Formal Verification (verificazione formale) che hanno appunto l’obiettivo di valutare la robustness di una rete neurale artificiale a eventuali attacchi, come quello di Zero-day Attack. Questo problema non si limita solo alle performance di un deep neural network ma si estende anche al livello di riservatezza e privacy.
Alcuni ricercatori hanno identificato nella verifica delle proprietà della rete neurale profonda un metodo promettente per difendersi agli adversarial examples, poiché tali sistemi sarebbero in grado d’identificare anche nuovi attacchi.
Uno di questi sistemi è Reluplex
Neural Network Verification (Reluplex)
In una rete neurale un sistema di Network Verification controllerebbe continuamente le proprietà di una rete neurale assicurandosi che uno specifico input violi o soddisfi tali proprietà.
Uno di questi metodi è chiamato Reluplex e impiegherebbe una ReLU Activation Function. Per verificare la rete neurale verrebbe anche usato un risolutore denominato Satisfiability Modulo Theory (SMT).
Nel campo del Neural Network Verification siamo ancora in fase di ricerca, con alcune sporadiche implementazioni di sistemi ben lontani dalle applicazioni in contesti di produzione.
A complicare ulteriormente la faccenda il problema ricade in una classe di problemi che, nella teoria della complessità computazionale, sono definita NP-Completi: tradotto in soldoni quanto più una rete risulti complessa e larga tanto più tempo è necessario per applicare la verifica.
ACAS Xu System: 45 deep neural networks
Reluplex è stato applicato con successo su un sistema denominato Airbone Collision-Avoidance Systems (ACAS) per droni svilupato dalla US Federal Aviation Administration (FAA).
L’ACAS Xu è compsoto da 45 reti neurali profonde. È cruciale che il loro comportamento rispecchi le specifiche di progettazione per evitare potenziali collisioni a mezz’aria.
Attraverso l’AI Verification è stato possibile provare formalmente il corretto comportamento della rete, per una lista di proprietà definite, identificando persino un bug.
Robustness to Adverarial Example
Un altro campo di applicazione è quello di verificare il comportamento della rete in presenza di Adversarial Example, dove è stato possibile dimostrare che piccole perturbazioni non erano in grado di ostacolare il normale funzionamento della rete.
AI Verification | GitHub Code
Ok direi che di teoria ne abbiamo fatta fin troppa.
A livello pratico?
Ripeto che la maggior parte del lavoro svolto è attualmente in fase di ricerca.
È comunque possibile trovare del codice online facente riferimento alle numerose pubblicazioni in merito.
Niente paura, ho fatto il lavoro al posto tuo.
Reluplex
Reluplex | Paper code implementation
A questo link possiamo trovare la documentazione e il codice (che andrebbe testato) per applicare le ricerche compiute. Possiamo usare Reluplex per testare 10 proprietà della rete ACAS Xu.
DiffAI
GitHub DiffAI v3 | Training DNN to be provably robust
DiffAI è un sistema per allenare le reti neurali artificiali (artificial neural networks) a essere validamente robuste e provare che effettivamente lo siano.
Persone da seguire:
Krishnamurthy Dvijotham | Reserach Scientist at DeepMind
Per approfondire:
