Mentre l’intelligenza artificiale rimodella lo sviluppo del software, una piccola startup afferma che il prossimo grande collo di bottiglia del settore non sarà scrivere codice, ma fare affidamento su di esso.
TeoremaUna società con sede a San Francisco creata da Y Combinator Primavera 2025 Batch ha annunciato martedì di aver raccolto 6 milioni di dollari in finanziamenti iniziali per creare strumenti automatizzati che verifichino l’accuratezza del software generato dall’intelligenza artificiale. Khosla Ventures ha condotto il tour con la partecipazione di Y Falegname, e14, SAIF, alcionee angel investor 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. Assistenti di codifica AI di aziende come GitHub, AmazzoniaE Google Ora produciamo miliardi di righe di codice ogni anno. L’adozione aziendale sta accelerando. Ma la capacità di verificare che il software scritto dall’intelligenza artificiale funzioni effettivamente come previsto non ha tenuto il passo; Ciò creò ciò che i fondatori del Teorema descrissero come espansione. "lacuna di sorveglianza" Minaccia le infrastrutture critiche, dai sistemi finanziari alle reti elettriche.
"Siamo già lì" Jason Gross, co-fondatore di Theorem, ha detto 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 riescano a verificarlo?
La tecnologia principale 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 prove. Questo approccio trasforma un processo che in passato 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 è stata limitata alle applicazioni più cruciali: sistemi avionici, controlli dei reattori nucleari e protocolli crittografici. Il costo proibitivo della tecnica (che spesso richiedeva otto righe di prova matematica per ogni riga di codice) la rendeva poco pratica per lo sviluppo di software tradizionale.
Gross lo sa in prima persona. Prima di fondare Theorem, ha conseguito il dottorato di ricerca al MIT, lavorando sul Teorema verificato. Il codice di crittografia che ora alimenta il protocollo di sicurezza HTTPS Manteniamo trilioni di connessioni Internet ogni giorno. Ha stimato che questo progetto ha consumato quindici anni-persona di lavoro.
"Nessuno sceglie di avere il codice sbagliato," Ha detto Gross. "In passato la verifica del software era antieconomica. Le prove sono state scritte da ingegneri di livello PhD. Ora tutti questi sono scritti dall’intelligenza artificiale."
In che modo la verifica formale rileva gli errori che i test tradizionali non rilevano?
Il sistema del teorema funziona secondo il principio delle chiamate lorde "analisi delle prove frazionarie." Invece di testare in modo esaustivo ogni possibile comportamento, cosa computazionalmente impossibile per software complessi, la tecnologia alloca risorse di verifica proporzionali all’importanza di ciascun componente del codice.
L’approccio ha recentemente identificato un bug sfuggito ai test di Anthropic, la società di sicurezza AI dietro il chatbot Claude. Gross ha affermato che la tecnica aiuta gli sviluppatori "Rileva rapidamente gli errori senza spendere troppi calcoli."
In una recente dimostrazione tecnica chiamata SFBench, Theorem ha utilizzato l’intelligenza artificiale per tradurre 1.276 problemi da Rocq (l’assistente di prova ufficiale) a Lean (un altro linguaggio di verifica) e poi ha dimostrato automaticamente che ogni traduzione era equivalente all’originale. L’azienda stima che un team di persone avrebbe bisogno di circa 2,7 anni-persona per completare lo stesso lavoro.
"Chiunque può eseguire gli agenti in parallelo, ma possiamo anche eseguirli in sequenza." Gross ha osservato che l’architettura di Theorem gestisce codice interconnesso in cui le soluzioni si basano l’una sull’altra su dozzine di file, il che guida i tradizionali agenti di codifica AI limitati da finestre di contesto.
Come ha fatto un’azienda a trasformare 1.500 pagine di specifiche in 16.000 righe di codice affidabile?
La startup sta attualmente lavorando con clienti nei laboratori di ricerca sull’intelligenza artificiale, sull’automazione della progettazione elettronica e sull’elaborazione accelerata da GPU. Un caso di studio dimostra il valore pratico della tecnologia.
Un cliente si è rivolto a Theorem con una specifica PDF di 1.500 pagine e un’applicazione software legacy afflitta da perdite di memoria, arresti anomali e altri bug sfuggenti. Il loro problema più urgente: aumentare le prestazioni da 10 megabit al secondo a 1 gigabit al secondo (un aumento di 100 volte) senza introdurre errori aggiuntivi.
Il sistema di Teorem ha generato 16.000 righe di codice di produzione che il cliente ha distribuito senza revisione manuale. Questa fiducia derivava da una specifica eseguibile compatta di poche centinaia di righe che generalizzava l’enorme documento PDF, abbinata a un hardware di controllo di parità che verificava che la nuova implementazione corrispondesse al comportamento previsto.
"Ora dispongono di un parser di livello produttivo in esecuzione a 1 Gbps che possono implementare con la certezza che nessuna informazione verrà persa durante l’analisi." Ha detto Gross.
Rischi per la sicurezza nascosti nel software generato dall’intelligenza artificiale per le infrastrutture critiche
L’annuncio del finanziamento arriva mentre i politici e gli esperti di tecnologia esaminano sempre più l’affidabilità dei sistemi di intelligenza artificiale implementati 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à con cui si evolve il software e la facilità con cui i bug sottili possono propagarsi.
Gross inquadra questa sfida in termini di sicurezza. Poiché l’intelligenza artificiale rende più economico individuare e sfruttare le vulnerabilità, i sostenitori hanno bisogno di ciò che lui chiama "difesa asimmetrica" — protezione scalabile senza aumenti proporzionati delle risorse.
"La sicurezza del software è un delicato equilibrio tra attacco e difesa." ha detto. "Con l’hacking dell’intelligenza artificiale, il costo dell’hacking di un sistema diminuisce drasticamente. L’unica soluzione valida è la difesa asimmetrica. Se vogliamo una soluzione di sicurezza software che possa sopravvivere a diverse generazioni di miglioramenti del modello, sarà attraverso la verifica."
Alla domanda se le autorità di regolamentazione avrebbero imposto la verifica formale del codice generato dall’intelligenza artificiale nei sistemi critici, Gross è andato dritto al punto: "Ora che la verifica formale è abbastanza economica, non utilizzarla per garantire garanzie sui sistemi critici potrebbe essere considerata una grave negligenza."
Cosa distingue Theorem dalle altre iniziative 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. Gross sostiene che la differenziazione dell’azienda risiede nel suo focus sull’ampliamento della sorveglianza del software piuttosto che sull’applicazione della verifica alla matematica o ad altri domini.
"I nostri strumenti sono utili per i team di ingegneria dei sistemi che lavorano vicino al metallo e necessitano di garanzia di precisione prima di unire le modifiche." ha detto.
Il team 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 sulla formazione di modelli di intelligenza artificiale che rafforzano la pipeline di convalida.
"Stiamo lavorando sul ragionamento formale del programma in modo che tutti possano non solo supervisionare il funzionamento di un’intelligenza artificiale al livello di un ingegnere informatico medio, ma anche sfruttare veramente le capacità di un’intelligenza artificiale al 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 team, aumentare le risorse informatiche per addestrare modelli di validazione ed entrare in nuovi settori come la robotica, l’energia rinnovabile, la criptovaluta e la sintesi di farmaci. Attualmente in azienda lavorano quattro persone.
L’emergere della nuova iniziativa segnala un cambiamento nel modo in cui i leader tecnologici aziendali dovrebbero valutare gli strumenti di codifica dell’intelligenza artificiale. La prima ondata di sviluppo basato sull’intelligenza artificiale prometteva un aumento della produttività; Più codice c’è, più veloce sarà. Il teorema scommette che la prossima ondata richiederà qualcosa di diverso: la prova matematica che la velocità non compromette la sicurezza.
Gross inquadra chiaramente i rischi. I sistemi di intelligenza artificiale stanno migliorando in modo esponenziale. Se questa tendenza continua, a suo avviso, l’ingegneria del software sovrumana sarà inevitabile: la capacità di progettare sistemi più complessi di qualsiasi cosa gli esseri umani abbiano mai costruito.
"E senza un’economia della sorveglianza completamente diversa," ha detto, "Metteremo in campo sistemi che non possiamo controllare."
Le macchine scrivono il codice. Ora qualcuno deve controllare il proprio lavoro.
