Google DeepMind ha introdotto AlphaProof Code, un sistema che porta la verifica formale del software a un livello di profondità finora difficile da raggiungere. Nel caso mostrato, gli agenti hanno scritto circa tre milioni di righe di prove in Lean per verificare la crittografia core di Signal.
Che cos’è la verifica formale
Verificare formalmente un programma significa dimostrare, con la matematica, che si comporta come previsto in ogni condizione: non basta che i test passino, occorre una prova che non lasci spazio a casi non considerati. È un’attività preziosa per il software critico, ma tradizionalmente lenta e costosa, perché richiede esperti e molto tempo.
Proprio il costo elevato ha finora limitato la verifica formale a pochi componenti essenziali. Ampliare questa pratica a più porzioni di software richiede un cambio di scala che, secondo DeepMind, l’IA può favorire riducendo il lavoro ripetitivo e la necessità di revisione manuale riga per riga.
Il ruolo dell’IA
AlphaProof Code affronta il collo di bottiglia: generare e controllare prove. Se l’intelligenza artificiale riesce a redigere dimostrazioni corrette e verificabili, il lavoro umano si sposta sulla definizione di cosa va dimostrato e sulla revisione dei risultati. Questo potrebbe rendere accessibile la verifica formale a porzioni di software che oggi ne restano fuori.
L’aspetto interessante è la combinazione: la macchina produce, il verificatore controlla e l’essere umano orienta. È un modello di collaborazione che ridimensiona il rischio di errori senza rinunciare al giudizio, e che può essere applicato anche a parti di codice aziendale sensibile.
Perché Signal è un caso significativo
Le librerie crittografiche sono il cuore della riservatezza delle comunicazioni: un difetto lì ha conseguenze enormi. Avere prove formali sul loro funzionamento rafforza la fiducia non solo degli utenti, ma anche di chi valuta la sicurezza di prodotti e servizi. È un esempio di come l’IA possa servire la robustezza, non solo la rapidità.
Prospettive per le imprese
Non tutte le aziende hanno bisogno di prove formali, ma il principio è trasferibile: usare l’IA per alzare l’asticella della qualità su componenti sensibili. Man mano che questi strumenti maturano, potrebbero entrare nei processi di sviluppo come ausilio alla revisione dei pezzi più delicati, riducendo il tempo tra l’idea e una versione affidabile.
Un cambio di prospettiva
Tradizionalmente la qualità del software si affida ai test, che verificano alcuni casi ma non tutti. La verifica formale sposta l’attenzione sulla dimostrazione: se una proprietà è provata, vale per ogni esecuzione consentita. È un cambio di prospettiva che incide anche su come si progetta e si mantiene il codice.
L’IA, in questo quadro, non sostituisce il rigore ma ne abbassa il costo, rendendo sostenibile un lavoro che prima richiedeva mesi di specialisti e risorse difficili da reperire.
In sintesi
AlphaProof Code mostra che l’IA può rendere praticabile la verifica formale di software critico. È un passo verso sistemi più affidabili, dove la correttezza è dimostrata e non solo sperata. Ada Consulting osserva queste evoluzioni per orientare le organizzazioni verso scelte tecnologiche solide.
Fonte: Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (Google DeepMind)
https://deepmind.google/blog/introducing-alphaproof-code/