Affrontare la sicurezza dell’intelligenza artificiale partendo da una domanda geometrica: e se la robustezza di un classificatore si potesse mappare su un problema di attraversamento di un reticolo? Il lavoro “Interval Certifications for Multilayered Perceptrons via Lattice Traversal” prende proprio questa strada, e nel farlo scardina alcune ipotesi consolidate. Non si parla di testing empirico contro attacchi avversari, ma di una garanzia formale che un input possa oscillare all’interno di un intervallo – un iper-rettangolo allineato agli assi – senza che la predizione della rete cambi. Chiamano questa “certificazione sound”, ed è il cuore della robustezza avversariale nota. Ma c’è un rovescio della medaglia: gli autori definiscono anche la “certificazione completa”, dove l’uscita dall’intervallo comporta per forza il cambio di predizione. Questo lato non era mai stato formalizzato in letteratura, e rivela asimmetrie profonde.

Tradotto in pratica: mentre la certificazione sound (qual è la massima zona sicura?) si scontra con una forte intrattabilità computazionale, la certificazione completa (qual è la minima zona che contiene il punto e garantisce il cambio di classe fuori?) ammette un algoritmo con numero polinomiale di chiamate a un oracolo. In altre parole, possiamo calcolare in modo efficiente la “stretta di sicurezza” intorno a un input, ma non possiamo determinare la massima estensione di quella sicurezza senza costi proibitivi. Per chi opera in contesti on-premise, con modelli auto-ospitati su hardware proprietario e dati sensibili, questo cambia le carte in tavola. La verifica formale non è più un esercizio accademico: diventa uno strumento per delimitare con precisione matematica le condizioni operative in cui un modello rimane affidabile, un requisito sempre più richiesto da regolamentazioni come l’AI Act europeo per i sistemi ad alto rischio.

Il meccanismo si basa su operatori di lattice traversal applicati in uno schema iterativo di raffinamento e verifica (refine & verify). Usando verificatori formali per MLP, gli intervalli prodotti sono massimali in senso sound e minimali in senso completo, con garanzie forti. Il sistema ParallelepipedoNN, sviluppato per la valutazione empirica, mostra la fattibilità dell’approccio. Aggiungendo l’analisi degli intervalli simmetrici – le sfere in norma L-infinito – emergono algoritmi logaritmici che rendono l’intero processo scalabile.

Questo non è solo un avanzamento teorico. Sposta gli equilibri per chi sviluppa o adotta AI in modalità self-hosted. Invece di affidarsi a benchmark di robustezza forniti da terze parti, spesso opachi e basati su campioni limitati, un’azienda potrebbe eseguire localmente la certificazione completa dei propri modelli, ottenendo una mappa delle regioni di input dove il modello si comporta in modo prevedibile. La sovranità sui dati si estende così alla sovranità sulla fiducia computazionale: è il proprio verificatore a dire, senza mediazioni, quali perturbazioni sono innocue e quali no. E la scoperta che le certificazioni complete siano computazionalmente più abbordabili delle sound suggerisce una strada pragmatica: invece di inseguire il confine massimo di invarianza, ci si accontenta di una regione ristretta ma dimostrabilmente sicura – abbastanza per moltissimi scenari industriali (diagnostica medica, controllo di processo, sorveglianza di infrastrutture critiche) dove un margine di perturbazione controllato è tutto ciò che serve.

La ricerca tocca anche il tema delicato dell’asimmetria tra i due tipi di certificazione. Mentre la complete certification trova soluzioni minime in tempo polinomiale, la sound certification è dimostrata fortemente intrattabile. Questo ribalta l’enfasi tipica della comunità: non più solo “quanto è robusto il mio modello?”, ma “entro quale intorno posso certificare che il modello non sbaglierà mai?”. Per i decisori IT, significa spostare l’investimento dalla ricerca del modello più resistente agli attacchi a quello più verificabile, un cambiamento di prospettiva che potrebbe influenzare l’architettura stessa delle reti future, privilegiando strutture lineari a tratti (come le MLP) più adatte alla verifica formale.

Sullo sfondo, la crescente pressione per auditabilità e trasparenza spinge l’adozione di strumenti come ParallelepipedoNN. In un’infrastruttura on-premise, dove il controllo è totale, integrare un layer di certificazione formale nel ciclo di deployment significa poter rispondere a requisiti normativi con evidenze matematiche, non con narrative di marketing. È la differenza tra dire “il nostro modello ha superato un test” e “possiamo provare che entro questo raggio di perturbazione non fallirà”.