Paolo Liberatore
Titoli di studio:
- 1994 Laurea in ingegneria informatica
- 1998 Dottorato di ricerca in ingegneria informatica
Posizione attuale: professore associato
- Università di Roma "La Sapienza"
- Dipartimento di ingegneria informatica, automatica e gestionale Antonio Ruberti
Periodi trascorsi all'estero:
- agosto-dicembre 1996: attività di ricerca presso i laboratori AT&T (Murray Hill, NJ) sul problema della compilazione di problemi NP completi e complessità di ragionamento sulle azioni e revisione della conoscenza;
- settembre-dicembre 1998: attività di ricerca presso l'Università di Linköping sul problema della complessità della soddisfacibilità di vincoli e su tecniche di soddisfacibilità massimale di formule proposizionale.
Progetti
Paolo Liberatore è stato responsabile italiano del progetto coordinato Italia-Francia "Knowledge fusion and planning in multi-agent decision making" e del progetto di ateneo "Applicazioni di tecniche di intelligenza artificiale alla composizione di servizi web". Ha inoltre partecipato ai seguenti progetti:
- Model checking e satisfiability: sviluppo di nuove procedure di decisione e loro valutazione ed analisi sperimentale comparate in ambito applicativo." (progetto cofinanziato MURST)
- Robotica mobile basata su conoscenza" (progetto di ateneo)
- "Strumenti automatici per la rappresentazione e la verifica di sistemi complessi" (progetto di facoltà)
- "Sistemi multirobot per interventi in casi di emergenza: architettura cognitiva e visione artificiale." (progetto di ateneo)
- "Tecniche di verifica automatica per Web Services" (progetto di facoltà)
- "Sistemi Avanzati di Intelligenza Artificiale per i Web Services" (progetto PRIN)
- "Automazione dell'ingegneria del software basata su conoscenza (ASTRO)" (progetto FIRB)
- "Applicazioni di tecniche di intelligenza artificiale alla composizione di servizi web" (progetto di ateneo)
Attività di revisione e organizzazione
- comitato di programma
- ECSQUARU 2001, KR 2002, NMR 2002, ECSQUARU 2003, KR 2004.
- Revisione di articoli per le seguenti conferenze:
- AAAI'98, AI*IA'95, AI*IA'97, AI*IA'99, AIMSA'98, BISFAI'99, ECAI'98, EPIA'95, IJCAI'97, IJCAI'99, KR'98, STACS 2000, ECAI 2000, KR 2000, PODS 2000, IJCAI 2001, PODS 2002, ECAI 2002, IJCAI 2003, KR 2004, KR 2006, KR 2010, ECAI 2012 e KR 2012.
- revisione per riviste:
- Artificial Intelligence Journal, Journal of Artificial Intelligence Research, International Journal of Cooperative Information Systems, Annals of Mathematics and Artificial Intelligence.
- comitati scientifici riviste
- ex membro del comitato scientifico (editorial board) della rivista Journal of Artificial Intelligence Research (JAIR); ex membro dell'advisory board
La ricerca svolta da Paolo Liberatore è concentrata sui formalismi logici per la rappresentazione della conoscenza in intelligenza artificiale, e su argomenti di complessità computazionale. In particolare ha lavorato sui seguenti temi.
Belief Revision (revisione della conoscenza). Questo è stato anche l'argomento principale della tesi di laurea. La tesi contiene in particolare la proposta di un operatore commutativo per l'integrazione di informazioni provenienti da varie fonti, ognuna con un uguale livello di plausibilità. Estratti della tesi sono stati pubblicati. Il primo articolo pubblicato contiene un algoritmo efficiente per la revisione della conoscenza. Questo algoritmo, a partire da una descrizione della base di conoscenza in forma clausale, identifica un possibile modello da eliminare, e in base a questa scelta rimuove dalla base di conoscenza le clausole che sono soddisfatte da questo modello. Un aspetto importante dei formalismi logici è quello della correlazione esistente fra essi. Questo permette la definizione di proprietà generali, e il riuso di algoritmi proposti in un formalismo in altri formalismi. Un articolo su conferenza poi pubblicato su rivista contiene una serie completa di riduzioni dal problema della revisione della conoscenza a quello della cirumscription, e viceversa. Dal momento che tutte queste riduzioni sono polinomiali, questo permette appunto di utilizzare algoritmi sviluppati per uno dei due formalismi nell'altro. Una simile correlazione fra il problema del belief update e quello della assunzione di mondo chiuso è stata stabilita: molti dei formalismi per l'aggiornamento della conoscenza che sono stati proposti per risolvere questo problema nel caso di formule disgiuntive sono riconducibili a opportuni formalismi introdotti precedentemente per la trattazione della assunzione di mondo chiuso. Una variante della revisione è stata introdotta, ed è stato presentato un formalismo generale di fusione di basi di conoscenza con lo stesso grado di priorità. Una definizione e implementazione di un sistema in grado di effettuare allo stesso tempo fusione, revisione e aggiornamento è stata poi realizzata. La generalizzazione di revisione, arbitraggio e aggiornamento ha portato all definizione di una semantica che consente il trattamento di problemi che comportano l'uso di tutti e tre gli operatori. Questa semantica è stata successivamente implementata.
Abduzione Uno dei problemi considerati è quello di trovare un insieme minimo di test che permettono di identificare univocamente una spiegazione abduttiva. Questo problema è applicabile a tutti i problemi di tipo diagnostico che si possono codificare in termini di abduzione, dal momento che lo scopo della diagnosi è quello di identificare univocamente le cause di un insieme di manifestazioni. L'abduzione è spesso usata per formalizzare problemi in cui la teoria logica, e gli insiemi di ipotesi e di (possibili) manifestazioni sono noti in anticipo, mentre l'insieme di manifestazioni effettivamente osservate può risultare noto molto piu'u tardi. Per problemi di questo tipo una precompilazione della parte di input nota in anticipo puè risultare vantaggiosa; questo tipo di strategia è stata quindi analizzata.
Computational Complexity (complessità computazionale). In questo campo, Paolo Liberatore ha lavorato essenzialmente alle proprietà computazionali della teoria delle azioni e del cambiamento. L'analisi computazionale è utile per determinare l'esatto grado di difficoltà dei problemi in intelligenza artificiale. Una prima analisi ha riguardato la complessità della revisione della conoscenza, nel caso in cui è richesta una sequenza di revisioni invece che una revisione singola. In seguito è stata studiata la complessità del belief update e del problema della ridondanza. Un problema centrale nello studio di complessità è quello della verifica di modelli, di cui è stato condotto uno studio sistematico di complessità, dimostrando tra le altre cose come la complessità del problema di verifica dei modelli può differire dalla complessità della implicazione. A rulstati simili risultati è anche giunta l'analisi della complessità della verifica dei modelli in sulla logica dei default: restrizioni della logica che hanno la stessa complessità di inferenza presentano invece proprietà differenti quando si considera il problema della verifica dei modelli. Dal momento che esistono molte semantiche diverse per default logic, è utile analizzare le teorie che hanno una interpretazione unica. Il loro studio consente di estendere dei risultati a più semantiche. Un altro studio di complessità ha riguardato il ragionamento sulle azioni, dimostrando che il formalismo base proposizionale è NP-completo. Questo implica che, sebbene il problema sia da considerarsi difficile, esistono delle tecniche algoritmiche che potrebbero consentirne la soluzione. In particolare, si dimostra la possibilità di utilizzare algoritmi per la soddisfacibilità di formule proposizionali, mostrando una traduzione molto semplice dalla logica delle azioni a quella proposizionale. Un problema simile, ma molto più complesso, è quello delle logiche lineari temporali. In questo caso, si è mostrata una traduzione da QBF a queste logiche, che produce vari benefici, fra cui la possibilità di risolvere problemi di QBF usando risolutori di logica noti, e quello di generare problemi difficili in modo casuale. Uno studio di complessità del problema della pianificazione automatica ha riguardato il problema della ripianificazione, ossia della costruzione di un piano qualora un piano precedentemente noto risulti non più valido a causa di un cambiamento degli obiettivi da raggiungere o di una scoperta di errori nella descrizione dello stato iniziale. Riguardo al problema della soddisfacibilità di vincoli, è stata considerata la complessità e la approssimabilità del problema di trovare un insieme massimale di variabili che soddisfino i vincoli. La complessità teorica dell'algoritmo di Davis, Putnam, Logemann e Loveland è stata analizzata, dimostrando che la complessità di determinare in modo ottimo la variabile su cui fare branching (tale scelta è una parte dell'algoritmo) è computazionalmente più difficile del problema che si vuole risolvere. La immediata conseguenza di questo risultato è che non è sensato indirizzarsi verso la scelta ottima, ma che effettuare scelte non ottime è in generale necessario. Questo risultato è stato poi esteso, in un successivo articolo, al caso in cui il branching è limitato a un insieme di variabili e all'algoritmo di risoluzione. Altre analisi hanno riguardato la unicità delle estensioni nella teoria dei default e problemi la dipendenza fra variabili nella logica proposizionale.
Compilabilità e rappresentazioni compatte Questa è una nuova applicazione della complessità computazionale. Il punto di partenza di questo studio è stata la definizione di due generachie di classi di problemi che formalizzano il livello di difficoltà di problemi in cui una compilazione di parte dell'input è permessa. Lo studio della possibilità di ridurre la complessità del problema in questo modo è stata poi portato avanti, considerando problemi differenti come la diagnosi, la pianificazione automatica, il ragionamento su azioni e la revisione della conoscenza. I Markov Decision Process, che formalizzano problemi di pianificazione in situazioni di incertezza, sono stati in seguito considerati. A partire dalla formalizzazione delle classi di compilabilità è possibile dimostrare risultati sulla rappresentazione succinta informazioni in formalismi logici. Dimostrazioni di non-compilabilità possono venire sfruttate per dimostrare che alcuni formalismi proposizionali sono in grado di rappresentare l'informazione in minore spazio. È stata analizzata la possibilità di rappresentare il risultato di una revisione in forma compatta. Questo problema è stato poi considerato anche nel caso in cui la informazione sia rappresentata in forma di clausole di Horn. Il problema della rappresentazione compatta di politiche per i processi di decisione markoviani (MDP), che sono problemi di pianificazione probabilistica, è in seguito analizzato.
- due volte: borsa di studio CNR per neolaureati
- premio ECCAI per migliore tesi di dottorato europea nell'ambito della intelligenza artificiale presentata nell'anno 1998
- migliore articolo alla conferenza KR 2004
Membro di
Ultime pubblicazioni
Belief merging in absence of reliability information on SYNTHESE | 2022 |
Belief Integration and Source Reliability Assessment on THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH | 2018 |
Belief merging by examples on ACM TRANSACTIONS ON COMPUTATIONAL LOGIC | 2015 |
On the complexity of second-best abductive explanations on INTERNATIONAL JOURNAL OF APPROXIMATE REASONING | 2015 |
Revision by History on THE JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH | 2015 |