Introduzione
L’IA generativa e in particolare i modelli linguistici di grandi dimensioni si sono dimostrati una tecnologia interessante per la comprensione e l’analisi sia del testo che del codice sorgente.
Spazio IT sta sperimentando questa tecnologia dall’inizio del 2023 ed alcuni risultati di questa ricerca sono stati presentati alla 28ma Ada-Europe International Conference on Reliable Software Technologies a giugno 2024.
Verifica del software
La verifica del software comporta la lettura e l’analisi di grandi se non enormi set di documenti e basi di codice. Sia i documenti che le fonti possono essere descritti come elenco di «cose», elenco di «oggetti», ad esempio:
- Una specifica di sistema (RS) è un elenco di requisiti di sistema
- Una Specifica Software è un elenco di Requisiti Software
- Un DDF è un elenco di componenti architettonici
- Una base di codice è un elenco di unità di compilazione
- Le unità di compilazione sono un elenco di classi, procedure e funzioni (naturalmente i nomi effettivi di queste «cose» dipendono dal linguaggio di programmazione).
Tutte le «cose» in una lista sono identificate da una sorta di «ID». Le liste sono di solito a diversi livelli di astrazione, ad esempio una lista di specifiche implementa una lista di requisiti. Le informazioni di tracciabilità legano insieme, stabiliscono una relazione tra «cose» solitamente appartenenti a liste a diversi livelli di astrazione, ad esempio:
requisiti –> design –> codice sorgente
I controlli automatici di tracciabilità hanno funzionato (finora) solo a livello di «ID».
L’IA generativa apre nuove opportunità per una corrispondenza semantica.
Modelli linguistici locali/isolati
Quando gli utenti utilizzano sistemi di intelligenza artificiale generativa come ChatGPT di OpenAI, Gemini di Google o altri forniti gratuitamente dalle principali aziende tecnologiche, non vi è alcuna garanzia che i dati che inseriscono, ovvero il contenuto, in particolare le informazioni all’interno dei prompt, rimangano riservati.
È sempre possibile creare registrazioni commerciali o accordi contrattuali che vietino al fornitore di servizi di conservare e sfruttare i contenuti degli utenti, ma si tratta solo di garanzie commerciali. L’unico metodo per gli utenti per garantire che i loro contenuti non vengano utilizzati in modo improprio è utilizzare esclusivamente modelli open source (con una conoscenza approfondita delle loro funzioni) e gestire questi modelli su una piattaforma informatica privata e locale, completamente isolata e protetta.
I modelli linguistici di grandi dimensioni richiedono enormi risorse computazionali. Per essere in grado di eseguire questi modelli su piattaforme di calcolo locali ed economiche viene utilizzata una tecnica, chiamata “quantizzazione”. La quantizzazione si riferisce al processo di riduzione della precisione dei parametri del modello, in genere convertendo i numeri a virgola mobile (che hanno precisione decimale) in numeri interi con una rappresentazione di larghezza in bit più piccola. Mentre la quantizzazione introduce una certa perdita di informazioni, il “dithering”, ovvero l’aggiunta di piccole quantità di rumore casuale ai dati prima della quantizzazione, può aiutare a mitigare questa perdita diffondendo l’errore di quantizzazione.
Oltre a semplificare o “ridimensionare” il modello, un altro metodo per conservare le risorse consiste nell’utilizzare piattaforme o framework efficienti, come “ggml“.
Retrieval-Augmented Generation e lavoro futuro
Il tentativo di applicare l’IA generativa alla verifica del software richiede la risoluzione di due problemi principali:
- Come fare in modo che il modello «digerisca» enormi set di documenti e basi di codice?
- Come creare i prompt corretti?
Spazio IT sta affrontando il primo problema sfruttando la tecnologia Retrieval-Augmented Generation (RAG), ovvero “il processo di ottimizzazione dell’output di un modello linguistico di grandi dimensioni, in modo che faccia riferimento a una knowledge base autorevole al di fuori delle sue fonti di dati di addestramento prima di generare una risposta”
Spazio IT sta lavorando anche alla generazione di prompt rilevanti, a partire dai propri strumenti di analisi statica.
L’IA generativa attualmente non può sostituire un lettore umano durante l’analisi del testo o del codice sorgente. Tuttavia, gli strumenti creati da Spazio IT, che utilizzano Modelli Locali e tecnologie RAG, sono già in grado di fornire preziosi feedback e suggerimenti utili. Naturalmente, queste raccomandazioni dovrebbero essere sottoposte a verifica preventiva da parte di esperti umani.
La seguente presentazione descrive come la Generative AI possa aiutare Software Verification.