VB,M.Nuñez
Mentre l’intelligenza artificiale sta rimodellando lo sviluppo del software, una piccola startup scommette che il prossimo grande ostacolo del settore non sarà la scrittura del codice, ma la fiducia in esso.Theorem , un’azienda con sede a San Francisco nata dal gruppo di Y Combinator della primavera 2025 , ha annunciato martedì di aver raccolto 6 milioni di dollari in finanziamenti iniziali per sviluppare strumenti automatizzati che verifichino la correttezza del software generato dall’intelligenza artificiale.
Khosla Ventures ha guidato il round, con la partecipazione di Y Combinator , e14 , SAIF , Halcyon e investitori informali tra cui Blake Borgesson, co-fondatore di Recursion Pharmaceuticals, e Arthur Breitman, co-fondatore della piattaforma blockchain Tezos.L’investimento arriva in un momento cruciale. Gli assistenti di programmazione basati sull’intelligenza artificiale di aziende come GitHub , Amazon e Google generano ormai miliardi di righe di codice all’anno. L’adozione da parte delle aziende sta accelerando. Ma la capacità di verificare che il software scritto con l’intelligenza artificiale funzioni effettivamente come previsto non ha tenuto il passo, creando quello che i fondatori di Theorem descrivono come un crescente “divario di supervisione” che minaccia infrastrutture critiche, dai sistemi finanziari alle reti elettriche.Continua a guardare5Breaking the Memory Wall: The Infrastructure Required for Statefulness”Ci siamo già”, ha affermato Jason Gross, co-fondatore di Theorem, quando gli abbiamo chiesto se il codice generato dall’intelligenza artificiale stia superando la capacità di revisione umana. “Se mi chiedessero di revisionare 60.000 righe di codice, non saprei come farlo”.Perché l’intelligenza artificiale scrive il codice più velocemente di quanto gli esseri umani possano verificarloLa tecnologia di base di Theorem combina la verifica formale – una tecnica matematica che dimostra che il software si comporta esattamente come specificato – con modelli di intelligenza artificiale addestrati a generare e verificare automaticamente le dimostrazioni. L’approccio trasforma un processo che storicamente richiedeva anni di ingegneria di livello dottorale in qualcosa che l’azienda sostiene possa essere completato in settimane o addirittura giorni.La verifica formale esiste da decenni, ma è rimasta confinata alle applicazioni più critiche: sistemi avionici, controlli di reattori nucleari e protocolli crittografici. Il costo proibitivo della tecnica – che spesso richiedeva otto righe di dimostrazione matematica per ogni singola riga di codice – la rendeva impraticabile per lo sviluppo software tradizionale.Gross lo sa in prima persona.
Prima di fondare Theorem, ha conseguito il dottorato di ricerca al MIT lavorando sul codice crittografico verificato che ora alimenta il protocollo di sicurezza HTTPS, proteggendo ogni giorno migliaia di miliardi di connessioni Internet. Quel progetto, secondo le sue stime, ha richiesto quindici anni-uomo di lavoro.”Nessuno preferisce avere codice errato”, ha detto Gross. “Prima la verifica del software non era economica. Un tempo le dimostrazioni venivano scritte da ingegneri con un dottorato di ricerca. Ora, è l’intelligenza artificiale a scriverle tutte.”Come la verifica formale rileva i bug che i test tradizionali non rilevanoIl sistema di Theorem funziona secondo un principio che Gross chiama “scomposizione frazionaria della prova”.
Anziché testare in modo esaustivo ogni possibile comportamento, computazionalmente irrealizzabile per software complessi, la tecnologia alloca le risorse di verifica in modo proporzionale all’importanza di ciascun componente del codice.L’approccio ha recentemente identificato un bug sfuggito ai test di Anthropic, l’azienda di sicurezza informatica che ha sviluppato il chatbot Claude. Gross ha affermato che la tecnica aiuta gli sviluppatori a “individuare i bug immediatamente senza dover spendere molto in termini di elaborazione”.In una recente dimostrazione tecnica chiamata SFBench, Theorem ha utilizzato l’intelligenza artificiale per tradurre 1.276 problemi da Rocq (un assistente di verifica formale) a Lean (un altro linguaggio di verifica), quindi ha automaticamente dimostrato che ogni traduzione era equivalente all’originale. L’azienda stima che un team umano avrebbe impiegato circa 2,7 anni-persona per completare lo stesso lavoro.
“Tutti possono eseguire agenti in parallelo, ma noi siamo anche in grado di eseguirli in sequenza”, ha spiegato Gross, osservando che l’architettura di Theorem gestisce codice interdipendente, in cui le soluzioni si basano l’una sull’altra su decine di file, che fa inciampare gli agenti di codifica AI convenzionali limitati dalle finestre di contesto.Come un’azienda ha trasformato una specifica di 1.500 pagine in 16.000 righe di codice affidabileLa startup sta già collaborando con clienti nei laboratori di ricerca sull’intelligenza artificiale, nell’automazione della progettazione elettronica e nel calcolo accelerato da GPU. Un caso di studio illustra il valore pratico della tecnologia.
Un cliente si è rivolto a Theorem con una specifica PDF di 1.500 pagine e un’implementazione software legacy afflitta da perdite di memoria, crash e altri bug elusivi. Il loro problema più urgente: migliorare le prestazioni da 10 megabit al secondo a 1 gigabit al secondo – un aumento di 100 volte – senza introdurre errori aggiuntivi.Il sistema di Theorem ha generato 16.000 righe di codice di produzione, che il cliente ha implementato senza mai revisionarlo manualmente. La sicurezza derivava da una specifica eseguibile compatta – poche centinaia di righe che generalizzavano l’enorme documento PDF – abbinata a un sistema di controllo di equivalenza che verificava che la nuova implementazione corrispondesse al comportamento previsto.”Ora dispongono di un parser di livello produttivo che funziona a 1 Gbps e che possono implementare con la certezza che nessuna informazione verrà persa durante l’analisi”, ha affermato Gross.
I rischi per la sicurezza nascosti nei software generati dall’intelligenza artificiale per le infrastrutture criticheL’annuncio del finanziamento arriva mentre i decisori politici e gli esperti di tecnologia esaminano sempre più attentamente l’affidabilità dei sistemi di intelligenza artificiale integrati nelle infrastrutture critiche. Il software controlla già i mercati finanziari, i dispositivi medici, le reti di trasporto e le reti elettriche. L’intelligenza artificiale sta accelerando la velocità di evoluzione di questo software e la facilità con cui bug subdoli possono propagarsi.Gross inquadra la sfida in termini di sicurezza. Poiché l’intelligenza artificiale rende più economico individuare e sfruttare le vulnerabilità, i difensori hanno bisogno di quella che lui chiama “difesa asimmetrica”, ovvero una protezione scalabile senza aumenti proporzionali delle risorse.”La sicurezza del software è un delicato equilibrio tra attacco e difesa”, ha affermato. “Con l’hacking dell’intelligenza artificiale, il costo dell’hacking di un sistema sta diminuendo drasticamente.
L’unica soluzione praticabile è la difesa asimmetrica. Se vogliamo una soluzione di sicurezza del software che possa durare per più di qualche generazione di miglioramenti del modello, la scelta dovrà ricadere sulla verifica”.Alla domanda se gli enti regolatori dovessero imporre una verifica formale per il codice generato dall’intelligenza artificiale nei sistemi critici, Gross ha offerto una risposta precisa: “Ora che la verifica formale è abbastanza economica, potrebbe essere considerata una grave negligenza non utilizzarla per le garanzie sui sistemi critici”.
Cosa distingue Theorem dalle altre startup di verifica del codice AITheorem entra in un mercato in cui numerose startup e laboratori di ricerca stanno esplorando l’intersezione tra intelligenza artificiale e verifica formale. La differenziazione dell’azienda, sostiene Gross, risiede nella sua particolare attenzione alla scalabilità della supervisione del software, piuttosto che all’applicazione della verifica alla matematica o ad altri domini.”I nostri strumenti sono utili per i team di ingegneria dei sistemi che lavorano a stretto contatto con il metallo e che necessitano di garanzie di correttezza prima di unire le modifiche”, ha affermato.
Il team fondatore riflette questo orientamento tecnico. Gross porta con sé una profonda competenza nella teoria dei linguaggi di programmazione e una comprovata esperienza nell’implementazione di codice verificato in produzione su larga scala. Il co-fondatore Rajashree Agrawal, ingegnere di ricerca specializzato in apprendimento automatico, si concentra sull’addestramento dei modelli di intelligenza artificiale che alimentano la pipeline di verifica.
“Stiamo lavorando sul ragionamento formale dei programmi in modo che tutti possano supervisionare non solo il lavoro di un’intelligenza artificiale di livello medio, come un ingegnere del software, ma sfruttare davvero le capacità di un’intelligenza artificiale di livello Linus Torvalds”, ha affermato Agrawal, riferendosi al leggendario creatore di Linux.
La corsa per verificare il codice dell’intelligenza artificiale prima che controlli tuttoTheorem prevede di utilizzare il finanziamento per espandere il proprio team, aumentare le risorse di calcolo per l’addestramento dei modelli di verifica e penetrare nuovi settori, tra cui robotica, energie rinnovabili, criptovalute e sintesi di farmaci. L’azienda impiega attualmente quattro persone.L’emergere della startup segnala un cambiamento nel modo in cui i leader tecnologici aziendali potrebbero dover valutare gli strumenti di programmazione basati sull’intelligenza artificiale. La prima ondata di sviluppo assistito dall’intelligenza artificiale prometteva guadagni di produttività: più codice, più velocemente. Theorem scommette che la prossima ondata richiederà qualcosa di diverso: la dimostrazione matematica che la velocità non va a discapito della sicurezza.Gross definisce la posta in gioco in termini netti.
I sistemi di intelligenza artificiale stanno migliorando in modo esponenziale. Se questa tendenza si mantiene, ritiene che l’ingegneria del software sovrumana sia inevitabile, in grado di progettare sistemi più complessi di qualsiasi cosa gli esseri umani abbiano mai costruito.”E senza un’economia di controllo radicalmente diversa”, ha affermato, “finiremo per implementare sistemi che non controlliamo”.
Le macchine stanno scrivendo il codice. Ora qualcuno deve controllare il loro lavoro.