Anthropic, insieme al partner Theorem, ha usato il modello di IA Claude per dimostrare matematicamente che il codice software esistente funziona correttamente. L’analisi ha riguardato 123 librerie open source incluse nel progetto di sicurezza OSS-Fuzz di Google. In poche settimane sono state generate circa 180 milioni di righe di codice per le dimostrazioni e, a quanto riferito, sono stati individuati anche centinaia di bug sfuggiti ai test tradizionali.
La distanza tra «ha superato i test» e «ne è stata dimostrata la correttezza»
Quando si parla di verificare la qualità del software, molti pensano ai test: si forniscono gli input predisposti e si controlla che il programma restituisca i risultati attesi. Ma i test verificano soltanto ciò che è stato provato. Non dicono come si comporterà il software in situazioni che non sono state testate.
È qui che entra in gioco la verifica formale. Il comportamento di un programma viene trattato come un problema matematico e si dimostra che, entro le condizioni stabilite, funzionerà sempre correttamente. In teoria è un approccio potente, ma richiedeva una quantità di lavoro enorme. Si stima che la verifica del piccolo kernel di sistema operativo seL4 abbia richiesto a un’équipe di esperti un totale di 20 anni-persona di lavoro. Non sorprende che il suo impiego sia rimasto limitato a casi estremi, come il software di controllo degli aerei di linea.
Questa volta l’Anthropic Frontier Red Team ha collaborato con Theorem e ha affidato a Claude il lavoro di dimostrazione. Non gli è stato chiesto di scrivere nuovo codice: il modello ha esaminato software già esistente, ha trasformato i test per individuare i crash in problemi matematici, ha analizzato anche il codice macchina prodotto dalla compilazione e ha assemblato un gran numero di dimostrazioni.
A valutare le dimostrazioni è un programma indipendente
Se un’IA dichiara «promossa» una dimostrazione che ha scritto da sé, non è molto convincente. È interessante, sotto questo aspetto, il sistema di valutazione adottato: un programma di verifica indipendente chiamato Rocq controlla automaticamente le dimostrazioni generate. Secondo Anthropic, il processo richiede pochissimo intervento da parte di revisori umani.
Il gruppo di ricerca definisce il sistema una generazione di dimostrazioni «completamente autonoma». Gli strumenti usati per le dimostrazioni e le basi formali, tuttavia, sono stati realizzati da persone di Theorem. Più che dire che l’IA abbia creato tutto da zero, è probabilmente più corretto affermare che, su un terreno preparato dagli esseri umani, è riuscita a scrivere in una volta sola una quantità enorme di dimostrazioni.
Centinaia di bug scoperti durante le dimostrazioni
Nel corso delle dimostrazioni Claude si è imbattuto in centinaia di bug ed è stato autorizzato anche a correggerli autonomamente. Secondo i ricercatori, molti emergevano soltanto in condizioni molto specifiche, per esempio con file di input estremamente grandi o con gli accessi alla memoria eseguiti in un determinato ordine. Non c’è da stupirsi che riuscissero a sfuggire ai test ordinari.
Sono stati citati anche casi concreti. Durante la verifica di un lettore PDF molto diffuso, in una settimana sono stati individuati tanti bug di sicurezza quanti quel software ne registra normalmente in un anno. In un’altra applicazione è stato scoperto un errore logico che era rimasto inosservato per oltre 10 anni.
C’è un altro aspetto da non trascurare: cosa succede se la dimostrazione non arriva a compimento. Anthropic spiega che, anche quando una dimostrazione fallisce, durante il tentativo possono emergere bug reali. Le dimostrazioni, quindi, non servono soltanto a ottenere un «certificato di conformità», ma possono anche fungere da strumento di esplorazione per portare alla luce i bug. Più che sostituire i test ordinari, sembrano un modo per colmarne le lacune.
Non fraintendere la portata di «verificato formalmente»
Tuttavia, è rischioso interpretare «verificato formalmente» come «privo di difetti». Anthropic stessa riconosce che la dimostrazione vale soltanto entro condizioni rigorose. Si presuppongono una specifica configurazione del processore, programmi eseguiti con un solo thread e input inferiori a 64 MB. Le librerie usate nella realtà funzionano invece su hardware e con impostazioni diverse.
Anche i costi non sono trascurabili. In alcuni casi, per una singola dimostrazione si possono usare centinaia di milioni di token. Il costo complessivo del progetto non è stato reso noto. Un piccolo esperimento aggiuntivo ha però mostrato che le dimostrazioni possono essere riutilizzate, e si osserva una tendenza a una maggiore efficienza con i modelli più recenti. Per risolvere metà delle dimostrazioni, Opus 5.5 avrebbe bisogno di circa il 40% di token in meno rispetto a Opus 5.
La domanda non è più «l’IA sa programmare?»
Se l’IA è in grado di scrivere codice e di garantirne la correttezza entro determinate condizioni, cambia il modo di porre la domanda. Non più «l’IA sa programmare?», ma «l’IA sa dimostrare la sicurezza del codice che ha scritto?». Per i team di sviluppo preoccupati per l’affidabilità del codice generato dall’IA, questo cambiamento non è di poco conto. Se l’IA riuscisse a verificare da sola il proprio codice, potrebbe ridurre il carico delle revisioni umane e contribuire a tagliare i costi non solo della verifica, ma dell’intero processo di sviluppo.
Anthropic prevede che, nel prossimo futuro, la verifica formale tramite IA diventerà una pratica comune quanto i test tradizionali. La roadmap di Theorem include software di infrastruttura critica come glibc, OpenSSL e cURL.
Ciò che conta davvero, qui, è saper leggere le «premesse» della dimostrazione, non il suo contenuto. In quale ambiente è stata elaborata e quali input presuppone? In un’epoca in cui affidiamo all’AI anche le verifiche, la capacità degli esseri umani di esaminare queste premesse sembra destinata a essere l’ultimo baluardo della sicurezza.
コメント