Mentre l’intelligenza artificiale rimodella lo sviluppo del software program, una piccola startup scommette che il prossimo grande collo di bottiglia del settore non sarà la scrittura di codice: si fiderà di esso.
Teoremauna società con sede a San Francisco emersa da Y Combinator’s Primavera 2025 batch, ha annunciato martedì di aver raccolto 6 milioni di dollari in finanziamenti iniziali per costruire strumenti automatizzati che verifichino la correttezza del software program generato dall’intelligenza artificiale. Khosla Ventures ha condotto il spherical, con la partecipazione di Combinatore Y, e14, SAIF, Halcyone angel investor tra cui Blake Borgesson, co-fondatore di Recursion Prescription drugs, e Arthur Breitman, co-fondatore della piattaforma blockchain Tezos.
L’investimento arriva in un momento cruciale. Assistenti di codifica AI di aziende come GitHub, AmazzoniaE Google ora generano miliardi di righe di codice ogni anno. L’adozione aziendale sta accelerando. Ma la capacità di verificare che il software program scritto dall’intelligenza artificiale funzioni effettivamente come previsto non ha tenuto il passo, creando quello che i fondatori di Theorem descrivono come un “divario di supervisione” sempre più ampio che minaccia le infrastrutture critiche, dai sistemi finanziari alle reti elettriche.
“Ci siamo già”, ha detto Jason Gross, co-fondatore di Theorem, quando abbiamo chiesto se il codice generato dall’intelligenza artificiale sta superando la capacità di revisione umana. “Se mi chiedessi di rivedere 60.000 righe di codice, non saprei come farlo.”
Perché l’intelligenza artificiale scrive il codice più velocemente di quanto gli esseri umani possano verificarlo
La tecnologia principale di Theorem combina la verifica formale – una tecnica matematica che dimostra che il software program si comporta esattamente come specificato – con modelli di intelligenza artificiale addestrati a generare e verificare automaticamente le show. L’approccio trasforma un processo che storicamente richiedeva anni di ingegneria a livello di dottorato 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ù cruciali: sistemi avionici, controlli dei reattori nucleari e protocolli crittografici. Il costo proibitivo della tecnica, che spesso richiedeva otto righe di show matematiche per ogni singola riga di codice, la rendeva poco pratica per lo sviluppo di software program tradizionale.
Gross lo sa in prima persona. Prima di fondare Theorem, ha conseguito il dottorato di ricerca al MIT lavorando sulla verifica codice di crittografia che ora alimenta il protocollo di sicurezza HTTPS proteggere trilioni di connessioni Web ogni giorno. Quel progetto, secondo le sue stime, ha consumato quindici anni-persona di lavoro.
“Nessuno preferisce avere un codice errato”, ha detto Gross. “Prima la verifica del software program non period economica. Le show venivano scritte da ingegneri di livello PhD. Ora, l’intelligenza artificiale scrive tutto.”
In che modo la verifica formale rileva i bug che i check tradizionali non rilevano
Il sistema del teorema funziona secondo un principio che Gross chiama “decomposizione con prova frazionaria”. Invece di testare in modo esaustivo ogni possibile comportamento – computazionalmente irrealizzabile per software program complessi – la tecnologia alloca risorse di verifica proporzionalmente all’importanza di ciascun componente del codice.
L’approccio ha recentemente identificato un bug che è sfuggito ai check di Anthropic, la società di sicurezza AI dietro il chatbot Claude. Gross ha affermato che la tecnica aiuta gli sviluppatori a “rilevare i propri bug ora senza spendere molto in termini di calcolo”.
In una recente dimostrazione tecnica chiamata SFBench, Theorem ha utilizzato l’intelligenza artificiale per tradurre 1.276 problemi da Rocq (un assistente di prova formale) a Lean (un altro linguaggio di verifica), quindi ha dimostrato automaticamente che ciascuna traduzione è equivalente all’originale. L’azienda stima che un crew umano avrebbe richiesto circa 2,7 anni-persona per completare lo stesso lavoro.
“Tutti possono eseguire agenti in parallelo, ma siamo anche in grado di eseguirli in sequenza”, ha spiegato Gross, sottolineando che l’architettura di Theorem gestisce codice interdipendente – in cui le soluzioni si basano l’una sull’altra su dozzine di file – che fa inciampare agenti di codifica AI convenzionali limitati da finestre di contesto.
Come un’azienda ha trasformato una specifica di 1.500 pagine in 16.000 righe di codice affidabile
La startup sta già lavorando 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 program legacy afflitta da perdite di memoria, arresti anomali e altri bug sfuggenti. 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 ulteriori errori.
Il sistema di Theorem ha generato 16.000 righe di codice di produzione, che il cliente ha implementato senza mai rivederlo manualmente. La fiducia proveniva da una specifica eseguibile compatta – poche centinaia di righe che generalizzava l’enorme documento PDF – abbinata a un sistema di controllo dell’equivalenza che verificava che la nuova implementazione corrispondesse al comportamento previsto.
“Ora hanno un parser di livello produttivo che opera a 1 Gbps che possono implementare con la certezza che nessuna informazione verrà persa durante l’analisi”, ha affermato Gross.
I rischi per la sicurezza in agguato nel software program generato dall’intelligenza artificiale per le infrastrutture critiche
L’annuncio del finanziamento arriva mentre politici e tecnologi esaminano sempre più attentamente l’affidabilità dei sistemi di intelligenza artificiale incorporati nelle infrastrutture critiche. Il software program controlla già i mercati finanziari, i dispositivi medici, le reti di trasporto e le reti elettriche. L’intelligenza artificiale sta accelerando la velocità con cui il software program si evolve e la facilità con cui i bug sottili 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”: una protezione scalabile senza aumenti proporzionali delle risorse.
“La sicurezza del software program è un delicato equilibrio tra attacco e difesa”, ha affermato. “Con l’hacking basato sull’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 software program che possa durare per più di qualche generazione di miglioramenti del modello, sarà tramite la verifica.”
Alla domanda se i regolatori debbano 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 grave negligenza non usarla per garanzie sui sistemi critici”.
Ciò che distingue Theorem dalle altre startup di verifica del codice AI
Theorem 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 program piuttosto che all’applicazione della verifica alla matematica o advert altri domini.
“I nostri strumenti sono utili per i crew di ingegneria dei sistemi, che lavorano vicino al metallo, e che necessitano di garanzie di correttezza prima di unire le modifiche”, ha affermato.
Il crew fondatore riflette questo orientamento tecnico. Gross apporta una profonda esperienza nella teoria dei linguaggi di programmazione e una comprovata esperienza nell’implementazione di codice verificato nella produzione su larga scala. Il co-fondatore Rajashree Agrawal, un ingegnere ricercatore sull’apprendimento automatico, si concentra sull’addestramento dei modelli di intelligenza artificiale che alimentano la pipeline di verifica.
“Stiamo lavorando sul ragionamento formale del programma in modo che tutti possano supervisionare non solo il lavoro di un’intelligenza artificiale media a livello di ingegnere del software program, ma sfruttare davvero le capacità di un’intelligenza artificiale a livello di Linus Torvalds”, ha detto Agrawal, riferendosi al leggendario creatore di Linux.
La corsa per verificare il codice AI prima che controlli tutto
Teorema prevede di utilizzare i finanziamenti per espandere il proprio crew, aumentare le risorse di calcolo per i modelli di verifica della formazione e spingersi verso nuovi settori tra cui robotica, energia rinnovabile, criptovaluta e sintesi di farmaci. Attualmente l’azienda impiega quattro persone.
L’emergere della startup segnala un cambiamento nel modo in cui i chief tecnologici aziendali potrebbero aver bisogno di valutare gli strumenti di codifica dell’intelligenza artificiale. La prima ondata di sviluppo assistito dall’intelligenza artificiale prometteva guadagni di produttività: più codice, più velocemente. Il teorema è scommettere che la prossima ondata richiederà qualcosa di diverso: la prova matematica che la velocità non va a scapito della sicurezza.
Gross inquadra la posta in gioco in termini crudi. I sistemi di intelligenza artificiale stanno migliorando in modo esponenziale. Se questa traiettoria dovesse reggere, ritiene che l’ingegneria del software program sovrumana sia inevitabile, capace di progettare sistemi più complessi di qualsiasi cosa gli esseri umani abbiano mai costruito.
“E senza un’economia di supervisione radicalmente diversa”, ha detto, “finiremo per implementare sistemi che non controlliamo”.
Le macchine stanno scrivendo il codice. Ora qualcuno deve controllare il loro lavoro.
