Focus

VoxLogicA: uno strumento per l'analisi dichiarativa di immagini

Come si può fare in modo che gli esperti di dominio nell'analisi di immagini (mediche) possano formalizzare, eseguire, migliorare e condividere i loro metodi, per esempio, per identificare tumori del cervello nelle immagini di risonanza magnetica 3D -- con solide garanzie che i loro risultati siano portabili,
predicibili e riproducibili, e con requisiti minimi sulla loro capacità ed esperienza informatica?

VoxLogicA è uno strumento progettato per supportare l'analisi di immagini, che pone l'accento sulla semplicità, focalizzato sulla produzione di risultati spiegabili e indipendenti dall'implementazione. Una sessione di VoxLogicA è una specifica testuale dell'analisi, che impiega una combinazione di caratteristiche spaziali (distanza fra le regioni, o inter-raggiungibilità), con similarità di texture, e primitive di imaging.

Le sessioni di VoxLogicA sono scritte usando un linguaggio logico dichiarativo, chiamato ImgQL ("Image Query Language"), ispirato da applicazioni largamente riconosciute, come lo "Structured Query Language" (SQL) per le basi di dati, con solide fondamenta matematiche, radicate nell'area delle Logiche Spaziali per gli Spazi Topologici.

VoxLogicA è un software pubblicamente distribuito, libero, gratuito e open source. Alla base vi è un "model checker", vale a dire un motore di calcolo molto potente per le query logiche, che sfrutta tecnologie avanzate, come la memoization e il multithreading, per ottenere performance di altissimo livello.

In uno studio recente, che fa parte di una collaborazione fra il gruppo "Formal Methods and Tools" dell'ISTI-CNR, e l'Azienda Ospedaliera Universitaria Senese, VoxLogicA è stato usato per produrre una specifica di appena 10 righe di testo, che può identificare un glioblastoma in una immagine 3D di risonanza magnetica in 8 secondi, su un comune laptop. Per fare un confronto, il tempo che serve ad un radioterapista esperto per eseguire lo stesso task è di circa mezz'ora.
La stessa procedura è stata applicata a circa 200 casi (il noto dataset "BRAin Tumor Segmentation (BRATS) challenge"). L'accuratezza dei risultati ottenuti può essere misurata; la nuova procedura dà risultati simili ai migliori metodi della BRATS challenge nel 2017 -- che rappresenta lo stato dell'arte nel campo, dominato da metodi di tipo "machine-learning" -- ed è confrontabile con la contornazione manuale fatta da esperti umani.

Sarà certamente molto rilevante nel prossimo futuro migliorare questo lavoro, sia nella direzione di studi clinici, sia per incorporare altri approcci computazionali, che possono essere coordinati e armonizzati usando specifiche logiche ad alto livello.

Un articolo di prossima pubblicazione che illustra il tool e le sue applicazioni alla segmentazione del glioblastoma sarà presentato alla "25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)", affiliata a "European Joint Conferences on Theory and Practice of Software (ETAPS)":

G. Belmonte, V. Ciancia, D. Latella, M. Massink. "VoxLogicA: a Spatial Model Checker for Declarative Image Analysis".

Il codice sorgente e gli eseguibili di VoxLogicA sono disponibili sul sito:
https://github.com/vincenzoml/VoxLogicA
corredati da un semplice esempio di un task di rimozione dello sfondo in 2D, che fa da tutorial per il tool.