Tradizionalmente, la verifica del codice software è stata un processo ad alta intensità di lavoro che prevedeva revisioni manuali del codice o l'esecuzione del codice per identificare anomalie. Sebbene preziosi, questi metodi sono suscettibili all’errore umano e poco pratici per sistemi complessi.
Entra in Baldur, una soluzione meticolosamente progettata che sfrutta la potenza dei Large Language Models (LLM) per generare automaticamente dimostrazioni matematiche. Perfezionando i LLM su ampi contenuti matematici e il linguaggio Isabelle/HOL utilizzato per le dimostrazioni, Baldur compie un passo da gigante verso l'automazione di quello che una volta era un compito arduo. Il risultato? Un sistema che lavora in tandem con i dimostratori di teoremi per verificare la correttezza del codice riduce significativamente il margine di errore.
Al centro del successo di Baldur c'è la partnership con Thor, lo strumento responsabile della generazione automatica delle prove. Thor vanta una percentuale di successo del 57%, ma se combinato con Baldur, i due raggiungono una notevole precisione del 65,7% nella generazione di prove. Questo duo dinamico, ispirato alla mitologia norrena, dimostra il potenziale della verifica del software basata sull'intelligenza artificiale.
Sfide negli LLM
Una delle principali sfide incontrate quando si lavora con LLM, come ChatGPT, è la loro occasionale mancanza di correttezza. Invece di sollevare segnali d’allarme, potrebbero “fallire silenziosamente”, fornendo risultati errati che sembrano validi. Affrontare questo problema è fondamentale per garantire l’affidabilità delle prove generate dall’intelligenza artificiale.
Lo sviluppo di Baldur non è stata un'impresa da poco, poiché ha richiesto diversi mesi e uno sforzo di collaborazione con Google. Emily First, l'autrice principale del progetto, ha impiegato Minerva , una LLM addestrata in un vasto corpus di testi in linguaggio naturale. Successivamente, Minerva è stato messo a punto su un consistente set di dati da 118 GB di articoli matematici e scientifici e contenuti web contenenti espressioni matematiche. Tuttavia, l’elemento chiave di differenziazione è stato l’ulteriore perfezionamento del linguaggio Isabelle/HOL, ponendo le basi per la generazione di dimostrazioni matematiche complete.
L'approccio di Baldur alla correzione degli errori è ingegnoso. Quando il dimostratore di teoremi identifica un errore in una dimostrazione generata, restituisce queste informazioni a Baldur, consentendo al sistema di imparare dai propri errori. Questo processo iterativo migliora l'accuratezza e l'affidabilità delle prove, rendendolo uno strumento altamente efficace per la verifica del codice.
Un futuro promettente per il software privo di bug
Anche se c’è margine di miglioramento, Baldur rappresenta una strada promettente per la verifica formale del software. Gli ingegneri sono ancora responsabili dello sviluppo del software, ma ora hanno un potente alleato sotto forma di Baldur, capace di automatizzare la creazione di dimostrazioni matematiche.
Yuriy Brun, professore al Manning College of Information and Computer Sciences dell’UMass Amherst, ha osservato: “Il nostro lavoro si concentra sul tentativo di automatizzare la scrittura di queste dimostrazioni. Baldur utilizza modelli linguistici di grandi dimensioni per, dato un teorema matematico, generare automaticamente una dimostrazione di quel teorema che un dimostratore di teoremi può quindi verificare.
Il successo di Baldur è attribuito al team dedicato che ha lavorato instancabilmente su questo progetto. Oltre a Emily First, Markus Rabe, che all’epoca lavorava per Google, e Talia Ringer, assistente professore presso l’Università dell’Illinois-Urbana Champaign, hanno contribuito in modo significativo. La Defense Advanced Research Projects Agency (DARPA) e la National Science Foundation (NSF) hanno sostenuto il progetto.
Soluzioni innovative come Baldur offrono speranza mentre l’industria tecnologica è alle prese con la crescente complessità dei sistemi software. Con le capacità dell'intelligenza artificiale in continua evoluzione e maturazione, il potenziale di Baldur nel portare la correttezza del software a nuovi livelli rimane promettente.