Intervista a Laura Bussi, lecturer alla University of Amsterdam e vincitrice del Premio «Paolo Gentilini» 2026 dell’AILA per le applicazioni biomediche della logica.

Ciao Laura! Quest’anno hai vinto il Premio Gentilini per le applicazioni della logica in ambito biomedico, e nello specifico per il tuo lavoro sulle logiche modali spaziali applicate al medical imaging per la segmentazione automatica di tumori. Ci racconti come funziona questo legame tra logica formale e imaging medico?

Grazie! È stato davvero bello ricevere questo riconoscimento, e voglio ringraziare AILA, i miei supervisori Vincenzo Ciancia e Fabio Gadducci, così come i miei coautori, i colleghi e le persone che mi sono state vicine in questi anni.
Il legame tra logica e imaging medico passa attraverso un metodo ben conosciuto e studiato in informatica, ovvero il model checking. Il model checking è una tecnica che permette di verificare algoritmicamente se una specifica formale sia soddisfatta da un modello che rappresenta un sistema. Ovviamente, la specifica deve essere scritta in un linguaggio rigoroso, ovvero in una qualche logica.

Normalmente, il model checking è usato per verificare proprietà temporali di un sistema. Per esempio, potremmo desiderare che un’azione sia eseguita immediatamente dopo un’altra. Pensate a un distributore di bevande: vogliamo che il caffè sia erogato dopo aver inserito denaro sufficiente e premuto il tasto corrispondente. Con il model checking, possiamo modellare il comportamento del nostro distributore, esprimere la proprietà desiderata usando una logica temporale, e il model checker, ovvero il software che implementa l’algoritmo di model checking, verificherà automaticamente se la proprietà sia soddisfatta.
Il progetto elaborato in seno al CNR, dal gruppo del mio supervisore Vincenzo Ciancia e altri colleghi, è stato usare il model checking per analizzare strutture spaziali o spazio-temporali, invece che solo temporali. Per fare ciò occorrono diversi ingredienti: una logica che ci permetta di ragionare su proprietà dello spazio, dei modelli che rappresentino strutture spaziali, e un model checker capace di analizzare questi modelli.

A questo punto è necessario porsi due domande: a quali spazi siamo interessati? E quali proprietà vogliamo esprimere? Ci sono molti esempi di spazi interessanti, per esempio i poliedri, che sono usati per rappresentare modelli 3D, o i grafi. Questi esempi fanno parte della stessa classe di spazi, chiamati spazi pre-topologici o Čech closure spaces. Possiamo quindi stabilire che gli spazi usati per i nostri modelli sono Čech closure spaces.
Possiamo adesso pensare alle proprietà a cui siamo interessati. Senz’altro ci sono proprietà di vicinato, ad esempio “tutti i vicini di un punto soddisfano una certa formula”. Ma potremmo anche essere interessati a proprietà di raggiungibilità, come “esiste un cammino fino a un punto che soddisfa A, che passa solo da punti che soddisfano B”. Introduciamo quindi una logica, chiamata Spatial Logic for Closure Spaces, che per certi aspetti estende la logica topologica di Tarski e McKinsey, interpretando l’operatore diamond come chiusura di Čech e introducendo un operatore di raggiungibilità.

E le immagini?

Proviamo a osservarle in questo modo: consideriamo i pixel come un insieme di vertici, e colleghiamo i vertici che sono vicini tra loro nell’immagine. Le proposizioni atomiche sono le proprietà di un pixel, come il colore o l’intensità. Abbiamo ottenuto un modello dove lo spazio è un grafo planare, quindi uno spazio pretopologico. Manca l’ultimo ingrediente, ovvero un model checker: il tool sviluppato al CNR si chiama VoxLogicA, ed è un model checker specializzato nell’analisi di immagini, basato sulla libreria di imaging ITK. A questo punto la catena è completa: abbiamo un linguaggio formale per esprimere proprietà di un’immagine, dei modelli (ovvero una qualunque immagine), e un model checker.

E le applicazioni?

L’analisi di immagini mediche segue delle procedure ben definite, che ben si prestano a essere formalizzate usando la logica spaziale. Non è l’unico approccio esistente: molti metodi di machine learning vengono utilizzati per lo stesso scopo. Ma VoxLogicA è facile da usare, trasparente e spiegabile, ed evita errori che possono essere commessi dal ragionamento statistico dei modelli di ML, con un’accuratezza pari a quella dei modelli più performanti e delle buone performance, a dimostrazione di come la logica spaziale abbia del potenziale per le applicazioni concrete.

La tua formazione è di natura informatica, a dimostrazione di come la logica sia davvero multidisciplinare. Come ti sei avvicinata a questa area di ricerca?

A dire il vero, io mi sono sempre sentita un po’ a metà tra i due mondi! Ho iniziato a studiare informatica spinta dal libro “Godel, Escher, Bach“, quindi per una fascinazione nei confronti della logica e dell’informatica teorica. Al di là della teoria in sé, però, sono sempre stata interessata a come i risultati teorici potessero trovare applicazione pratica. La mia tesi triennale è stata molto teorica, ma durante la magistrale mi sono interessata anche a corsi più pratici, come programmazione parallela e distribuita. Durante il corso di verifica del software, Vincenzo ha tenuto una lezione sulla logica spaziale e VoxLogicA, e mi sono innamorata del progetto. Cercava qualcuno che lavorasse all’implementazione su GPU di VoxLogicA per migliorare l’efficienza, e così quella è diventata la mia tesi magistrale, e, in seguito, parte del mio dottorato. Durante il dottorato ho continuato a lavorare su due fronti, ovvero l’assiomatizzazione della logica spaziale e l’introduzione di operatori temporali, e loro implementazione, per poter puntare ad applicazioni come il tracciamento di lesioni attraverso sequenze di immagini mediche. Insomma, sono rimasta un po’ a fare da ponte tra la logica e le sue applicazioni concrete, ed è una situazione che mi piace molto.

C’è un momento nel tuo percorso in cui hai visto la logica “funzionare” davvero su dati clinici reali — magari un caso in cui l’approccio formale ha dato un risultato che un metodo più empirico non avrebbe colto?

Beh, qui occorre ammetterlo: i modelli di IA subsimbolica attuali sono molto validi per questi compiti, quindi non posso dire di aver visto il nostro metodo surclassare gli altri in termini di risultati. Però ci sono situazioni in cui sbagliano. Ad esempio, nel dataset BraTS, composto di immagini di gliomi, capita che questi “colorino” come tumore anche parte del cervelletto, mentre sappiamo che questo è scorretto e la logica ci permette di evitarlo. Oggi tendo a vedere i due approcci come complementari, ovvero usare la logica per guidare l’AI subsimbolica verso risultati spiegabili e corretti. C’è una parte di conoscenza che può essere codificata a prescindere, e non appresa dall’esperienza: per esempio, noi non impariamo che non si attraversa con il semaforo rosso per esperienza, lo sappiamo già. Un altro punto che reputo interessante è il vantaggio in termini ambientali: addestrare e usare questi modelli è costoso e inquinante, e la logica ci permette di ridurre questo impatto. In questo senso, per me è stato molto emozionante vedere per la prima volta un video generato da VoxLogicA GPU che mostrava il risultato dell’analisi frame by frame. Quello che avrebbe richiesto giorni di addestramento di una Neural Network girava sul mio laptop senza richiedere lavoro aggiuntivo.

Concludiamo con una riflessione più ampia. La logica ha spesso un’immagine di disciplina astratta, lontana dal mondo reale. Il tuo lavoro sembra raccontare una storia completamente diversa. Quanto pensi che il potenziale applicativo della logica sia ancora sottovalutato, anche all’interno della comunità scientifica? E quali altri campi ti sembrano terreno fertile per i prossimi anni?

Credo di aver messo qualche seme per questa domanda già nelle risposte precedenti, e sì, purtroppo la logica ha questa fama di materia completamente astratta, che non trova applicazioni reali. E mi sembra che, nei primi anni del boom dei Large Language Models, questo atteggiamento si sia addirittura esacerbato. Ricordo molti discorsi tipo “ah sì, i metodi formali, quelli che funzionano solo in teoria, ma poi non scalano o sono troppo difficili”. Oggi credo che il vento stia un po’ cambiando. Sia l’AI neurosimbolica che l’explainable AI sono campi dove c’è fermento, perché si comincia a capire che questi modelli sono difficili da controllare, non trasparenti e possibilmente pericolosi. Pensiamo, ad esempio, ai bias che ereditano dai dati di training, o la possibilità che generino “allucinazioni”, ossia informazioni false o perfino dannose. Credo che la logica abbia grandi potenzialità in questo campo. Per certi versi rimane una disciplina astratta, ma questo non vuol dire che sia lontana dal mondo reale. Oltre a campi come il model checking, dove la logica viene usata quotidianamente per applicazioni reali, credo che quello dell’interazione tra conoscenza simbolica e subsimbolica sia oggi il campo più fertile, in cui la logica ha molte possibilità da esplorare.

Guarda la pagina  AILA x MaddMaths!

AILAxMaddMaths!

AILA x MaddMaths! è un progetto di divulgazione e comunicazione della logica promosso dall’AILA, pensato per raccontare la logica in tutte le sue sfaccettature.